14.253 Probans-seqop used on non-endorsement

Prev Up Next Page 724 of 800 Search internet

Origin: check. Landing-place: diagnose.

Probans-seqop used on non-endorsement R

The modus probans sequent operator applied to a sequent << P ,, C ,, s endorse x >> yields << P ,, C setunion {{ s }} ,, x >>. Thus, the probans operator allows to move a side condition s from the conclusion to the set of assumed side conditions. The 'Probans-seqop used on non-endorsement' indicates that the conclusion of the sequent did not have form s endorse x. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 724 of 800 Search logiweb.eu

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