14.275 Lemma L has no proof

Prev Up Next Page 746 of 800 Search internet

Origin: check. Landing-place: diagnose.

Lemma L has no proof. Avoid referencing that lemma.

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.

The 'Lemma L has no proof' message indicates that L is used as a lemma but does not have a proof. The error could be that a proof of L is missing or the error could be that e.g. an axiom was used as if it were a lemma.

Note that the verifier has no reservations about lemmas which have no proof. But the verifier protests if such a lemma is used as a lemma in the proof of some other lemma.

Prev Up Next Page 746 of 800 Search logiweb.eu

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