14.264 IdEst-seqop used on non-matching result

Prev Up Next 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 << P ,, C ,, x >> and a name n yields << P ,, C ,, n >> 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.

Prev Up Next Page 735 of 800 Search logiweb.eu

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