MODULE ( HEADER ( SPEC ( NAME ("prophilbert3"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("Further Theorems of Propositional Calculus"), DESCRIPTION ( "This module includes proofs of popositional calculus theorems. The following theorems and proofs are adapted from D. Hilbert and W. Ackermann's `Grundzuege der theoretischen Logik' (Berlin 1928, Springer)" ), EMAIL ("module@qedeq.org"), AUTHORS ( AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org")) ) ), IMPORTS ( IMPORT ( SPEC ( NAME ("prophilbert2"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ) ), USEDBY ( SPEC ( NAME ("predtheo2"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION (".") ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("hilb36"), "First distributive law (first direction):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(1)), ADDSENTENCE ( LINK ("hilb24")) ), LINE ( IMPL(AND(PROP(1), PROP(3)), PROP(1)), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(AND(PROP(4), PROP(3)), PROP(4)), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(AND(PROP(2), PROP(3)), PROP(2)), REPLACEPROP ( 3, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(2)))), REPLACEPROP ( 5, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 6, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 7, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 8, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(2)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(2)))), REPLACEPROP ( 9, PROP(5), PROP(2) ) ), LINE ( IMPL(IMPL(AND(PROP(2), PROP(3)), PROP(2)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2)))), REPLACEPROP ( 10, PROP(6), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2))), MODUSPONENS (4, 11) ), LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(2)), ADDSENTENCE ( LINK ("hilb25")) ), LINE ( IMPL(AND(PROP(1), PROP(3)), PROP(3)), REPLACEPROP ( 13, PROP(2), PROP(3) ) ), LINE ( IMPL(AND(PROP(4), PROP(3)), PROP(3)), REPLACEPROP ( 14, PROP(1), PROP(4) ) ), LINE ( IMPL(AND(PROP(2), PROP(3)), PROP(3)), REPLACEPROP ( 15, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(3)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(3)))), REPLACEPROP ( 9, PROP(5), PROP(3) ) ), LINE ( IMPL(IMPL(AND(PROP(2), PROP(3)), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3)))), REPLACEPROP ( 17, PROP(6), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3))), MODUSPONENS (16, 18) ), LINE ( IMPL(PROP(1), IMPL(PROP(2), AND(PROP(1), PROP(2)))), ADDSENTENCE ( LINK ("hilb28")) ), LINE ( IMPL(PROP(1), IMPL(PROP(3), AND(PROP(1), PROP(3)))), REPLACEPROP ( 20, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(4), IMPL(PROP(3), AND(PROP(4), PROP(3)))), REPLACEPROP ( 21, PROP(1), PROP(4) ) ), LINE ( IMPL(PROP(4), IMPL(OR(PROP(1), PROP(3)), AND(PROP(4), OR(PROP(1), PROP(3))))), REPLACEPROP ( 22, PROP(3), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), REPLACEPROP ( 23, PROP(4), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(2)))), REPLACEPROP ( 25, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 26, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 27, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(5)))), REPLACEPROP ( 28, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 29, PROP(5), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 30, PROP(6), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(2))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), MODUSPONENS (24, 31) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (12, 32) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb16")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(4))), IMPL(PROP(2), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 34, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 35, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(6), PROP(4)))), REPLACEPROP ( 36, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(PROP(5), IMPL(PROP(6), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 37, PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(6), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 38, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 39, PROP(6), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (33, 40) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), PROP(6)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 29, PROP(5), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))))), REPLACEPROP ( 42, PROP(6), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), OR(PROP(1), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), MODUSPONENS (41, 43) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (19, 44) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(2))), IMPL(PROP(1), PROP(2))), ADDSENTENCE ( LINK ("hilb33")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), PROP(3))), REPLACEPROP ( 46, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), IMPL(PROP(4), PROP(3))), IMPL(PROP(4), PROP(3))), REPLACEPROP ( 47, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), IMPL(PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), REPLACEPROP ( 48, PROP(3), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), REPLACEPROP ( 49, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), MODUSPONENS (45, 50) ) ) ) ), PARAGRAPH ( LABEL ("hilb37"), "First distributive law (second direction):", PROPOSITION ( SENTENCE ( IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))) ), PROOF ( LINE ( IMPL(PROP(1), IMPL(PROP(2), AND(PROP(1), PROP(2)))), ADDSENTENCE ( LINK ("hilb28")) ), LINE ( IMPL(PROP(1), IMPL(PROP(3), AND(PROP(1), PROP(3)))), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(4), IMPL(PROP(3), AND(PROP(4), PROP(3)))), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(PROP(2), IMPL(PROP(3), AND(PROP(2), PROP(3)))), REPLACEPROP ( 3, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(3), PROP(1)), OR(PROP(3), PROP(2)))), ADDAXIOM ( LINK ("axiom4")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(2)))), REPLACEPROP ( 5, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(OR(PROP(4), PROP(1)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 6, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(4), PROP(6)), OR(PROP(4), PROP(5)))), REPLACEPROP ( 7, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), PROP(5)))), REPLACEPROP ( 8, PROP(4), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(6), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 9, PROP(5), AND(PROP(2), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(3), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 10, PROP(6), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), ADDSENTENCE ( LINK ("hilb1")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(2)))), REPLACEPROP ( 12, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(5)), IMPL(IMPL(PROP(4), PROP(1)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 13, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(4), PROP(6)), IMPL(PROP(4), PROP(5)))), REPLACEPROP ( 14, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(PROP(2), PROP(6)), IMPL(PROP(2), PROP(5)))), REPLACEPROP ( 15, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(PROP(2), PROP(6)), IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 16, PROP(5), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(IMPL(PROP(3), AND(PROP(2), PROP(3))), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(IMPL(PROP(2), IMPL(PROP(3), AND(PROP(2), PROP(3)))), IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))))), REPLACEPROP ( 17, PROP(6), IMPL(PROP(3), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(2), IMPL(PROP(3), AND(PROP(2), PROP(3)))), IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (11, 18) ), LINE ( IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (4, 19) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb16")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(4))), IMPL(PROP(2), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 21, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(1), PROP(4)))), REPLACEPROP ( 22, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(PROP(5), IMPL(PROP(6), PROP(4)))), REPLACEPROP ( 23, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(PROP(5), IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 24, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 25, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(2), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 26, PROP(6), PROP(2) ) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (20, 27) ), LINE ( IMPL(IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(6)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 9, PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 29, PROP(6), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), PROP(5)), IMPL(IMPL(OR(PROP(1), PROP(3)), PROP(6)), IMPL(OR(PROP(1), PROP(3)), PROP(5)))), REPLACEPROP ( 15, PROP(4), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), PROP(6)), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 31, PROP(5), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))) ) ), LINE ( IMPL(IMPL(IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))))), REPLACEPROP ( 32, PROP(6), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3)))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(PROP(2), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3))))))), MODUSPONENS (30, 33) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), OR(PROP(1), AND(PROP(2), PROP(3)))))), MODUSPONENS (28, 34) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(OR(PROP(1), PROP(1)), AND(PROP(2), PROP(3))))), IMPLICATIONEQUIVALENT (35, LINK("hilb14"), LINK("hilb15"), 1) ), LINE ( IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPLICATIONEQUIVALENT (36, LINK("hilb11"), LINK("hilb12"), 1) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), IMPL(PROP(6), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 25, PROP(5), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(3)), IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 38, PROP(6), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (37, 39) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(AND(PROP(1), PROP(2)), PROP(3))), ADDSENTENCE ( LINK ("hilb29")) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(4))), IMPL(AND(PROP(1), PROP(2)), PROP(4))), REPLACEPROP ( 41, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(AND(PROP(1), PROP(5)), PROP(4))), REPLACEPROP ( 42, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(AND(PROP(6), PROP(5)), PROP(4))), REPLACEPROP ( 43, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(AND(PROP(6), PROP(5)), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 44, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(AND(PROP(6), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 45, PROP(5), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(2)), IMPL(OR(PROP(1), PROP(3)), OR(PROP(1), AND(PROP(2), PROP(3))))), IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3))))), REPLACEPROP ( 46, PROP(6), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), MODUSPONENS (40, 47) ) ) ) ), PARAGRAPH ( LABEL ("hilb38"), "A form for the abbreviation rule form for disjunction (first direction):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(2)), NOT(AND(NOT(PROP(1)), NOT(PROP(2))))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(2), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(2), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(PROP(1), PROP(2))))), IMPLICATIONEQUIVALENT (3, LINK("hilb5"), LINK("hilb6"), 5) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2))))), IMPLICATIONEQUIVALENT (4, LINK("hilb5"), LINK("hilb6"), 8) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))))), IMPLICATIONEQUIVALENT (5, LINK("hilb5"), LINK("hilb6"), 11) ), LINE ( IMPL(OR(PROP(1), PROP(2)), NOT(AND(NOT(PROP(1)), NOT(PROP(2))))), REVERSEABBREVIATION (6, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb39"), "A form for the abbreviation rule form for disjunction (second direction):", PROPOSITION ( SENTENCE ( IMPL(NOT(AND(NOT(PROP(1)), NOT(PROP(2)))), OR(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(2), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(2), OR(PROP(1), PROP(2)) ) ), LINE ( IMPL(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(2))), IMPLICATIONEQUIVALENT (3, LINK("hilb5"), LINK("hilb6"), 2) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), OR(PROP(1), PROP(2))), IMPLICATIONEQUIVALENT (4, LINK("hilb5"), LINK("hilb6"), 5) ), LINE ( IMPL(NOT(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), OR(PROP(1), PROP(2))), IMPLICATIONEQUIVALENT (5, LINK("hilb5"), LINK("hilb6"), 8) ), LINE ( IMPL(NOT(AND(NOT(PROP(1)), NOT(PROP(2)))), OR(PROP(1), PROP(2))), REVERSEABBREVIATION (6, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb40"), "By duality we get the second distributive law (first direction):", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), OR(PROP(2), PROP(3))), OR(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), ADDSENTENCE ( LINK ("hilb37")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(1)))), REPLACEPROP ( 2, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(4)))), REPLACEPROP ( 3, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(NOT(OR(PROP(1), AND(PROP(2), PROP(3)))), NOT(PROP(4)))), REPLACEPROP ( 4, PROP(3), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))), OR(PROP(1), AND(PROP(2), PROP(3)))), IMPL(NOT(OR(PROP(1), AND(PROP(2), PROP(3)))), NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))))), REPLACEPROP ( 5, PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(NOT(OR(PROP(1), AND(PROP(2), PROP(3)))), NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), MODUSPONENS (1, 6) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(3)))))), NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))))), IMPLICATIONEQUIVALENT (7, LINK("hilb5"), LINK("hilb6"), 5) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(3)))))), NOT(AND(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(3))))), IMPLICATIONEQUIVALENT (8, LINK("hilb5"), LINK("hilb6"), 12) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(3)))))), NOT(AND(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(3))))))), IMPLICATIONEQUIVALENT (9, LINK("hilb5"), LINK("hilb6"), 17) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(4)))))), NOT(AND(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(4))))))), REPLACEPROP ( 10, PROP(3), PROP(4) ) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(AND(PROP(5), PROP(4)))))), NOT(AND(NOT(NOT(OR(PROP(1), PROP(5)))), NOT(NOT(OR(PROP(1), PROP(4))))))), REPLACEPROP ( 11, PROP(2), PROP(5) ) ), LINE ( IMPL(NOT(OR(PROP(6), NOT(NOT(AND(PROP(5), PROP(4)))))), NOT(AND(NOT(NOT(OR(PROP(6), PROP(5)))), NOT(NOT(OR(PROP(6), PROP(4))))))), REPLACEPROP ( 12, PROP(1), PROP(6) ) ), LINE ( IMPL(NOT(OR(PROP(6), NOT(NOT(AND(PROP(5), NOT(PROP(3))))))), NOT(AND(NOT(NOT(OR(PROP(6), PROP(5)))), NOT(NOT(OR(PROP(6), NOT(PROP(3)))))))), REPLACEPROP ( 13, PROP(4), NOT(PROP(3)) ) ), LINE ( IMPL(NOT(OR(PROP(6), NOT(NOT(AND(NOT(PROP(2)), NOT(PROP(3))))))), NOT(AND(NOT(NOT(OR(PROP(6), NOT(PROP(2))))), NOT(NOT(OR(PROP(6), NOT(PROP(3)))))))), REPLACEPROP ( 14, PROP(5), NOT(PROP(2)) ) ), LINE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(NOT(AND(NOT(PROP(2)), NOT(PROP(3))))))), NOT(AND(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(3)))))))), REPLACEPROP ( 15, PROP(6), NOT(PROP(1)) ) ), LINE ( IMPL(AND(PROP(1), NOT(AND(NOT(PROP(2)), NOT(PROP(3))))), NOT(AND(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(3)))))))), REVERSEABBREVIATION (16, LINK ("and"), 1) ), LINE ( IMPL(AND(PROP(1), OR(PROP(2), PROP(3))), NOT(AND(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(3)))))))), IMPLICATIONEQUIVALENT (17, LINK("hilb39"), LINK("hilb38"), 1) ), LINE ( IMPL(AND(PROP(1), OR(PROP(2), PROP(3))), OR(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), NOT(OR(NOT(PROP(1)), NOT(PROP(3)))))), IMPLICATIONEQUIVALENT (18, LINK("hilb39"), LINK("hilb38"), 1) ), LINE ( IMPL(AND(PROP(1), OR(PROP(2), PROP(3))), OR(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(3)))))), REVERSEABBREVIATION (19, LINK ("and"), 1) ), LINE ( IMPL(AND(PROP(1), OR(PROP(2), PROP(3))), OR(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(3)))), REVERSEABBREVIATION (20, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb41"), "The second distributive law (second direction):", PROPOSITION ( SENTENCE ( IMPL(OR(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(3))), AND(PROP(1), OR(PROP(2), PROP(3)))) ), PROOF ( LINE ( IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb36")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb7")) ), LINE ( IMPL(IMPL(PROP(1), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(1)))), REPLACEPROP ( 2, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(4)))), REPLACEPROP ( 3, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), IMPL(NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), NOT(PROP(4)))), REPLACEPROP ( 4, PROP(3), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(PROP(1), AND(PROP(2), PROP(3))), AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), IMPL(NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), NOT(OR(PROP(1), AND(PROP(2), PROP(3)))))), REPLACEPROP ( 5, PROP(4), OR(PROP(1), AND(PROP(2), PROP(3))) ) ), LINE ( IMPL(NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), NOT(OR(PROP(1), AND(PROP(2), PROP(3))))), MODUSPONENS (1, 6) ), LINE ( IMPL(NOT(AND(OR(PROP(1), PROP(2)), OR(PROP(1), PROP(3)))), NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(3))))))), IMPLICATIONEQUIVALENT (7, LINK("hilb5"), LINK("hilb6"), 13) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(1), PROP(2)))), OR(PROP(1), PROP(3)))), NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(3))))))), IMPLICATIONEQUIVALENT (8, LINK("hilb5"), LINK("hilb6"), 4) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(3)))))), NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(3))))))), IMPLICATIONEQUIVALENT (9, LINK("hilb5"), LINK("hilb6"), 9) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(1), PROP(2)))), NOT(NOT(OR(PROP(1), PROP(4)))))), NOT(OR(PROP(1), NOT(NOT(AND(PROP(2), PROP(4))))))), REPLACEPROP ( 10, PROP(3), PROP(4) ) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(1), PROP(5)))), NOT(NOT(OR(PROP(1), PROP(4)))))), NOT(OR(PROP(1), NOT(NOT(AND(PROP(5), PROP(4))))))), REPLACEPROP ( 11, PROP(2), PROP(5) ) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(6), PROP(5)))), NOT(NOT(OR(PROP(6), PROP(4)))))), NOT(OR(PROP(6), NOT(NOT(AND(PROP(5), PROP(4))))))), REPLACEPROP ( 12, PROP(1), PROP(6) ) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(6), PROP(5)))), NOT(NOT(OR(PROP(6), NOT(PROP(3))))))), NOT(OR(PROP(6), NOT(NOT(AND(PROP(5), NOT(PROP(3)))))))), REPLACEPROP ( 13, PROP(4), NOT(PROP(3)) ) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(PROP(6), NOT(PROP(2))))), NOT(NOT(OR(PROP(6), NOT(PROP(3))))))), NOT(OR(PROP(6), NOT(NOT(AND(NOT(PROP(2)), NOT(PROP(3)))))))), REPLACEPROP ( 14, PROP(5), NOT(PROP(2)) ) ), LINE ( IMPL(NOT(AND(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(3))))))), NOT(OR(NOT(PROP(1)), NOT(NOT(AND(NOT(PROP(2)), NOT(PROP(3)))))))), REPLACEPROP ( 15, PROP(6), NOT(PROP(1)) ) ), LINE ( IMPL(NOT(AND(NOT(AND(PROP(1), PROP(2))), NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(3))))))), NOT(OR(NOT(PROP(1)), NOT(NOT(AND(NOT(PROP(2)), NOT(PROP(3)))))))), REVERSEABBREVIATION (16, LINK ("and"), 1) ), LINE ( IMPL(NOT(AND(NOT(AND(PROP(1), PROP(2))), NOT(AND(PROP(1), PROP(3))))), NOT(OR(NOT(PROP(1)), NOT(NOT(AND(NOT(PROP(2)), NOT(PROP(3)))))))), REVERSEABBREVIATION (17, LINK ("and"), 1) ), LINE ( IMPL(NOT(AND(NOT(AND(PROP(1), PROP(2))), NOT(AND(PROP(1), PROP(3))))), AND(PROP(1), NOT(AND(NOT(PROP(2)), NOT(PROP(3)))))), REVERSEABBREVIATION (18, LINK ("and"), 1) ), LINE ( IMPL(OR(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(3))), AND(PROP(1), NOT(AND(NOT(PROP(2)), NOT(PROP(3)))))), IMPLICATIONEQUIVALENT (19, LINK("hilb39"), LINK("hilb38"), 1) ), LINE ( IMPL(OR(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(3))), AND(PROP(1), OR(PROP(2), PROP(3)))), IMPLICATIONEQUIVALENT (20, LINK("hilb39"), LINK("hilb38"), 1) ) ) ) ) ) )