MODULE (
  HEADER (
    SPEC (
      NAME ("luktheo1"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    HEADLINE ("First theorems of Propositional Calculus"),
    DESCRIPTION (
      "This module includes first proofs of propositional calculus theorems."
    ),
    EMAIL ("module@qedeq.org"),
    AUTHORS (
      AUTHOR ("Franz Fritsche",EMAIL ("ff@qedeq.org")),
      AUTHOR ("Michael Meyling",EMAIL ("mime@qedeq.org"))
    )
  ),
  IMPORTS (
    IMPORT (
      SPEC (
        NAME ("lukaxiom"),
        VERSION ("1.00.00"),
        VERSION ("1.00.00"),
        LOCATIONS (
          LOCATION ("."),
          LOCATION ("http://www.qedeq.org/0_00_53")
        )
      )
    )
  ),
  PARAGRAPHS (
    PARAGRAPH (
      LABEL ("theorem1"),
      "First we prove a theorem known as {\emph identity}:",
      PROPOSITION (
        SENTENCE (
          IMPL(PROP(1), PROP(1))
        ),
        PROOF (
          LINE (
            IMPL(PROP(1), IMPL(PROP(2), PROP(1))),
            ADDAXIOM ( LINK ("axiom1"))
          ),
          LINE (
            IMPL(PROP(1), IMPL(IMPL(PROP(1), PROP(1)), PROP(1))),
            REPLACEPROP (
              1, 
              PROP(2),
              IMPL(PROP(1), PROP(1))
            )
          ),
          LINE (
            IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))),
            ADDAXIOM ( LINK ("axiom2"))
          ),
          LINE (
            IMPL(IMPL(PROP(1), IMPL(IMPL(PROP(1), PROP(1)), PROP(3))), IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(1))), IMPL(PROP(1), PROP(3)))),
            REPLACEPROP (
              3, 
              PROP(2),
              IMPL(PROP(1), PROP(1))
            )
          ),
          LINE (
            IMPL(IMPL(PROP(1), IMPL(IMPL(PROP(1), PROP(1)), PROP(1))), IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(1))), IMPL(PROP(1), PROP(1)))),
            REPLACEPROP (
              4, 
              PROP(3),
              PROP(1)
            )
          ),
          LINE (
            IMPL(IMPL(PROP(1), IMPL(PROP(1), PROP(1))), IMPL(PROP(1), PROP(1))),
            MODUSPONENS (2, 5)
          ),
          LINE (
            IMPL(PROP(1), IMPL(PROP(1), PROP(1))),
            REPLACEPROP (
              1, 
              PROP(2),
              PROP(1)
            )
          ),
          LINE (
            IMPL(PROP(1), PROP(1)),
            MODUSPONENS (7, 6)
          )
        )
      )
    ),
    PARAGRAPH (
      LABEL ("theorem2"),
      "Now we prove a theorem  known as (one form of) {\emph hypothetical syllogism}:",
      PROPOSITION (
        SENTENCE (
          IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3))))
        ),
        PROOF (
          LINE (
            IMPL(PROP(1), IMPL(PROP(2), PROP(1))),
            ADDAXIOM ( LINK ("axiom1"))
          ),
          LINE (
            IMPL(PROP(1), IMPL(IMPL(PROP(2), PROP(3)), PROP(1))),
            REPLACEPROP (
              1, 
              PROP(2),
              IMPL(PROP(2), PROP(3))
            )
          ),
          LINE (
            IMPL(IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))), IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))))),
            REPLACEPROP (
              2, 
              PROP(1),
              IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3))))
            )
          ),
          LINE (
            IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))),
            ADDAXIOM ( LINK ("axiom2"))
          ),
          LINE (
            IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3))))),
            MODUSPONENS(4, 3)
          ),
          LINE (
            IMPL(IMPL(PROP(4), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(4), PROP(2)), IMPL(PROP(4), PROP(3)))),
            REPLACEPROP (
              4, 
              PROP(1),
              PROP(4)
            )
          ),
          LINE (
            IMPL(IMPL(PROP(4), IMPL(PROP(5), PROP(3))), IMPL(IMPL(PROP(4), PROP(5)), IMPL(PROP(4), PROP(3)))),
            REPLACEPROP (
              6, 
              PROP(2),
              PROP(5)
            )
          ),
          LINE (
            IMPL(IMPL(PROP(4), IMPL(PROP(5), PROP(6))), IMPL(IMPL(PROP(4), PROP(5)), IMPL(PROP(4), PROP(6)))),
            REPLACEPROP (
              7, 
              PROP(3),
              PROP(6)
            )
          ),
          LINE (
            IMPL(IMPL(IMPL(PROP(2), PROP(3)), IMPL(PROP(5), PROP(6))), IMPL(IMPL(IMPL(PROP(2), PROP(3)), PROP(5)), IMPL(IMPL(PROP(2), PROP(3)), PROP(6)))),
            REPLACEPROP (
              8, 
              PROP(4),
              IMPL(PROP(2), PROP(3))
            )
          ),
          LINE (
            IMPL(IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), PROP(6))), IMPL(IMPL(IMPL(PROP(2), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), IMPL(IMPL(PROP(2), PROP(3)), PROP(6)))),
            REPLACEPROP (
              9, 
              PROP(5),
              IMPL(PROP(1), IMPL(PROP(2), PROP(3)))
            )
          ),
          LINE (
            IMPL(IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), IMPL(PROP(2), PROP(3))), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3))))), IMPL(IMPL(IMPL(PROP(2), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))))),
            REPLACEPROP (
              10, 
              PROP(6),
              IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))
            )
          ),
          LINE (
            IMPL(IMPL(IMPL(PROP(2), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))), IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3))))),
            MODUSPONENS(5, 11)
          ),
          LINE (
            IMPL(PROP(1), IMPL(PROP(4), PROP(1))),
            REPLACEPROP (
              1, 
              PROP(2),
              PROP(4)
            )
          ),
          LINE (
            IMPL(IMPL(PROP(2), PROP(3)), IMPL(PROP(4), IMPL(PROP(2), PROP(3)))),
            REPLACEPROP (
              13, 
              PROP(1),
              IMPL(PROP(2), PROP(3))
            )
          ),
          LINE (
            IMPL(IMPL(PROP(2), PROP(3)), IMPL(PROP(1), IMPL(PROP(2), PROP(3)))),
            REPLACEPROP (
              14, 
              PROP(4),
              PROP(1)
            )
          ),
          LINE (
            IMPL(IMPL(PROP(2), PROP(3)), IMPL(IMPL(PROP(1), PROP(2)), IMPL(PROP(1), PROP(3)))),
            MODUSPONENS(15, 12)
          )

          
        )
      )
    )
  )
)