Page 730 of 800
| Page 730 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Deref-seqop applied to R produced non-meta term: R prime
The Deref sequent operator applied to a sequent 
yields 
where 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 'Deref-seqop produced non-meta term' indicates that the statement definition of n is illformed.
| Page 730 of 800 | Search logiweb.eu |