|Page 726 of 800||Search internet|
Origin: check. Landing-place: diagnose.
Verify-seqop used on false condition: s
The verify sequent operator applied to a sequent yields provided the side condition s evaluates to . Thus, the verify operator allows to remove a satisfied side condition. The 'Verify-seqop used on false condition' indicates, however, that the side condition was not true. The error may indicate an error in the proof or a bug in a tactic.
|Page 726 of 800||Search logiweb.eu|