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)
          )
        )
      )
    )
  )
)