Page 725 of 800
| Page 725 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
Verify-seqop used on non-endorsement: R
The verify sequent operator applied to a sequent 
yields 
provided the side condition s is true. Thus, the verify operator allows to remove a satisfied side condition. The 'Verify-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 725 of 800 | Search logiweb.eu |