Logiweb(TM)

14.271 Proof of non-existent lemma

Prev Up Next Page 742 of 800 Search internet


Origin: check. Landing-place: diagnose.

Proof of non-existent lemma: L

The sequent evaluator has found a proof of a lemma named L but the page did not define a lemma named L.

From the point of view of the verifier, a lemma is a symbol for which the home page of the symbol has both a statement definition and a proof definition. In contrast, axioms and theories are symbols which merely have a statement definition. Symbols which merely have a proof definition give rise to the 'Proof of non-existent lemma' error message.

Prev Up Next Page 742 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05