MODULE ( HEADER ( SPEC ( NAME ("prophilbert2"), 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 ("prophilbert1"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ) ), USEDBY ( SPEC ( NAME ("prophilbert3"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION (".") ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("hilb18"), "Negation of a conjunction:", PROPOSITION ( SENTENCE ( IMPL(NOT(AND(PROP(1), PROP(2))), OR(NOT(PROP(1)), NOT(PROP(2)))) ), PROOF ( LINE ( IMPL(NOT(NOT(PROP(1))), PROP(1)), ADDSENTENCE ( LINK ("hilb6")) ), LINE ( IMPL(NOT(NOT(PROP(2))), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), OR(NOT(PROP(1)), NOT(PROP(2)))), REPLACEPROP ( 2, PROP(2), OR(NOT(PROP(1)), NOT(PROP(2))) ) ), LINE ( IMPL(NOT(AND(PROP(1), PROP(2))), OR(NOT(PROP(1)), NOT(PROP(2)))), REVERSEABBREVIATION (3, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb19"), "The reverse of a negation of a conjunction:", PROPOSITION ( SENTENCE ( IMPL(OR(NOT(PROP(1)), NOT(PROP(2))), NOT(AND(PROP(1), PROP(2)))) ), PROOF ( LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb5")) ), LINE ( IMPL(PROP(2), NOT(NOT(PROP(2)))), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(OR(NOT(PROP(1)), NOT(PROP(2))), NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))))), REPLACEPROP ( 2, PROP(2), OR(NOT(PROP(1)), NOT(PROP(2))) ) ), LINE ( IMPL(OR(NOT(PROP(1)), NOT(PROP(2))), NOT(AND(PROP(1), PROP(2)))), REVERSEABBREVIATION (3, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb20"), "Negation of a disjunction:", PROPOSITION ( SENTENCE ( IMPL(NOT(OR(PROP(1), PROP(2))), 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(NOT(OR(PROP(1), PROP(2))), NOT(OR(PROP(1), PROP(2)))), REPLACEPROP ( 2, PROP(2), NOT(OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(NOT(OR(PROP(1), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), PROP(2)))), IMPLICATIONEQUIVALENT (3, LINK("hilb5"), LINK("hilb6"), 8) ), LINE ( IMPL(NOT(OR(PROP(1), PROP(2))), NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2)))))), IMPLICATIONEQUIVALENT (4, LINK("hilb5"), LINK("hilb6"), 11) ), LINE ( IMPL(NOT(OR(PROP(1), PROP(2))), AND(NOT(PROP(1)), NOT(PROP(2)))), REVERSEABBREVIATION (5, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb21"), "Reverse of a negation of a disjunction:", PROPOSITION ( SENTENCE ( IMPL(AND(NOT(PROP(1)), NOT(PROP(2))), NOT(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(NOT(OR(PROP(1), PROP(2))), NOT(OR(PROP(1), PROP(2)))), REPLACEPROP ( 2, PROP(2), NOT(OR(PROP(1), PROP(2))) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(PROP(1))), PROP(2))), NOT(OR(PROP(1), PROP(2)))), IMPLICATIONEQUIVALENT (3, LINK("hilb5"), LINK("hilb6"), 4) ), LINE ( IMPL(NOT(OR(NOT(NOT(PROP(1))), NOT(NOT(PROP(2))))), NOT(OR(PROP(1), PROP(2)))), IMPLICATIONEQUIVALENT (4, LINK("hilb5"), LINK("hilb6"), 7) ), LINE ( IMPL(AND(NOT(PROP(1)), NOT(PROP(2))), NOT(OR(PROP(1), PROP(2)))), REVERSEABBREVIATION (5, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb22"), "The Conjunction is commutative:", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(2), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(2))), REPLACEPROP ( 2, PROP(2), AND(PROP(1), PROP(2)) ) ), LINE ( IMPL(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), USEABBREVIATION (3, LINK ("and"), 2) ), LINE ( IMPL(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(2)), NOT(PROP(1))))), IMPLICATIONEQUIVALENT (4, LINK("hilb9"), LINK("hilb10"), 1) ), LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(2), PROP(1))), REVERSEABBREVIATION (5, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb23"), "A technical lemma that is simular to the previous one:", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(2), PROP(1)), AND(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("hilb22")) ), LINE ( IMPL(AND(PROP(1), PROP(3)), AND(PROP(3), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(AND(PROP(4), PROP(3)), AND(PROP(3), PROP(4))), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(AND(PROP(4), PROP(1)), AND(PROP(1), PROP(4))), REPLACEPROP ( 3, PROP(3), PROP(1) ) ), LINE ( IMPL(AND(PROP(2), PROP(1)), AND(PROP(1), PROP(2))), REPLACEPROP ( 4, PROP(4), PROP(2) ) ) ) ) ), PARAGRAPH ( LABEL ("hilb24"), "Reduction of a conjunction:", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), PROP(2)), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(3))), REPLACEPROP ( 1, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(4), OR(PROP(4), PROP(3))), REPLACEPROP ( 2, PROP(1), PROP(4) ) ), LINE ( IMPL(PROP(4), OR(PROP(4), NOT(PROP(2)))), REPLACEPROP ( 3, PROP(3), NOT(PROP(2)) ) ), LINE ( IMPL(NOT(PROP(1)), OR(NOT(PROP(1)), NOT(PROP(2)))), REPLACEPROP ( 4, PROP(4), NOT(PROP(1)) ) ), 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 ( 6, PROP(2), PROP(3) ) ), LINE ( IMPL(IMPL(PROP(4), PROP(3)), IMPL(NOT(PROP(3)), NOT(PROP(4)))), REPLACEPROP ( 7, PROP(1), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(4), OR(NOT(PROP(1)), NOT(PROP(2)))), IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), NOT(PROP(4)))), REPLACEPROP ( 8, PROP(3), OR(NOT(PROP(1)), NOT(PROP(2))) ) ), LINE ( IMPL(IMPL(NOT(PROP(1)), OR(NOT(PROP(1)), NOT(PROP(2)))), IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), NOT(NOT(PROP(1))))), REPLACEPROP ( 9, PROP(4), NOT(PROP(1)) ) ), LINE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), NOT(NOT(PROP(1)))), MODUSPONENS (5, 10) ), LINE ( IMPL(AND(PROP(1), PROP(2)), NOT(NOT(PROP(1)))), REVERSEABBREVIATION (11, LINK ("and"), 1) ), LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(1)), IMPLICATIONEQUIVALENT (12, LINK("hilb6"), LINK("hilb5"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb25"), "Another form of a reduction of a conjunction:", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), PROP(2)), PROP(2)) ), 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(4), PROP(1)), PROP(4)), REPLACEPROP ( 3, PROP(3), PROP(1) ) ), LINE ( IMPL(AND(PROP(2), PROP(1)), PROP(2)), REPLACEPROP ( 4, PROP(4), PROP(2) ) ), LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(2)), IMPLICATIONEQUIVALENT (5, LINK("hilb22"), LINK("hilb23"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb26"), "The conjunction is associative too (first implication):", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), AND(PROP(2), PROP(3))), AND(AND(PROP(1), PROP(2)), PROP(3))) ), PROOF ( LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))), ADDSENTENCE ( LINK ("hilb15")) ), 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), OR(PROP(2), PROP(3)))), IMPL(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), NOT(PROP(4)))), REPLACEPROP ( 4, PROP(3), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPL(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), NOT(OR(OR(PROP(1), PROP(2)), PROP(3))))), REPLACEPROP ( 5, PROP(4), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(NOT(OR(PROP(1), OR(PROP(2), PROP(3)))), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), MODUSPONENS (1, 6) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(OR(PROP(2), PROP(3)))))), NOT(OR(OR(PROP(1), PROP(2)), PROP(3)))), IMPLICATIONEQUIVALENT (7, LINK("hilb5"), LINK("hilb6"), 5) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(OR(PROP(2), PROP(3)))))), NOT(OR(NOT(NOT(OR(PROP(1), PROP(2)))), PROP(3)))), IMPLICATIONEQUIVALENT (8, LINK("hilb5"), LINK("hilb6"), 12) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(OR(PROP(2), PROP(4)))))), NOT(OR(NOT(NOT(OR(PROP(1), PROP(2)))), PROP(4)))), REPLACEPROP ( 9, PROP(3), PROP(4) ) ), LINE ( IMPL(NOT(OR(PROP(1), NOT(NOT(OR(PROP(5), PROP(4)))))), NOT(OR(NOT(NOT(OR(PROP(1), PROP(5)))), PROP(4)))), REPLACEPROP ( 10, PROP(2), PROP(5) ) ), LINE ( IMPL(NOT(OR(PROP(6), NOT(NOT(OR(PROP(5), PROP(4)))))), NOT(OR(NOT(NOT(OR(PROP(6), PROP(5)))), PROP(4)))), REPLACEPROP ( 11, PROP(1), PROP(6) ) ), LINE ( IMPL(NOT(OR(PROP(6), NOT(NOT(OR(PROP(5), NOT(PROP(3))))))), NOT(OR(NOT(NOT(OR(PROP(6), PROP(5)))), NOT(PROP(3))))), REPLACEPROP ( 12, PROP(4), NOT(PROP(3)) ) ), LINE ( IMPL(NOT(OR(PROP(6), NOT(NOT(OR(NOT(PROP(2)), NOT(PROP(3))))))), NOT(OR(NOT(NOT(OR(PROP(6), NOT(PROP(2))))), NOT(PROP(3))))), REPLACEPROP ( 13, PROP(5), NOT(PROP(2)) ) ), LINE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(NOT(OR(NOT(PROP(2)), NOT(PROP(3))))))), NOT(OR(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(PROP(3))))), REPLACEPROP ( 14, PROP(6), NOT(PROP(1)) ) ), LINE ( IMPL(AND(PROP(1), NOT(OR(NOT(PROP(2)), NOT(PROP(3))))), NOT(OR(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(PROP(3))))), REVERSEABBREVIATION (15, LINK ("and"), 1) ), LINE ( IMPL(AND(PROP(1), AND(PROP(2), PROP(3))), NOT(OR(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(PROP(3))))), REVERSEABBREVIATION (16, LINK ("and"), 1) ), LINE ( IMPL(AND(PROP(1), AND(PROP(2), PROP(3))), AND(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), PROP(3))), REVERSEABBREVIATION (17, LINK ("and"), 1) ), LINE ( IMPL(AND(PROP(1), AND(PROP(2), PROP(3))), AND(AND(PROP(1), PROP(2)), PROP(3))), REVERSEABBREVIATION (18, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb27"), "The conjunction is associative (second implication):", PROPOSITION ( SENTENCE ( IMPL(AND(AND(PROP(1), PROP(2)), PROP(3)), AND(PROP(1), AND(PROP(2), PROP(3)))) ), PROOF ( LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))), ADDSENTENCE ( LINK ("hilb14")) ), 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(OR(PROP(1), PROP(2)), PROP(3))), IMPL(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), NOT(PROP(4)))), REPLACEPROP ( 4, PROP(3), OR(OR(PROP(1), PROP(2)), PROP(3)) ) ), LINE ( IMPL(IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPL(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), NOT(OR(PROP(1), OR(PROP(2), PROP(3)))))), REPLACEPROP ( 5, PROP(4), OR(PROP(1), OR(PROP(2), PROP(3))) ) ), LINE ( IMPL(NOT(OR(OR(PROP(1), PROP(2)), PROP(3))), NOT(OR(PROP(1), OR(PROP(2), PROP(3))))), MODUSPONENS (1, 6) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(1), PROP(2)))), PROP(3))), NOT(OR(PROP(1), OR(PROP(2), PROP(3))))), IMPLICATIONEQUIVALENT (7, LINK("hilb5"), LINK("hilb6"), 4) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(1), PROP(2)))), PROP(3))), NOT(OR(PROP(1), NOT(NOT(OR(PROP(2), PROP(3))))))), IMPLICATIONEQUIVALENT (8, LINK("hilb5"), LINK("hilb6"), 13) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(1), PROP(2)))), PROP(4))), NOT(OR(PROP(1), NOT(NOT(OR(PROP(2), PROP(4))))))), REPLACEPROP ( 9, PROP(3), PROP(4) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(1), PROP(5)))), PROP(4))), NOT(OR(PROP(1), NOT(NOT(OR(PROP(5), PROP(4))))))), REPLACEPROP ( 10, PROP(2), PROP(5) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(6), PROP(5)))), PROP(4))), NOT(OR(PROP(6), NOT(NOT(OR(PROP(5), PROP(4))))))), REPLACEPROP ( 11, PROP(1), PROP(6) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(6), PROP(5)))), NOT(PROP(3)))), NOT(OR(PROP(6), NOT(NOT(OR(PROP(5), NOT(PROP(3)))))))), REPLACEPROP ( 12, PROP(4), NOT(PROP(3)) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(PROP(6), NOT(PROP(2))))), NOT(PROP(3)))), NOT(OR(PROP(6), NOT(NOT(OR(NOT(PROP(2)), NOT(PROP(3)))))))), REPLACEPROP ( 13, PROP(5), NOT(PROP(2)) ) ), LINE ( IMPL(NOT(OR(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), NOT(PROP(3)))), NOT(OR(NOT(PROP(1)), NOT(NOT(OR(NOT(PROP(2)), NOT(PROP(3)))))))), REPLACEPROP ( 14, PROP(6), NOT(PROP(1)) ) ), LINE ( IMPL(AND(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), PROP(3)), NOT(OR(NOT(PROP(1)), NOT(NOT(OR(NOT(PROP(2)), NOT(PROP(3)))))))), REVERSEABBREVIATION (15, LINK ("and"), 1) ), LINE ( IMPL(AND(AND(PROP(1), PROP(2)), PROP(3)), NOT(OR(NOT(PROP(1)), NOT(NOT(OR(NOT(PROP(2)), NOT(PROP(3)))))))), REVERSEABBREVIATION (16, LINK ("and"), 1) ), LINE ( IMPL(AND(AND(PROP(1), PROP(2)), PROP(3)), AND(PROP(1), NOT(OR(NOT(PROP(2)), NOT(PROP(3)))))), REVERSEABBREVIATION (17, LINK ("and"), 1) ), LINE ( IMPL(AND(AND(PROP(1), PROP(2)), PROP(3)), AND(PROP(1), AND(PROP(2), PROP(3)))), REVERSEABBREVIATION (18, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb28"), "Form for the conjunction rule:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), IMPL(PROP(2), AND(PROP(1), PROP(2)))) ), PROOF ( LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("hilb4")) ), LINE ( OR(OR(NOT(PROP(1)), NOT(PROP(2))), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), REPLACEPROP ( 1, PROP(1), OR(NOT(PROP(1)), NOT(PROP(2))) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))), ADDSENTENCE ( LINK ("hilb15")) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(4)), OR(PROP(1), OR(PROP(2), PROP(4)))), REPLACEPROP ( 3, PROP(3), PROP(4) ) ), LINE ( IMPL(OR(OR(PROP(1), PROP(5)), PROP(4)), OR(PROP(1), OR(PROP(5), PROP(4)))), REPLACEPROP ( 4, PROP(2), PROP(5) ) ), LINE ( IMPL(OR(OR(PROP(6), PROP(5)), PROP(4)), OR(PROP(6), OR(PROP(5), PROP(4)))), REPLACEPROP ( 5, PROP(1), PROP(6) ) ), LINE ( IMPL(OR(OR(PROP(6), PROP(5)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), OR(PROP(6), OR(PROP(5), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))))), REPLACEPROP ( 6, PROP(4), NOT(OR(NOT(PROP(1)), NOT(PROP(2)))) ) ), LINE ( IMPL(OR(OR(PROP(6), NOT(PROP(2))), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), OR(PROP(6), OR(NOT(PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))))), REPLACEPROP ( 7, PROP(5), NOT(PROP(2)) ) ), LINE ( IMPL(OR(OR(NOT(PROP(1)), NOT(PROP(2))), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), OR(NOT(PROP(1)), OR(NOT(PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))))), REPLACEPROP ( 8, PROP(6), NOT(PROP(1)) ) ), LINE ( OR(NOT(PROP(1)), OR(NOT(PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2)))))), MODUSPONENS (2, 9) ), LINE ( IMPL(PROP(1), OR(NOT(PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2)))))), REVERSEABBREVIATION (10, LINK ("impl"), 1) ), LINE ( IMPL(PROP(1), IMPL(PROP(2), NOT(OR(NOT(PROP(1)), NOT(PROP(2)))))), REVERSEABBREVIATION (11, LINK ("impl"), 1) ), LINE ( IMPL(PROP(1), IMPL(PROP(2), AND(PROP(1), PROP(2)))), REVERSEABBREVIATION (12, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb29"), "Preconditions could be put together in a conjunction (first direction):", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(AND(PROP(1), PROP(2)), PROP(3))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(2), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), REPLACEPROP ( 2, PROP(2), IMPL(PROP(1), IMPL(PROP(2), PROP(3))) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), OR(NOT(PROP(1)), IMPL(PROP(2), PROP(3)))), USEABBREVIATION (3, LINK ("impl"), 4) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), OR(NOT(PROP(1)), OR(NOT(PROP(2)), PROP(3)))), USEABBREVIATION (4, LINK ("impl"), 4) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), OR(OR(NOT(PROP(1)), NOT(PROP(2))), PROP(3))), IMPLICATIONEQUIVALENT (5, LINK("hilb14"), LINK("hilb15"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), OR(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), PROP(3))), IMPLICATIONEQUIVALENT (6, LINK("hilb5"), LINK("hilb6"), 8) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), PROP(3))), REVERSEABBREVIATION (7, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(AND(PROP(1), PROP(2)), PROP(3))), REVERSEABBREVIATION (8, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb30"), "Preconditions could be put together in a conjunction (second direction):", PROPOSITION ( SENTENCE ( IMPL(IMPL(AND(PROP(1), PROP(2)), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(PROP(2), PROP(2)), REPLACEPROP ( 1, PROP(1), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), REPLACEPROP ( 2, PROP(2), IMPL(PROP(1), IMPL(PROP(2), PROP(3))) ) ), LINE ( IMPL(OR(NOT(PROP(1)), IMPL(PROP(2), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), USEABBREVIATION (3, LINK ("impl"), 2) ), LINE ( IMPL(OR(NOT(PROP(1)), OR(NOT(PROP(2)), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), USEABBREVIATION (4, LINK ("impl"), 2) ), LINE ( IMPL(OR(OR(NOT(PROP(1)), NOT(PROP(2))), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), IMPLICATIONEQUIVALENT (5, LINK("hilb14"), LINK("hilb15"), 1) ), LINE ( IMPL(OR(NOT(NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), IMPLICATIONEQUIVALENT (6, LINK("hilb5"), LINK("hilb6"), 3) ), LINE ( IMPL(IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), REVERSEABBREVIATION (7, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(AND(PROP(1), PROP(2)), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), REVERSEABBREVIATION (8, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb31"), "Absorbtion of a conjunction (first direction):", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), PROP(1)), PROP(1)) ), PROOF ( LINE ( IMPL(AND(PROP(1), PROP(2)), PROP(1)), ADDSENTENCE ( LINK ("hilb24")) ), LINE ( IMPL(AND(PROP(1), PROP(1)), PROP(1)), REPLACEPROP ( 1, PROP(2), PROP(1) ) ) ) ) ), PARAGRAPH ( LABEL ("hilb32"), "Absorbtion of a conjunction (second direction):", PROPOSITION ( SENTENCE ( IMPL(PROP(1), AND(PROP(1), PROP(1))) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("hilb11")) ), 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), PROP(1)), IMPL(NOT(PROP(1)), NOT(PROP(4)))), REPLACEPROP ( 4, PROP(3), PROP(1) ) ), LINE ( IMPL(IMPL(OR(PROP(1), PROP(1)), PROP(1)), IMPL(NOT(PROP(1)), NOT(OR(PROP(1), PROP(1))))), REPLACEPROP ( 5, PROP(4), OR(PROP(1), PROP(1)) ) ), LINE ( IMPL(NOT(PROP(1)), NOT(OR(PROP(1), PROP(1)))), MODUSPONENS (1, 6) ), LINE ( IMPL(NOT(PROP(2)), NOT(OR(PROP(2), PROP(2)))), REPLACEPROP ( 7, PROP(1), PROP(2) ) ), LINE ( IMPL(NOT(NOT(PROP(1))), NOT(OR(NOT(PROP(1)), NOT(PROP(1))))), REPLACEPROP ( 8, PROP(2), NOT(PROP(1)) ) ), LINE ( IMPL(PROP(1), NOT(OR(NOT(PROP(1)), NOT(PROP(1))))), IMPLICATIONEQUIVALENT (9, LINK("hilb6"), LINK("hilb5"), 1) ), LINE ( IMPL(PROP(1), AND(PROP(1), PROP(1))), REVERSEABBREVIATION (10, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb33"), "Absorbtion of identical preconditions (first direction):", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(2))), IMPL(PROP(1), PROP(2))) ), PROOF ( 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 ( 1, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(5), PROP(4))), IMPL(AND(PROP(1), PROP(5)), PROP(4))), REPLACEPROP ( 2, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(4))), IMPL(AND(PROP(6), PROP(5)), PROP(4))), REPLACEPROP ( 3, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(5), PROP(2))), IMPL(AND(PROP(6), PROP(5)), PROP(2))), REPLACEPROP ( 4, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(PROP(6), IMPL(PROP(1), PROP(2))), IMPL(AND(PROP(6), PROP(1)), PROP(2))), REPLACEPROP ( 5, PROP(5), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(2))), IMPL(AND(PROP(1), PROP(1)), PROP(2))), REPLACEPROP ( 6, PROP(6), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(2))), IMPL(PROP(1), PROP(2))), IMPLICATIONEQUIVALENT (7, LINK("hilb31"), LINK("hilb32"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb34"), "Absorbtion of identical preconditions (second direction):", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), IMPL(PROP(1), PROP(2)))) ), PROOF ( LINE ( IMPL(IMPL(AND(PROP(1), PROP(2)), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), ADDSENTENCE ( LINK ("hilb30")) ), LINE ( IMPL(IMPL(AND(PROP(1), PROP(2)), PROP(4)), IMPL(PROP(1), IMPL(PROP(2), PROP(4)))), REPLACEPROP ( 1, PROP(3), PROP(4) ) ), LINE ( IMPL(IMPL(AND(PROP(1), PROP(5)), PROP(4)), IMPL(PROP(1), IMPL(PROP(5), PROP(4)))), REPLACEPROP ( 2, PROP(2), PROP(5) ) ), LINE ( IMPL(IMPL(AND(PROP(6), PROP(5)), PROP(4)), IMPL(PROP(6), IMPL(PROP(5), PROP(4)))), REPLACEPROP ( 3, PROP(1), PROP(6) ) ), LINE ( IMPL(IMPL(AND(PROP(6), PROP(5)), PROP(2)), IMPL(PROP(6), IMPL(PROP(5), PROP(2)))), REPLACEPROP ( 4, PROP(4), PROP(2) ) ), LINE ( IMPL(IMPL(AND(PROP(6), PROP(1)), PROP(2)), IMPL(PROP(6), IMPL(PROP(1), PROP(2)))), REPLACEPROP ( 5, PROP(5), PROP(1) ) ), LINE ( IMPL(IMPL(AND(PROP(1), PROP(1)), PROP(2)), IMPL(PROP(1), IMPL(PROP(1), PROP(2)))), REPLACEPROP ( 6, PROP(6), PROP(1) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), IMPL(PROP(1), PROP(2)))), IMPLICATIONEQUIVALENT (7, LINK("hilb31"), LINK("hilb32"), 1) ) ) ) ) ) )