dV on "equals": an implementation is missing about keymaerax-release HOT 2 CLOSED

Thanks for the report. That's actually a bug in the error checking: dV does not support equational postconditions directly because there is no good notion of "epsilon" progress towards it.

Here are two alternative more "canonical" ways to prove an equational postcondition.

1. In your example, the intuition for the proof since x starts at 0 and reaches x > 1 eventually, it should have hit x=1 along the way. Use K<&> from the right-click menu to turn the postcondition to x>1 (or x>=1) first.

This gives you two branches. The "easy" branch <{x'=1}>x>1 which should prove by dV automatically.

The more interesting branch has a box modality: [{x'=1 & !x=1}] !x>1. Intuitively, this gives a contrapositive reading of what I wrote above, i.e., if the ODE never hit x=1, then it could never have hit x>1. This should prove automatically by ODE.

2. Another case is if the equality happens to be an invariant of your system, for example:

x=0 & c=0 -> <{x'=1,c'=c}>(x>1&c=0)

Here, you can again use K<&> with x>1. The interesting branch has a box modality: [{x'=1,c'=c & !(x>1&c=0)}] !x>1. This proves automatically (or you can diff cut c=0).

Alternatively, if you would like to use [{x'=1,c'=c}]c=0 more in your subsequent proofs, then use "compactCut" from the right-click menu to first add an assumption [{x'=1,c'=c}]c=0.

from keymaerax-release.

Fixed in e078f77

from keymaerax-release.