Theorem "rec10conv1" ProgramVariables Real x; Real y; End. Problem < {y:=x-1; x:=1;}*>y=0 End. Tactic "rec10conv1: Proof 1" iterated('R=="<{y:=x-1;x:=1;}*>y=0"); iterated('R=="y=0|#<{y:=x-1;x:=1;}*>y=0#"); composed('R=="y=0|#(y=0|<{y:=x-1;x:=1;}*>y=0)#"); assignd('R=="y=0|#(y=0|<{y:=x-1;x:=1;}*>y=0)#"); orR('R=="y_0=0|\forall y (y=x-1->(y=0|<{y:=x-1;x:=1;}*>y=0))"); allR('R=="\forall y (y=x-1->(y=0|<{y:=x-1;x:=1;}*>y=0))"); implyR('R=="y=x-1->(y=0|<{y:=x-1;x:=1;}*>y=0)"); assignd('R=="(y=0|<{y:=x-1;x:=1;}*>y=0)"); orR('R=="y=0|<{y:=x-1;x:=1;}*>y=0"); composed('R=="<{y:=x-1;x:=1;}*>y=0"); assignd('R=="<{y:=x-1;x:=1;}*>y=0"); assignd('R=="<{y:=x-1;x:=1;}*>y=0"); iterated('R=="<{y:=x-1;x:=1;}*>y=0"); orR('R=="y=0|<{y:=x-1;x:=1;}*>y=0"); QE using "y_1=x_0-1 :: y=1-1 :: x=1 :: y_0=0 :: y_1=0 :: y=0 :: nil"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", "v>=y-x", 'R=="<{y:=y-1;x:=x+1;}*>x>=y"); <( "Init": QE, "Post": QE, "Step": composed('R=="v-1>=y-x"); assignd('R=="v-1>=y-x"); assignd('R=="v-1>=y-1-x"); 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.