## 14.271 Proof of non-existent lemma

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.

Page 742 of 800 |
| Search logiweb.eu |

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