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" implyR(1) ; loop("(l()<=x&x<=r())&l()+2*abs(v)*T()<=r()", 1) ; <( QE, QE, master ) End. Tactic "rec5time: Proof 2" implyR(1) ; loop("(l()<=x&x<=r())&l()+2*abs(v)*T()<=r()", 1) ; <( master, master, unfold ; <( diffInvariant("x-(old(x)-v*t)=0&t>=0", 1) ; dW(1) ; QE, diffInvariant("x-(old(x)+v*t)=0&t>=0", 1) ; dW(1) ; QE ) ) End. End.