|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 yields . 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 . The error may indicate an error in the proof or a bug in a tactic.
|Page 724 of 800||Search logiweb.eu|