Theorem "rec10conv1" ProgramVariables Real x; Real y; End. Problem < {y:=x-1; x:=1;}*>y=0 End. Tactic "rec10conv1: Proof 1" iterated(1) ; unfold ; iterated(2) ; unfold ; iterated(3) ; orR(3) ; hideR(4=={`<{y:=x-1;x:=1;}*>y=0`}) ; QE End. End. Theorem "rec10conv2" ProgramVariables Real y; Real x; End. Problem < {y:=y-1; x:=x+1;}*>x >= y End. Tactic "rec10conv2: Proof 1" con({`v`}, {`y-x<=v`}, 1) ; <( QE, QE, composed(1) ; assignd(1) ; assignd(1) ; QE ) End. End. Theorem "rec10clashes" ProgramVariables Real x; Real y; End. Problem ([x:=x+y;]x=1 <-> (x+y)=1) & ([x:=x+y;]x+x=1 <-> (x+y)+x=1) & ([x:=x+y;][x:=x+y;]x=1 <-> [x:=(x+y)+y;]x=1) & ([x:=x+y;][x:=x+y;]x=1 <-> [x:=(x+y)+y;](x+y)=1) & ([x:=x+y;][x:=x+y;]x=1 <-> [x:=x+y;](x+y)=1) & ([x:=x+y;][{x'=x+y}]x=1 <-> [{x'=(x+y)+y}]x=1) & ([x:=x+y;][{y'=y+1}]x=1 <-> [{y'=y+1}]x+y=1) & ([x:=x+y;][{y:=y;}*]x=1 <-> [{y:=y;}*]x+y=1) End. End.