Uses the following modules:
Is used by the following modules:
First distributive law (first direction):
1. Proposition
((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) (hilb36)
1 | ((P Ù Q) Þ P) | add proposition hilb24 |
2 | ((P Ù A) Þ P) | replace proposition variable Q by A in 1 |
3 | ((B Ù A) Þ B) | replace proposition variable P by B in 2 |
4 | ((Q Ù A) Þ Q) | replace proposition variable B by Q in 3 |
5 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
6 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 5 |
7 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 6 |
8 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 7 |
9 | ((D Þ C) Þ ((P Ú D) Þ (P Ú C))) | replace proposition variable B by P in 8 |
10 | ((D Þ Q) Þ ((P Ú D) Þ (P Ú Q))) | replace proposition variable C by Q in 9 |
11 | (((Q Ù A) Þ Q) Þ ((P Ú (Q Ù A)) Þ (P Ú Q))) | replace proposition variable D by (Q Ù A) in 10 |
12 | ((P Ú (Q Ù A)) Þ (P Ú Q)) | modus ponens with 4, 11 |
13 | ((P Ù Q) Þ Q) | add proposition hilb25 |
14 | ((P Ù A) Þ A) | replace proposition variable Q by A in 13 |
15 | ((B Ù A) Þ A) | replace proposition variable P by B in 14 |
16 | ((Q Ù A) Þ A) | replace proposition variable B by Q in 15 |
17 | ((D Þ A) Þ ((P Ú D) Þ (P Ú A))) | replace proposition variable C by A in 9 |
18 | (((Q Ù A) Þ A) Þ ((P Ú (Q Ù A)) Þ (P Ú A))) | replace proposition variable D by (Q Ù A) in 17 |
19 | ((P Ú (Q Ù A)) Þ (P Ú A)) | modus ponens with 16, 18 |
20 | (P Þ (Q Þ (P Ù Q))) | add proposition hilb28 |
21 | (P Þ (A Þ (P Ù A))) | replace proposition variable Q by A in 20 |
22 | (B Þ (A Þ (B Ù A))) | replace proposition variable P by B in 21 |
23 | (B Þ ((P Ú A) Þ (B Ù (P Ú A)))) | replace proposition variable A by (P Ú A) in 22 |
24 | ((P Ú Q) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) | replace proposition variable B by (P Ú Q) in 23 |
25 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
26 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 25 |
27 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 26 |
28 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 27 |
29 | ((D Þ C) Þ (((P Ú (Q Ù A)) Þ D) Þ ((P Ú (Q Ù A)) Þ C))) | replace proposition variable B by (P Ú (Q Ù A)) in 28 |
30 | ((D Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ D) Þ ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))))) | replace proposition variable C by ((P Ú A) Þ ((P Ú Q) Ù (P Ú A))) in 29 |
31 | (((P Ú Q) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ (P Ú Q)) Þ ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))))) | replace proposition variable D by (P Ú Q) in 30 |
32 | (((P Ú (Q Ù A)) Þ (P Ú Q)) Þ ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A))))) | modus ponens with 24, 31 |
33 | ((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) | modus ponens with 12, 32 |
34 | ((P Þ (Q Þ A)) Þ (Q Þ (P Þ A))) | add proposition hilb16 |
35 | ((P Þ (Q Þ B)) Þ (Q Þ (P Þ B))) | replace proposition variable A by B in 34 |
36 | ((P Þ (C Þ B)) Þ (C Þ (P Þ B))) | replace proposition variable Q by C in 35 |
37 | ((D Þ (C Þ B)) Þ (C Þ (D Þ B))) | replace proposition variable P by D in 36 |
38 | ((D Þ (C Þ ((P Ú Q) Ù (P Ú A)))) Þ (C Þ (D Þ ((P Ú Q) Ù (P Ú A))))) | replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 37 |
39 | ((D Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ ((P Ú A) Þ (D Þ ((P Ú Q) Ù (P Ú A))))) | replace proposition variable C by (P Ú A) in 38 |
40 | (((P Ú (Q Ù A)) Þ ((P Ú A) Þ ((P Ú Q) Ù (P Ú A)))) Þ ((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))))) | replace proposition variable D by (P Ú (Q Ù A)) in 39 |
41 | ((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) | modus ponens with 33, 40 |
42 | ((D Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ D) Þ ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))))) | replace proposition variable C by ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) in 29 |
43 | (((P Ú A) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Þ (((P Ú (Q Ù A)) Þ (P Ú A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))))) | replace proposition variable D by (P Ú A) in 42 |
44 | (((P Ú (Q Ù A)) Þ (P Ú A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))))) | modus ponens with 41, 43 |
45 | ((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) | modus ponens with 19, 44 |
46 | ((P Þ (P Þ Q)) Þ (P Þ Q)) | add proposition hilb33 |
47 | ((P Þ (P Þ A)) Þ (P Þ A)) | replace proposition variable Q by A in 46 |
48 | ((B Þ (B Þ A)) Þ (B Þ A)) | replace proposition variable P by B in 47 |
49 | ((B Þ (B Þ ((P Ú Q) Ù (P Ú A)))) Þ (B Þ ((P Ú Q) Ù (P Ú A)))) | replace proposition variable A by ((P Ú Q) Ù (P Ú A)) in 48 |
50 | (((P Ú (Q Ù A)) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) Þ ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A)))) | replace proposition variable B by (P Ú (Q Ù A)) in 49 |
51 | ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) | modus ponens with 45, 50 |
qed |
First distributive law (second direction):
2. Proposition
(((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) (hilb37)
1 | (P Þ (Q Þ (P Ù Q))) | add proposition hilb28 |
2 | (P Þ (A Þ (P Ù A))) | replace proposition variable Q by A in 1 |
3 | (B Þ (A Þ (B Ù A))) | replace proposition variable P by B in 2 |
4 | (Q Þ (A Þ (Q Ù A))) | replace proposition variable B by Q in 3 |
5 | ((P Þ Q) Þ ((A Ú P) Þ (A Ú Q))) | add axiom axiom4 |
6 | ((P Þ Q) Þ ((B Ú P) Þ (B Ú Q))) | replace proposition variable A by B in 5 |
7 | ((P Þ C) Þ ((B Ú P) Þ (B Ú C))) | replace proposition variable Q by C in 6 |
8 | ((D Þ C) Þ ((B Ú D) Þ (B Ú C))) | replace proposition variable P by D in 7 |
9 | ((D Þ C) Þ ((P Ú D) Þ (P Ú C))) | replace proposition variable B by P in 8 |
10 | ((D Þ (Q Ù A)) Þ ((P Ú D) Þ (P Ú (Q Ù A)))) | replace proposition variable C by (Q Ù A) in 9 |
11 | ((A Þ (Q Ù A)) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) | replace proposition variable D by A in 10 |
12 | ((P Þ Q) Þ ((A Þ P) Þ (A Þ Q))) | add proposition hilb1 |
13 | ((P Þ Q) Þ ((B Þ P) Þ (B Þ Q))) | replace proposition variable A by B in 12 |
14 | ((P Þ C) Þ ((B Þ P) Þ (B Þ C))) | replace proposition variable Q by C in 13 |
15 | ((D Þ C) Þ ((B Þ D) Þ (B Þ C))) | replace proposition variable P by D in 14 |
16 | ((D Þ C) Þ ((Q Þ D) Þ (Q Þ C))) | replace proposition variable B by Q in 15 |
17 | ((D Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((Q Þ D) Þ (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))))) | replace proposition variable C by ((P Ú A) Þ (P Ú (Q Ù A))) in 16 |
18 | (((A Þ (Q Ù A)) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((Q Þ (A Þ (Q Ù A))) Þ (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))))) | replace proposition variable D by (A Þ (Q Ù A)) in 17 |
19 | ((Q Þ (A Þ (Q Ù A))) Þ (Q Þ ((P Ú A) Þ (P Ú (Q Ù A))))) | modus ponens with 11, 18 |
20 | (Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))) | modus ponens with 4, 19 |
21 | ((P Þ (Q Þ A)) Þ (Q Þ (P Þ A))) | add proposition hilb16 |
22 | ((P Þ (Q Þ B)) Þ (Q Þ (P Þ B))) | replace proposition variable A by B in 21 |
23 | ((P Þ (C Þ B)) Þ (C Þ (P Þ B))) | replace proposition variable Q by C in 22 |
24 | ((D Þ (C Þ B)) Þ (C Þ (D Þ B))) | replace proposition variable P by D in 23 |
25 | ((D Þ (C Þ (P Ú (Q Ù A)))) Þ (C Þ (D Þ (P Ú (Q Ù A))))) | replace proposition variable B by (P Ú (Q Ù A)) in 24 |
26 | ((D Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ (D Þ (P Ú (Q Ù A))))) | replace proposition variable C by (P Ú A) in 25 |
27 | ((Q Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ (Q Þ (P Ú (Q Ù A))))) | replace proposition variable D by Q in 26 |
28 | ((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) | modus ponens with 20, 27 |
29 | ((D Þ (P Ú (Q Ù A))) Þ ((P Ú D) Þ (P Ú (P Ú (Q Ù A))))) | replace proposition variable C by (P Ú (Q Ù A)) in 9 |
30 | ((Q Þ (P Ú (Q Ù A))) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) | replace proposition variable D by Q in 29 |
31 | ((D Þ C) Þ (((P Ú A) Þ D) Þ ((P Ú A) Þ C))) | replace proposition variable B by (P Ú A) in 15 |
32 | ((D Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) Þ (((P Ú A) Þ D) Þ ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))))) | replace proposition variable C by ((P Ú Q) Þ (P Ú (P Ú (Q Ù A)))) in 31 |
33 | (((Q Þ (P Ú (Q Ù A))) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) Þ (((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))))) | replace proposition variable D by (Q Þ (P Ú (Q Ù A))) in 32 |
34 | (((P Ú A) Þ (Q Þ (P Ú (Q Ù A)))) Þ ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A)))))) | modus ponens with 30, 33 |
35 | ((P Ú A) Þ ((P Ú Q) Þ (P Ú (P Ú (Q Ù A))))) | modus ponens with 28, 34 |
36 | ((P Ú A) Þ ((P Ú Q) Þ ((P Ú P) Ú (Q Ù A)))) | elementary equivalence in 35 at 1 of hilb14 with hilb15 |
37 | ((P Ú A) Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) | elementary equivalence in 36 at 1 of hilb11 with hilb12 |
38 | ((D Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) Þ ((P Ú Q) Þ (D Þ (P Ú (Q Ù A))))) | replace proposition variable C by (P Ú Q) in 25 |
39 | (((P Ú A) Þ ((P Ú Q) Þ (P Ú (Q Ù A)))) Þ ((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A))))) | replace proposition variable D by (P Ú A) in 38 |
40 | ((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) | modus ponens with 37, 39 |
41 | ((P Þ (Q Þ A)) Þ ((P Ù Q) Þ A)) | add proposition hilb29 |
42 | ((P Þ (Q Þ B)) Þ ((P Ù Q) Þ B)) | replace proposition variable A by B in 41 |
43 | ((P Þ (C Þ B)) Þ ((P Ù C) Þ B)) | replace proposition variable Q by C in 42 |
44 | ((D Þ (C Þ B)) Þ ((D Ù C) Þ B)) | replace proposition variable P by D in 43 |
45 | ((D Þ (C Þ (P Ú (Q Ù A)))) Þ ((D Ù C) Þ (P Ú (Q Ù A)))) | replace proposition variable B by (P Ú (Q Ù A)) in 44 |
46 | ((D Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ ((D Ù (P Ú A)) Þ (P Ú (Q Ù A)))) | replace proposition variable C by (P Ú A) in 45 |
47 | (((P Ú Q) Þ ((P Ú A) Þ (P Ú (Q Ù A)))) Þ (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A)))) | replace proposition variable D by (P Ú Q) in 46 |
48 | (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) | modus ponens with 40, 47 |
qed |
A form for the abbreviation rule form for disjunction (first direction):
3. Proposition
((P Ú Q) Þ Ø(ØP Ù ØQ)) (hilb38)
1 | (P Þ P) | add proposition hilb2 |
2 | (Q Þ Q) | replace proposition variable P by Q in 1 |
3 | ((P Ú Q) Þ (P Ú Q)) | replace proposition variable Q by (P Ú Q) in 2 |
4 | ((P Ú Q) Þ ØØ(P Ú Q)) | elementary equivalence in 3 at 5 of hilb5 with hilb6 |
5 | ((P Ú Q) Þ ØØ(ØØP Ú Q)) | elementary equivalence in 4 at 8 of hilb5 with hilb6 |
6 | ((P Ú Q) Þ ØØ(ØØP Ú ØØQ)) | elementary equivalence in 5 at 11 of hilb5 with hilb6 |
7 | ((P Ú Q) Þ Ø(ØP Ù ØQ)) | reverse abbreviation and in 6 at occurence 1 |
qed |
A form for the abbreviation rule form for disjunction (second direction):
4. Proposition
(Ø(ØP Ù ØQ) Þ (P Ú Q)) (hilb39)
1 | (P Þ P) | add proposition hilb2 |
2 | (Q Þ Q) | replace proposition variable P by Q in 1 |
3 | ((P Ú Q) Þ (P Ú Q)) | replace proposition variable Q by (P Ú Q) in 2 |
4 | (ØØ(P Ú Q) Þ (P Ú Q)) | elementary equivalence in 3 at 2 of hilb5 with hilb6 |
5 | (ØØ(ØØP Ú Q) Þ (P Ú Q)) | elementary equivalence in 4 at 5 of hilb5 with hilb6 |
6 | (ØØ(ØØP Ú ØØQ) Þ (P Ú Q)) | elementary equivalence in 5 at 8 of hilb5 with hilb6 |
7 | (Ø(ØP Ù ØQ) Þ (P Ú Q)) | reverse abbreviation and in 6 at occurence 1 |
qed |
By duality we get the second distributive law (first direction):
5. Proposition
((P Ù (Q Ú A)) Þ ((P Ù Q) Ú (P Ù A))) (hilb40)
1 | (((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) | add proposition hilb37 |
2 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
3 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 2 |
4 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 3 |
5 | ((B Þ (P Ú (Q Ù A))) Þ (Ø(P Ú (Q Ù A)) Þ ØB)) | replace proposition variable A by (P Ú (Q Ù A)) in 4 |
6 | ((((P Ú Q) Ù (P Ú A)) Þ (P Ú (Q Ù A))) Þ (Ø(P Ú (Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A)))) | replace proposition variable B by ((P Ú Q) Ù (P Ú A)) in 5 |
7 | (Ø(P Ú (Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A))) | modus ponens with 1, 6 |
8 | (Ø(P Ú ØØ(Q Ù A)) Þ Ø((P Ú Q) Ù (P Ú A))) | elementary equivalence in 7 at 5 of hilb5 with hilb6 |
9 | (Ø(P Ú ØØ(Q Ù A)) Þ Ø(ØØ(P Ú Q) Ù (P Ú A))) | elementary equivalence in 8 at 12 of hilb5 with hilb6 |
10 | (Ø(P Ú ØØ(Q Ù A)) Þ Ø(ØØ(P Ú Q) Ù ØØ(P Ú A))) | elementary equivalence in 9 at 17 of hilb5 with hilb6 |
11 | (Ø(P Ú ØØ(Q Ù B)) Þ Ø(ØØ(P Ú Q) Ù ØØ(P Ú B))) | replace proposition variable A by B in 10 |
12 | (Ø(P Ú ØØ(C Ù B)) Þ Ø(ØØ(P Ú C) Ù ØØ(P Ú B))) | replace proposition variable Q by C in 11 |
13 | (Ø(D Ú ØØ(C Ù B)) Þ Ø(ØØ(D Ú C) Ù ØØ(D Ú B))) | replace proposition variable P by D in 12 |
14 | (Ø(D Ú ØØ(C Ù ØA)) Þ Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA))) | replace proposition variable B by ØA in 13 |
15 | (Ø(D Ú ØØ(ØQ Ù ØA)) Þ Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA))) | replace proposition variable C by ØQ in 14 |
16 | (Ø(ØP Ú ØØ(ØQ Ù ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) | replace proposition variable D by ØP in 15 |
17 | ((P Ù Ø(ØQ Ù ØA)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) | reverse abbreviation and in 16 at occurence 1 |
18 | ((P Ù (Q Ú A)) Þ Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA))) | elementary equivalence in 17 at 1 of hilb39 with hilb38 |
19 | ((P Ù (Q Ú A)) Þ (Ø(ØP Ú ØQ) Ú Ø(ØP Ú ØA))) | elementary equivalence in 18 at 1 of hilb39 with hilb38 |
20 | ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú Ø(ØP Ú ØA))) | reverse abbreviation and in 19 at occurence 1 |
21 | ((P Ù (Q Ú A)) Þ ((P Ù Q) Ú (P Ù A))) | reverse abbreviation and in 20 at occurence 1 |
qed |
The second distributive law (second direction):
6. Proposition
(((P Ù Q) Ú (P Ù A)) Þ (P Ù (Q Ú A))) (hilb41)
1 | ((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) | add proposition hilb36 |
2 | ((P Þ Q) Þ (ØQ Þ ØP)) | add proposition hilb7 |
3 | ((P Þ A) Þ (ØA Þ ØP)) | replace proposition variable Q by A in 2 |
4 | ((B Þ A) Þ (ØA Þ ØB)) | replace proposition variable P by B in 3 |
5 | ((B Þ ((P Ú Q) Ù (P Ú A))) Þ (Ø((P Ú Q) Ù (P Ú A)) Þ ØB)) | replace proposition variable A by ((P Ú Q) Ù (P Ú A)) in 4 |
6 | (((P Ú (Q Ù A)) Þ ((P Ú Q) Ù (P Ú A))) Þ (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú (Q Ù A)))) | replace proposition variable B by (P Ú (Q Ù A)) in 5 |
7 | (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú (Q Ù A))) | modus ponens with 1, 6 |
8 | (Ø((P Ú Q) Ù (P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) | elementary equivalence in 7 at 13 of hilb5 with hilb6 |
9 | (Ø(ØØ(P Ú Q) Ù (P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) | elementary equivalence in 8 at 4 of hilb5 with hilb6 |
10 | (Ø(ØØ(P Ú Q) Ù ØØ(P Ú A)) Þ Ø(P Ú ØØ(Q Ù A))) | elementary equivalence in 9 at 9 of hilb5 with hilb6 |
11 | (Ø(ØØ(P Ú Q) Ù ØØ(P Ú B)) Þ Ø(P Ú ØØ(Q Ù B))) | replace proposition variable A by B in 10 |
12 | (Ø(ØØ(P Ú C) Ù ØØ(P Ú B)) Þ Ø(P Ú ØØ(C Ù B))) | replace proposition variable Q by C in 11 |
13 | (Ø(ØØ(D Ú C) Ù ØØ(D Ú B)) Þ Ø(D Ú ØØ(C Ù B))) | replace proposition variable P by D in 12 |
14 | (Ø(ØØ(D Ú C) Ù ØØ(D Ú ØA)) Þ Ø(D Ú ØØ(C Ù ØA))) | replace proposition variable B by ØA in 13 |
15 | (Ø(ØØ(D Ú ØQ) Ù ØØ(D Ú ØA)) Þ Ø(D Ú ØØ(ØQ Ù ØA))) | replace proposition variable C by ØQ in 14 |
16 | (Ø(ØØ(ØP Ú ØQ) Ù ØØ(ØP Ú ØA)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) | replace proposition variable D by ØP in 15 |
17 | (Ø(Ø(P Ù Q) Ù ØØ(ØP Ú ØA)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) | reverse abbreviation and in 16 at occurence 1 |
18 | (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) Þ Ø(ØP Ú ØØ(ØQ Ù ØA))) | reverse abbreviation and in 17 at occurence 1 |
19 | (Ø(Ø(P Ù Q) Ù Ø(P Ù A)) Þ (P Ù Ø(ØQ Ù ØA))) | reverse abbreviation and in 18 at occurence 1 |
20 | (((P Ù Q) Ú (P Ù A)) Þ (P Ù Ø(ØQ Ù ØA))) | elementary equivalence in 19 at 1 of hilb39 with hilb38 |
21 | (((P Ù Q) Ú (P Ù A)) Þ (P Ù (Q Ú A))) | elementary equivalence in 20 at 1 of hilb39 with hilb38 |
qed |
This module is used by the following modules: