Theorem "rec6simple" Functions Real l; Real r; Real T; End. ProgramVariables Real v; Real x; Real t; End. Problem T > 0 & v > 0 & t = 0 & l <= x & x + v*T <= r -> [ {x'=v, t'=1 & t <= T}] (l <= x & x <= r) End. Tactic "rec6simple: Proof 1" unfold ; dC({`x=old(x)+v*t`}, 1) ; <( dC({`t>=0`}, 1) ; <( dW(1) ; QE, dI(1) ), dI(1) ) End. End. Theorem "rec6right" Functions Real l; Real r; Real T; End. ProgramVariables Real v; Real x; Real t; End. Problem T > 0 & v > 0 & t = 0 & l <= x & x + v*T <= r -> [ {x'=v, v'=-v^2, t'=1 & t <= T}] (x <= r) End. Tactic "rec6right: Proof 1" unfold ; dC({`x<=old(x)+old(v)*t`}, 1) ; <( dW(1) ; QE, dC({`v<=old(v)`}, 1) ; <( dI(1), dI(1) ) ) End. End. Theorem "rec6left" Functions Real l; Real r; Real T; End. ProgramVariables Real v; Real x; Real t; End. Problem T > 0 & v > 0 & t = 0 & l <= x & x + v*T <= r -> [ {x'=v, v'=-v^2, t'=1 & t <= T}] (l <= x) End. Tactic "rec6left: Proof 1" unfold ; dC({`v>0`}, 1) ; <( dI(1), dG({`{y'=v/2*y}`}, {`v*y^2>0`}, 1) ; existsR({`1`}, 1) ; dI(1) ) End. End.