MODULE ( HEADER ( SPEC ( NAME ("prophilbert1"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION ("http://www.qedeq.org/0_00_53") ) ), HEADLINE ("First 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 ("propaxiom"), VERSION ("1.00.00"), VERSION ("1.00.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ), IMPORT ( SPEC ( NAME ("subst"), VERSION ("1.00.00"), VERSION ("1.01.00"), LOCATIONS ( LOCATION ("."), LOCATION ("http://www.qedeq.org/0_00_53") ) ) ) ), USEDBY ( SPEC ( NAME ("prophilbert2"), VERSION ("1.00.00"), VERSION ("1.02.00"), LOCATIONS ( LOCATION (".") ) ) ), PARAGRAPHS ( PARAGRAPH ( LABEL ("rule9"), "Now we could declare the rule {\it Apply Axiom}. \par parameters: \par \begin{tabular}{ll} $p$ & proof line number \\ $\langle$link$\rangle$ & axiom reference \\ \end{tabular} \par If the proof line $n$ has the form \qedeq{p}' and an axiom {\it ref} matches the form \qedeq{IMPL(p, q)}' (p, q be formulas), then the string \qedeq{q}' could be added as a new proof line. \par For example: from proof line \qedeq{OR(r, s)}' we derive \qedeq{OR(r, s)}' by applying axiom 3. \par", DECLARERULE ( "APPLYAXIOM", "Apply Axiom" ) ), PARAGRAPH ( LABEL ("rule10"), "Analogous to the preceding we declare the rule {\it Apply Sentence}.", DECLARERULE ( "APPLYSENTENCE", "Apply Sentence" ) ), PARAGRAPH ( LABEL ("hilb1"), "First we prove a simple implication, that follows directly from the fourth axiom:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))) ), PROOF ( 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(NOT(PROP(3)), PROP(1)), OR(NOT(PROP(3)), PROP(2)))), REPLACEPROP ( 1, PROP(3), NOT(PROP(3)) ) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), OR(NOT(PROP(3)), PROP(2)))), REVERSEABBREVIATION (2, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))), REVERSEABBREVIATION (3, LINK ("impl"), 1) ) ) ), "This proposition is the form for the Hypothetical Syllogism." ), PARAGRAPH ( LABEL ("rule11"), "Now we could declare the rule {\it Hypothetical Syllogism}. \par parameters: \par \begin{tabular}{ll} $p$ & proof line number \\ $m$ & proof line number \\ \end{tabular} \par If the proof line $n$ has the form \qedeq{IMPL(p, q)}'; and the proof line $m$ has the form \qedeq{IMPL(q, r)}' (p, q and r must be formulas), then the string `\qedeq{IMPL(p, s)}' could be added as a new proof line. \par", DECLARERULE ( "HYPOTHETICALSYLLOGISM", "Hypothetical Syllogism", LINK("hilb1") ) ), PARAGRAPH ( LABEL ("hilb2"), "The self implication could be derived:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(1) ) ), LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ), LINE ( IMPL(PROP(1), PROP(1)), HYPOTHETICALSYLLOGISM (2, 3) ) ) ) ), PARAGRAPH ( LABEL ("hilb3"), "One form of the classical {\bf tertium non datur}", PROPOSITION ( SENTENCE ( OR(NOT(PROP(1)), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( OR(NOT(PROP(1)), PROP(1)), USEABBREVIATION (1, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb4"), "The standard form of the excluded middle:", PROPOSITION ( SENTENCE ( OR(PROP(1), NOT(PROP(1))) ), PROOF ( LINE ( OR(NOT(PROP(1)), PROP(1)), ADDSENTENCE ( LINK ("hilb3")) ), LINE ( OR(PROP(1), NOT(PROP(1))), APPLYAXIOM (1, LINK("axiom3")) ) ) ) ), PARAGRAPH ( LABEL ("hilb5"), "Double negation is implicated:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), NOT(NOT(PROP(1)))) ), PROOF ( LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("hilb4")) ), LINE ( OR(NOT(PROP(1)), NOT(NOT(PROP(1)))), REPLACEPROP ( 1, PROP(1), NOT(PROP(1)) ) ), LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), REVERSEABBREVIATION (2, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb6"), "The reverse is also true:", PROPOSITION ( SENTENCE ( IMPL(NOT(NOT(PROP(1))), PROP(1)) ), PROOF ( LINE ( IMPL(PROP(1), NOT(NOT(PROP(1)))), ADDSENTENCE ( LINK ("hilb5")) ), LINE ( IMPL(NOT(PROP(1)), NOT(NOT(NOT(PROP(1))))), REPLACEPROP ( 1, PROP(1), NOT(PROP(1)) ) ), LINE ( IMPL(OR(PROP(1), NOT(PROP(1))), OR(PROP(1), NOT(NOT(NOT(PROP(1)))))), APPLYAXIOM (2, LINK("axiom4")) ), LINE ( OR(PROP(1), NOT(PROP(1))), ADDSENTENCE ( LINK ("hilb4")) ), LINE ( OR(PROP(1), NOT(NOT(NOT(PROP(1))))), MODUSPONENS (4, 3) ), LINE ( OR(NOT(NOT(NOT(PROP(1)))), PROP(1)), APPLYAXIOM (5, LINK("axiom3")) ), LINE ( IMPL(NOT(NOT(PROP(1))), PROP(1)), REVERSEABBREVIATION (6, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb7"), "The correct reverse of an implication:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))) ), 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)), PROP(2)), OR(NOT(PROP(1)), NOT(NOT(PROP(2))))), APPLYAXIOM (2, LINK("axiom4")) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(NOT(PROP(1)), NOT(NOT(PROP(2)))), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), SUBSTLINE (4) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), HYPOTHETICALSYLLOGISM (3, 5) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(NOT(PROP(2))), NOT(PROP(1)))), REVERSEABBREVIATION (6, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(NOT(PROP(2)), NOT(PROP(1)))), REVERSEABBREVIATION (7, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("rule12"), DECLARERULE ( "REVERSEIMPLICATION", "Correct reverse of an implication", LINK( "hilb7") ) ), PARAGRAPH ( LABEL ("rule13"), DECLARERULE ( "LEFTADDITION", "Add a Conjunction on the Left", LINK ("axiom4") ) ), PARAGRAPH ( LABEL ("rule14"), DECLARERULE ( "RIGHTADDITION", "Add a Conjunction on the Right", LINK("axiom3"), LINK("axiom4") ) ), PARAGRAPH ( LABEL ("defimpl1"), "Definition of an Implication 1. part:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(2))), SUBSTLINE (1) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), OR(NOT(PROP(1)), PROP(2))), USEABBREVIATION (2, LINK ("impl"), 3) ) ) ) ), PARAGRAPH ( LABEL ("defimpl2"), "Definition of an Implication 2. part:", PROPOSITION ( SENTENCE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(2))), SUBSTLINE (1) ), LINE ( IMPL(OR(NOT(PROP(1)), PROP(2)), IMPL(PROP(1), PROP(2))), USEABBREVIATION (2, LINK ("impl"), 2) ) ) ) ), PARAGRAPH ( LABEL ("rule17"), DECLARERULE ( "RIGHTADDITIONIMPLICATION", "Addition of an Implication on the Right", LINK("defimpl1"), LINK("defimpl2") ) ), PARAGRAPH ( LABEL ("rule18"), DECLARERULE ( "LEFTADDITIONIMPLICATION", "Addition of an Implication on the Left", LINK("defimpl1"), LINK("defimpl2") ) ), PARAGRAPH ( LABEL ("defand1"), "Definition of a Conjunction 1. part:", PROPOSITION ( SENTENCE ( IMPL(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(2))), SUBSTLINE (1) ), LINE ( IMPL(AND(PROP(1), PROP(2)), NOT(OR(NOT(PROP(1)), NOT(PROP(2))))), USEABBREVIATION (2, LINK ("and"), 2) ) ) ) ), PARAGRAPH ( LABEL ("defand2"), "Definition of a Conjunction 2. part:", PROPOSITION ( SENTENCE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), AND(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(AND(PROP(1), PROP(2)), AND(PROP(1), PROP(2))), SUBSTLINE (1) ), LINE ( IMPL(NOT(OR(NOT(PROP(1)), NOT(PROP(2)))), AND(PROP(1), PROP(2))), USEABBREVIATION (2, LINK ("and"), 1) ) ) ) ), PARAGRAPH ( LABEL ("rule19"), DECLARERULE ( "LEFTADDITIONCONJUNCTION", "Addition of a Conjunction on the Left", LINK("defand1"), LINK("defand2") ) ), PARAGRAPH ( LABEL ("rule20"), DECLARERULE( "RIGHTADDITIONCONJUNCTION", "Addition of a Conjunction on the Right", LINK("defand1"), LINK("defand2") ) ), PARAGRAPH ( LABEL ("defequi1"), "Definition of an Equivalence 1. part:", PROPOSITION ( SENTENCE ( IMPL ( EQUI (PROP(1), PROP(2)), AND ( IMPL (PROP(1), PROP(2)), IMPL (PROP(2), PROP(1)) ) ) ), PROOF ( LINE ( IMPL (PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL (EQUI(PROP(1), PROP(2)), EQUI(PROP(1), PROP(2))), SUBSTLINE (1) ), LINE ( IMPL( EQUI (PROP(1), PROP(2)), AND ( IMPL (PROP(1), PROP(2)), IMPL (PROP(2), PROP(1)) ) ), USEABBREVIATION (2, LINK ("equi"), 2) ) ) ) ), PARAGRAPH ( LABEL ("defequi2"), "Definition of an Equivalence 2. part:", PROPOSITION ( SENTENCE ( IMPL ( AND ( IMPL (PROP(1), PROP(2)), IMPL (PROP(2), PROP(1)) ), EQUI (PROP(1), PROP(2)) ) ), PROOF ( LINE ( IMPL (PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL (EQUI(PROP(1), PROP(2)), EQUI(PROP(1), PROP(2))), SUBSTLINE (1) ), LINE ( IMPL ( AND ( IMPL (PROP(1), PROP(2)), IMPL (PROP(2), PROP(1)) ), EQUI (PROP(1), PROP(2)) ), USEABBREVIATION (2, LINK ("equi"), 1) ) ) ) ), PARAGRAPH ( LABEL ("rule21"), DECLARERULE ( "LEFTADDITIONEQUIVALENCE", "Addition of an Equivalence on the Left", LINK("defequi1"), LINK("defequi2") ) ), PARAGRAPH ( LABEL ("rule22"), DECLARERULE ( "RIGHTADDITIONEQUIVALENCE", "Addition of an Equivalence on the Right", LINK("defequi1"), LINK("defequi2") ) ), PARAGRAPH ( LABEL ("rule30"), DECLARERULE ( "IMPLICATIONEQUIVALENT", "Elementary equivalence of two formulas" ) ), PARAGRAPH ( LABEL ("hilb8"), "A simular formulation for the second axiom:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), OR(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), HYPOTHETICALSYLLOGISM (1, 2) ) ) ) ), PARAGRAPH ( LABEL ("hilb9"), "A technical lemma (equal to the third axiom):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ) ) ) ), PARAGRAPH ( LABEL ("hilb10"), "And another technical lemma (simular to the third axiom):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(2)), OR(PROP(2), PROP(1))), ADDAXIOM ( LINK ("axiom3")) ), LINE ( IMPL(OR(PROP(2), PROP(1)), OR(PROP(1), PROP(2))), SUBSTLINE (1) ) ) ) ), PARAGRAPH ( LABEL ("hilb11"), "A technical lemma (equal to the first axiom):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)) ), PROOF ( LINE ( IMPL(OR(PROP(1), PROP(1)), PROP(1)), ADDAXIOM ( LINK ("axiom1")) ) ) ) ), PARAGRAPH ( LABEL ("hilb12"), "A simple propositon that follows directly from the second axiom:", PROPOSITION ( SENTENCE ( IMPL(PROP(1), OR(PROP(1), PROP(1))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(1))), REPLACEPROP ( 1, PROP(2), PROP(1) ) ) ) ) ), PARAGRAPH ( LABEL ("hilb13"), "This is a pre form for the associative law:", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(PROP(1), OR(PROP(2), PROP(1))), ADDSENTENCE ( LINK ("hilb8")) ), LINE ( IMPL(PROP(3), OR(PROP(1), PROP(3))), SUBSTLINE (1) ), LINE ( IMPL(OR(PROP(2), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3)))), APPLYAXIOM (2, LINK("axiom4")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3))))), APPLYAXIOM (3, LINK("axiom4")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1))), IMPLICATIONEQUIVALENT (4, LINK("hilb9"), LINK("hilb10"), 3) ), LINE ( IMPL(OR(PROP(1), PROP(3)), OR(PROP(2), OR(PROP(1), PROP(3)))), REPLACEPROP ( 1, PROP(1), OR(PROP(1), PROP(3)) ) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(2))), ADDAXIOM ( LINK ("axiom2")) ), LINE ( IMPL(PROP(1), OR(PROP(1), PROP(3))), REPLACEPROP ( 7, PROP(2), PROP(3) ) ), LINE ( IMPL(PROP(1), OR(PROP(2), OR(PROP(1), PROP(3)))), HYPOTHETICALSYLLOGISM (8, 6) ), LINE ( IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(OR(PROP(2), OR(PROP(1), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3))))), APPLYAXIOM (9, LINK("axiom4")) ), LINE ( IMPL(OR(OR(PROP(2), OR(PROP(1), PROP(3))), PROP(1)), OR(PROP(2), OR(PROP(1), PROP(3)))), IMPLICATIONEQUIVALENT (10, LINK("hilb11"), LINK("hilb12"), 1) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), HYPOTHETICALSYLLOGISM (5, 11) ) ) ) ), PARAGRAPH ( LABEL ("hilb14"), "The associative law for the disjunction (first direction):", PROPOSITION ( SENTENCE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))) ), PROOF ( LINE ( IMPL(PROP(1), PROP(1)), ADDSENTENCE ( LINK ("hilb2")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(2), PROP(3)))), SUBSTLINE (1) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPLICATIONEQUIVALENT (2, LINK("hilb9"), LINK("hilb10"), 4) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb13")) ), LINE ( IMPL(OR(PROP(1), OR(PROP(3), PROP(2))), OR(PROP(3), OR(PROP(1), PROP(2)))), SUBSTLINE (4) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(3), OR(PROP(1), PROP(2)))), HYPOTHETICALSYLLOGISM (3, 5) ), LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(OR(PROP(1), PROP(2)), PROP(3))), IMPLICATIONEQUIVALENT (6, LINK("hilb9"), LINK("hilb10"), 3) ) ) ) ), PARAGRAPH ( LABEL ("hilb15"), "The associative law for the disjunction (second direction):", PROPOSITION ( SENTENCE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(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(OR(PROP(3), OR(PROP(2), PROP(1))), OR(OR(PROP(3), PROP(2)), PROP(1))), SUBSTLINE (1) ), LINE ( IMPL(OR(OR(PROP(2), PROP(1)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPLICATIONEQUIVALENT (2, LINK("hilb9"), LINK("hilb10"), 1) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(OR(PROP(3), PROP(2)), PROP(1))), IMPLICATIONEQUIVALENT (3, LINK("hilb9"), LINK("hilb10"), 2) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(3), PROP(2)))), IMPLICATIONEQUIVALENT (4, LINK("hilb9"), LINK("hilb10"), 3) ), LINE ( IMPL(OR(OR(PROP(1), PROP(2)), PROP(3)), OR(PROP(1), OR(PROP(2), PROP(3)))), IMPLICATIONEQUIVALENT (5, LINK("hilb9"), LINK("hilb10"), 4) ) ) ) ), PARAGRAPH ( LABEL ("hilb16"), "Another consequence from hilb13 is the exchange of preconditions:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))) ), PROOF ( LINE ( IMPL(OR(PROP(1), OR(PROP(2), PROP(3))), OR(PROP(2), OR(PROP(1), PROP(3)))), ADDSENTENCE ( LINK ("hilb13")) ), LINE ( IMPL(OR(NOT(PROP(1)), OR(NOT(PROP(2)), PROP(3))), OR(NOT(PROP(2)), OR(NOT(PROP(1)), PROP(3)))), SUBSTLINE (1) ), LINE ( IMPL(IMPL(PROP(1), OR(NOT(PROP(2)), PROP(3))), OR(NOT(PROP(2)), OR(NOT(PROP(1)), PROP(3)))), REVERSEABBREVIATION (2, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), OR(NOT(PROP(2)), OR(NOT(PROP(1)), PROP(3)))), REVERSEABBREVIATION (3, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), OR(NOT(PROP(1)), PROP(3)))), REVERSEABBREVIATION (4, LINK ("impl"), 1) ), LINE ( IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(PROP(2), IMPL(PROP(1), PROP(3)))), REVERSEABBREVIATION (5, LINK ("impl"), 1) ) ) ) ), PARAGRAPH ( LABEL ("hilb17"), "An analogus form for \hyperref[hilb16]{hilb16}:", PROPOSITION ( SENTENCE ( IMPL(IMPL(PROP(2), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))) ), PROOF ( 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(2), IMPL(PROP(1), PROP(3))), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), SUBSTLINE (1) ) ) ) ) ) )