MODULE (
  HEADER (
    SPEC (
      NAME ("properror"),
      VERSION ("1.00.00"),
      VERSION ("1.00.00"),
      LOCATIONS (
        LOCATION (".")
      )
    ),
    HEADLINE ("A module with an error."),
    DESCRIPTION (
      "This module has an error that must be found by the proof verifier."
    ),
    EMAIL ("principa@meyling.com"),
    AUTHORS (
      AUTHOR ("Michael Meyling",EMAIL ("michael@meyling.com"))
    )
  ),
  IMPORTS (
    IMPORT (
      SPEC (
        NAME ("propaxiom"),
        VERSION ("1.00.00"),
        VERSION ("1.00.00"),
        LOCATIONS (
          LOCATION (".")
        )
      )
    )
  ),
  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 but it has an additional proof line at the end. The proof lines are all correct. Only the last proof line is not identical with the sentence we would like to proof. So the proof checker should tell you about an error in line 93.",
      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)
          ),
          LINE (
            IMPL(OR(PROP(1), PROP(1)), PROP(1)),
            ADDAXIOM ( LINK ("axiom1"))
          )
        )
      )
    )
  )
)