Theorem "rec5time" Functions Real l; Real r; Real T; End. ProgramVariables Real v; Real x; Real t; End. Problem l <= x & x<=r & v >= 0 & T > 0 & l + 2*v*T <= r -> [ { {if (x+v*T < l & v <= 0 | x + v*T > r & v >= 0) {v:=-v;}} {t:=0; {x'=v, t'=1 & t <= T}} }*@invariant((l<=x&x<=r) & l + 2*abs(v)*T <= r) ](l <= x & x <= r) End. Tactic "rec5time: Proof 1" unfold ; loop({`(l()<=x&x<=r())&l()+2*abs(v)*T()<=r()`}, 1) ; <( QE, QE, boxAnd(1) ; andR(1) ; <( unfold ; <( diffInvariant({`x-(old(x)-v*t)=0&t>=0`}, 1) ; dW(1) ; QE, diffInvariant({`x-(old(x)+v*t)=0&t>=0`}, 3) ; dW(3) ; QE, diffInvariant({`x-(old(x)+v*t)=0&t>=0`}, 3) ; dW(3) ; QE, diffInvariant({`x-(old(x)+v*t)=0&t>=0`}, 3) ; dW(3) ; QE, diffInvariant({`x-(old(x)+v*t)=0&t>=0`}, 3) ; dW(3) ; QE ), master ) ) End. Tactic "rec5time: Proof 2" unfold ; loop({`(l()<=x&x<=r())&l()+2*abs(v)*T()<=r()`}, 1) ; <( QE, QE, boxAnd(1) ; andR(1) ; <( unfold ; <( ODE(1), ODE(3), ODE(3), ODE(3), ODE(3) ), master ) ) End. Tactic "rec5time: Proof 3" unfold ; loop({`(l()<=x&x<=r())&l()+2*abs(v)*T()<=r()`}, 1) ; <( QE, QE, boxAnd(1) ; andR(1) ; <( composeb(1) ; composeb(1.1) ; ODE(1.1.1) ; master, master ) ) End. End.