MODULE (
  HEADER (
    SPEC (
      NAME ("properror2"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION ("http://www.qedeq.org/0_00_53")
      )
    ),
    HEADLINE ("A module with an error."),
    DESCRIPTION (
      "This module has an error that must be found by the proof verifier."
    ),
    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")
        )
      )
    )
  ),
  PARAGRAPHS (
    PARAGRAPH (
      LABEL ("thilb1"),
      "This first paragraph should be verified, it has no errors.",
      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)
          )
        )
      ),
      "(By the way: this proposition is the form for the Hypothetical Syllogism.)"
    ),
    PARAGRAPH (
      LABEL ("ehilb1"),
      "Now we try to proof the same formula with a wrong proof. It is equal to the first one til the third proof line where the usage of ""REVERSEABBREVIATION"" wants to reverse the abbreviation for an implication at the second occurence (instead of the first one). The proof checker should tell you about an error in line 87.",
      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"), 2)
          ),
          LINE (
            IMPL(IMPL(PROP(1), PROP(2)), IMPL(IMPL(PROP(3), PROP(1)), IMPL(PROP(3), PROP(2)))),
            REVERSEABBREVIATION (3, LINK ("impl"), 1)
          )
        )
      )
    )
  )
)

