| 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.
| Search logiweb.eu |