14.263 Endorse-seqop used on non-meta term

Prev Up Next Page 734 of 800 Search internet

Origin: check. Landing-place: diagnose.

Endorse-seqop used on non-meta term: x

The Endorse sequent operator applied to a sequent << P ,, C ,, x >> and a metaterm s yields << P ,, C setminus {{ s }} ,, s endorse x >>. Thus, the Endorse operator allows to move a side condition s from the set of assumed side conditions to the conclusion. The Endorse operator can be used for hypothetical reasoning like 'Assume x is free for y in z, prove some lemma, conclude that if x is free for y in z then the lemma holds'. In this case, 'x is free for y in z' serves as side condition s.

The 'Endorse-seqop used on non-meta term' indicates that the side condition s was illformed. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 734 of 800 Search logiweb.eu

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