14.255 Verify-seqop used on false condition

Prev Up Next 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 << P ,, C ,, s endorse x >> yields << P ,, C ,, x >> provided the side condition s evaluates to true. 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.

Prev Up Next Page 726 of 800 Search logiweb.eu

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