## 14.275 Lemma L has no proof

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.

Page 746 of 800 |
| Search logiweb.eu |

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