Page 735 of 800
| Page 735 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
IdEst-seqop used on non-matching result. Attempt to match y with R
The IdEst sequent operator applied to a sequent 
and a name n yields 
if n is the name of a lemma and x is what the lemma says. Alternatively, n may be a theorem, axiom, theory, or whatever that has a statement definition. The 'IdEst-seqop used on non-matching result' indicates that the statement definition of n was not x.
| Page 735 of 800 | Search logiweb.eu |