let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 3) = s . (intpos 3) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
let s be 0 -started State of SCMPDS; ( s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 3) = s . (intpos 3) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) ) )
set a = GBP ;
set x = DataLoc ((s . (intpos 4)),(- 1));
set y = DataLoc ((s . (intpos 4)),0);
assume that
A1:
s . (intpos 4) >= 7 + (s . (intpos 6))
and
A2:
s . GBP = 0
and
A3:
s . (intpos 6) > 0
; ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 3) = s . (intpos 3) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
set t0 = s;
set t1 = Exec (((GBP,5) := ((intpos 4),(- 1))),s);
set t2 = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s);
set Q2 = P;
A4:
7 + (s . (intpos 6)) > 7 + 0
by A3, XREAL_1:6;
then A5:
|.(s . (intpos 4)).| = s . (intpos 4)
by A1, ABSVALUE:def 1;
set Fi = (GBP,6) := 0;
set t02 = Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s));
set Q02 = P;
set t3 = IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))));
set t4 = IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))));
set t5 = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))));
set t6 = Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))));
A6:
DataLoc ((s . GBP),5) = intpos (0 + 5)
by A2, SCMP_GCD:1;
then A7:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP = 0
by A2, AMI_3:10, SCMPDS_2:47;
then A8:
DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:1;
then A9:
|.(((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP) + 5).| = 0 + 5
by XTUPLE_0:1;
then
|.((s . (intpos 4)) + 0).| <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP) + 5).|
by A1, A4, A5, XXREAL_0:2;
then A10:
DataLoc ((s . (intpos 4)),0) <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP),5)
by XTUPLE_0:1;
A11:
|.((s . GBP) + 5).| = 0 + 5
by A6, XTUPLE_0:1;
then
|.((s . (intpos 4)) + 0).| <> |.((s . GBP) + 5).|
by A1, A4, A5, XXREAL_0:2;
then
( s . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & DataLoc ((s . (intpos 4)),0) <> DataLoc ((s . GBP),5) )
by XTUPLE_0:1;
then A12:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_2:47;
A13:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 5) = s . (DataLoc ((s . (intpos 4)),(- 1)))
by A6, SCMPDS_2:47;
A14:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 4) = s . (intpos 4)
by A6, AMI_3:10, SCMPDS_2:47;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc ((s . (intpos 4)),0)) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:42
.=
s . (DataLoc ((s . (intpos 4)),0))
by A12, A10, SCMPDS_2:50
;
then A15:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:15;
A16: (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP =
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . GBP
by SCMPDS_5:15
.=
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . GBP
by SCMPDS_5:42
.=
0
by A7, A8, AMI_3:10, SCMPDS_2:50
;
A17:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5) = intpos (0 + 5)
by A16, SCMP_GCD:1;
then A18:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP = 0
by A16, AMI_3:10, SCMPDS_2:47;
|.(((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP) + 5).| = 0 + 5
by A17, XTUPLE_0:1;
then
|.((s . (intpos 4)) + 0).| <> |.(((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP) + 5).|
by A1, A4, A5, XXREAL_0:2;
then
DataLoc ((s . (intpos 4)),0) <> DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)
by XTUPLE_0:1;
then A19:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0))
by A15, SCMPDS_2:47;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos 4) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (intpos 4)
by SCMPDS_5:42
.=
s . (intpos 4)
by A14, A8, AMI_3:10, SCMPDS_2:50
;
then A20:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:15;
then A21:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) = s . (intpos 4)
by A17, AMI_3:10, SCMPDS_2:47;
then A22: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1))) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1)))
by SCMPDS_5:42
.=
s . (DataLoc ((s . (intpos 4)),0))
by A21, A19, SCMPDS_2:47
;
A23:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 3) = s . (intpos 3)
by A6, AMI_3:10, SCMPDS_2:47;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos 3) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (intpos 3)
by SCMPDS_5:42
.=
s . (intpos 3)
by A23, A8, AMI_3:10, SCMPDS_2:50
;
then A24:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 3) = s . (intpos 3)
by SCMPDS_5:15;
then A25:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) = s . (intpos 3)
by A17, AMI_3:10, SCMPDS_2:47;
A26:
s . (intpos 4) >= 1 + (6 + (s . (intpos 6)))
by A1;
then A27:
(s . (intpos 4)) - 1 >= 6 + (s . (intpos 6))
by XREAL_1:19;
A28:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 2) = s . (intpos 2)
by A6, AMI_3:10, SCMPDS_2:47;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos 2) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (intpos 2)
by SCMPDS_5:42
.=
s . (intpos 2)
by A28, A8, AMI_3:10, SCMPDS_2:50
;
then A29:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 2) = s . (intpos 2)
by SCMPDS_5:15;
then A30:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) = s . (intpos 2)
by A17, AMI_3:10, SCMPDS_2:47;
A31:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 6) = s . (intpos 6)
by A6, AMI_3:10, SCMPDS_2:47;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos 6) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (intpos 6)
by SCMPDS_5:42
.=
s . (intpos 6)
by A31, A8, AMI_3:10, SCMPDS_2:50
;
then
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 6) = s . (intpos 6)
by SCMPDS_5:15;
then A32:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6) = s . (intpos 6)
by A17, AMI_3:10, SCMPDS_2:47;
A33:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),6) = intpos (0 + 6)
by A16, SCMP_GCD:1;
A34:
now ( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 implies (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 )assume
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6)
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6)
by SCMPDS_5:40
.=
0
by A33, SCMPDS_2:46
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0
by SCMPDS_5:35;
verum end;
A35:
6 + (s . (intpos 6)) > 6 + 0
by A3, XREAL_1:6;
then
0 <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by A27, A21, ABSVALUE:def 1;
then A36:
GBP <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by XTUPLE_0:1;
A37:
(s . (intpos 4)) - 1 > 0
by A3, A26, XREAL_1:19;
then A38:
|.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).| = (s . (intpos 4)) - 1
by A21, ABSVALUE:def 1;
then
4 <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by A27, A35, XXREAL_0:2;
then A39:
intpos 4 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by XTUPLE_0:1;
A40: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 4)
by SCMPDS_5:42
.=
s . (intpos 4)
by A21, A39, SCMPDS_2:47
;
then A41:
|.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).| = s . (intpos 4)
by A1, A4, ABSVALUE:def 1;
then
4 <> |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by A1, A4, XXREAL_0:2;
then A42:
intpos 4 <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0)
by XTUPLE_0:1;
3 <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by A27, A35, A38, XXREAL_0:2;
then A43:
intpos 3 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by XTUPLE_0:1;
3 <> |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by A1, A4, A41, XXREAL_0:2;
then A44:
intpos 3 <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0)
by XTUPLE_0:1;
A45: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 3)
by SCMPDS_5:42
.=
s . (intpos 3)
by A25, A43, SCMPDS_2:47
;
A46: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 3)
by SCMPDS_5:41
.=
s . (intpos 3)
by A45, A44, SCMPDS_2:47
;
2 <> |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by A1, A4, A41, XXREAL_0:2;
then A47:
intpos 2 <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0)
by XTUPLE_0:1;
A48: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 4)
by SCMPDS_5:41
.=
s . (intpos 4)
by A40, A42, SCMPDS_2:47
;
A49: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . GBP
by SCMPDS_5:42
.=
0
by A18, A36, SCMPDS_2:47
;
A50:
(2 * |.((s . (intpos 4)) + (- 1)).|) + 1 = (2 * ((s . (intpos 4)) - 1)) + 1
by A27, A35, ABSVALUE:def 1;
then
|.((s . (intpos 4)) + (- 1)).| <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP) + 5).|
by A3, A27, A9, XREAL_1:6;
then A51:
DataLoc ((s . (intpos 4)),(- 1)) <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP),5)
by XTUPLE_0:1;
0 <> |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by A1, A4, A40, ABSVALUE:def 1;
then A52:
GBP <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0)
by XTUPLE_0:1;
A53: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . GBP
by SCMPDS_5:41
.=
0
by A49, A52, SCMPDS_2:47
;
then A54:
GBP <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by AMI_3:10, SCMP_GCD:1;
2 <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by A27, A35, A38, XXREAL_0:2;
then A55:
intpos 2 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by XTUPLE_0:1;
A56: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 2)
by SCMPDS_5:42
.=
s . (intpos 2)
by A30, A55, SCMPDS_2:47
;
A57: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 2)
by SCMPDS_5:41
.=
s . (intpos 2)
by A56, A47, SCMPDS_2:47
;
A58:
intpos 2 <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by A53, AMI_3:10, SCMP_GCD:1;
(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . GBP
by SCMPDS_5:41
.=
0
by A53, A54, SCMPDS_2:48
;
then A59:
DataLoc (((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),6) = intpos (0 + 6)
by SCMP_GCD:1;
then A60:
|.(((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP) + 6).| = 0 + 6
by XTUPLE_0:1;
A61:
DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4) = intpos (0 + 4)
by A53, SCMP_GCD:1;
then A62:
|.(((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP) + 4).| = 0 + 4
by XTUPLE_0:1;
then
|.((s . (intpos 4)) + (- 1)).| <> |.(((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP) + 4).|
by A27, A35, A50, XXREAL_0:2;
then A63:
DataLoc ((s . (intpos 4)),(- 1)) <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by XTUPLE_0:1;
A64: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 2)
by SCMPDS_5:41
.=
s . (intpos 2)
by A57, A58, SCMPDS_2:48
;
now (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) = s . (intpos 2)per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) = s . (intpos 2)hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2)
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2)
by SCMPDS_5:40
.=
s . (intpos 2)
by A29, A33, AMI_3:10, SCMPDS_2:46
;
verum end; suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) = s . (intpos 2)hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 2)
by SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 2)
by SCMPDS_5:41
.=
s . (intpos 2)
by A64, A59, AMI_3:10, SCMPDS_2:48
;
verum end;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 2) = s . (intpos 2)
by SCMPDS_5:35; ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 3) = s . (intpos 3) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
A65:
intpos 3 <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by A53, AMI_3:10, SCMP_GCD:1;
A66: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 3)
by SCMPDS_5:41
.=
s . (intpos 3)
by A46, A65, SCMPDS_2:48
;
now (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) = s . (intpos 3)per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) = s . (intpos 3)hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3)
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3)
by SCMPDS_5:40
.=
s . (intpos 3)
by A24, A33, AMI_3:10, SCMPDS_2:46
;
verum end; suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) = s . (intpos 3)hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 3)
by SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 3)
by SCMPDS_5:41
.=
s . (intpos 3)
by A66, A59, AMI_3:10, SCMPDS_2:48
;
verum end;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 3) = s . (intpos 3)
by SCMPDS_5:35; ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
A67:
intpos 6 <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by A53, AMI_3:10, SCMP_GCD:1;
6 <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by A26, A35, A38, XREAL_1:19;
then A68:
intpos 6 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by XTUPLE_0:1;
A69: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 6)
by SCMPDS_5:42
.=
s . (intpos 6)
by A32, A68, SCMPDS_2:47
;
6 <> |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by A1, A4, A41, XXREAL_0:2;
then A70:
intpos 6 <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0)
by XTUPLE_0:1;
A71: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 6)
by SCMPDS_5:41
.=
s . (intpos 6)
by A69, A70, SCMPDS_2:47
;
A72: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 6)
by SCMPDS_5:41
.=
s . (intpos 6)
by A71, A67, SCMPDS_2:48
;
A73: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 4)
by SCMPDS_5:41
.=
((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)
by A61, SCMPDS_2:48
.=
(s . (intpos 4)) - 1
by A48
;
A74:
now ( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) )assume A75:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0
;
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 )then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 6)
by SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 6)
by SCMPDS_5:41
.=
(s . (intpos 6)) + (- 1)
by A72, A59, SCMPDS_2:48
.=
(s . (intpos 6)) - 1
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1
by SCMPDS_5:35;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)
by A75, SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 4)
by SCMPDS_5:41
.=
(s . (intpos 4)) - 1
by A73, A59, AMI_3:10, SCMPDS_2:48
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1
by SCMPDS_5:35;
verum end;
hereby ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6)hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6)
by A3, A34;
verum end; suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6)hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) < s . (intpos 6)
by A74, XREAL_1:146;
verum end;
hereby ( ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose A76:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6))then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)
by SCMPDS_5:40
.=
s . (intpos 4)
by A20, A33, AMI_3:10, SCMPDS_2:46
;
then
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:35;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7
+ ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6))
by A1, A4, A34, A76, XXREAL_0:2;
verum end; suppose A77:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7 + ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6))
(s . (intpos 4)) - 1
>= (7 + (s . (intpos 6))) - 1
by A1, XREAL_1:9;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) >= 7
+ ((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6))
by A74, A77;
verum end;
A78:
now for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos i) = s . (intpos i) )assume that A79:
i >= 7
and
i <> (s . (intpos 4)) - 1
and
i <> s . (intpos 4)
;
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos i) = s . (intpos i)
i > 5
by A79, XXREAL_0:2;
hence
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos i) = s . (intpos i)
by A6, AMI_3:10, SCMPDS_2:47;
verum end;
A80:
now for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos i) = s . (intpos i) )assume that A81:
i >= 7
and A82:
(
i <> (s . (intpos 4)) - 1 &
i <> s . (intpos 4) )
;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos i) = s . (intpos i)A83:
i > 5
by A81, XXREAL_0:2;
thus (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos i) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (intpos i)
by SCMPDS_5:42
.=
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos i)
by A8, A83, AMI_3:10, SCMPDS_2:50
.=
s . (intpos i)
by A78, A81, A82
;
verum end;
A84:
now for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i) )assume that A85:
i >= 7
and A86:
(
i <> (s . (intpos 4)) - 1 &
i <> s . (intpos 4) )
;
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)
i > 5
by A85, XXREAL_0:2;
hence (Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) =
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos i)
by A17, AMI_3:10, SCMPDS_2:47
.=
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos i)
by SCMPDS_5:15
.=
s . (intpos i)
by A80, A85, A86
;
verum end;
A87:
now for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i) )assume that A88:
i >= 7
and A89:
i <> (s . (intpos 4)) - 1
and A90:
i <> s . (intpos 4)
;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)A91:
intpos i <> DataLoc (
((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),
(- 1))
proof
assume
intpos i = DataLoc (
((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),
(- 1))
;
contradiction
then
i = |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by XTUPLE_0:1;
hence
contradiction
by A37, A21, A89, ABSVALUE:def 1;
verum
end; thus (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos i)
by SCMPDS_5:42
.=
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by A91, SCMPDS_2:47
.=
s . (intpos i)
by A84, A88, A89, A90
;
verum end;
A92:
now for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i) )assume that A93:
(
i >= 7 &
i <> (s . (intpos 4)) - 1 )
and A94:
i <> s . (intpos 4)
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)A95:
intpos i <> DataLoc (
((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),
0)
proof
assume
intpos i = DataLoc (
((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),
0)
;
contradiction
then
i = |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by XTUPLE_0:1;
hence
contradiction
by A1, A4, A40, A94, ABSVALUE:def 1;
verum
end; thus (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos i)
by SCMPDS_5:41
.=
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by A95, SCMPDS_2:47
.=
s . (intpos i)
by A87, A93, A94
;
verum end;
A96:
now for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) holds
(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i) )assume that A97:
i >= 7
and A98:
(
i <> (s . (intpos 4)) - 1 &
i <> s . (intpos 4) )
;
(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) = s . (intpos i)
i > 4
by A97, XXREAL_0:2;
then A99:
intpos i <> DataLoc (
((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by A53, AMI_3:10, SCMP_GCD:1;
thus (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos i)
by SCMPDS_5:41
.=
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by A99, SCMPDS_2:48
.=
s . (intpos i)
by A92, A97, A98
;
verum end;
hereby ( ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) ) )
let i be
Nat;
( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos b1) = s . (intpos b1) )set xi =
intpos i;
assume that A100:
i >= 7
and A101:
(
i <> (s . (intpos 4)) - 1 &
i <> s . (intpos 4) )
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos b1) = s . (intpos b1)A102:
i > 6
by A100, XXREAL_0:2;
per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos b1) = s . (intpos b1)then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by SCMPDS_5:40
.=
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos i)
by A33, A102, AMI_3:10, SCMPDS_2:46
.=
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos i)
by SCMPDS_5:15
.=
s . (intpos i)
by A80, A100, A101
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i)
by SCMPDS_5:35;
verum end; suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0
;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos b1) = s . (intpos b1)then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos i)
by SCMPDS_5:41
.=
(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos i)
by A59, A102, AMI_3:10, SCMPDS_2:48
.=
s . (intpos i)
by A96, A100, A101
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos i) = s . (intpos i)
by SCMPDS_5:35;
verum end;
end;
A103: (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 5) =
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (intpos 5)
by SCMPDS_5:15
.=
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (intpos 5)
by SCMPDS_5:42
.=
(s . (DataLoc ((s . (intpos 4)),(- 1)))) - (s . (DataLoc ((s . (intpos 4)),0)))
by A14, A13, A12, A8, SCMPDS_2:50
;
then A104:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) = (s . (DataLoc ((s . (intpos 4)),(- 1)))) - (s . (DataLoc ((s . (intpos 4)),0)))
by A16, SCMP_GCD:1;
|.((s . (intpos 4)) + (- 1)).| <> |.((s . GBP) + 5).|
by A3, A27, A50, A11, XREAL_1:6;
then
DataLoc ((s . (intpos 4)),(- 1)) <> DataLoc ((s . GBP),5)
by XTUPLE_0:1;
then A105:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_2:47;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),s)))) . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:42
.=
s . (DataLoc ((s . (intpos 4)),(- 1)))
by A105, A51, SCMPDS_2:50
;
then A106:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:15;
then A107:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 5) = s . (DataLoc ((s . (intpos 4)),(- 1)))
by A20, A17, SCMPDS_2:47;
5 <> |.(((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)).|
by A27, A35, A38, XXREAL_0:2;
then A108:
intpos 5 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by XTUPLE_0:1;
A109: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 5) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 5)
by SCMPDS_5:42
.=
s . (DataLoc ((s . (intpos 4)),(- 1)))
by A107, A108, SCMPDS_2:47
;
|.((s . (intpos 4)) + 0).| <> |.(((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP) + 4).|
by A1, A4, A5, A62, XXREAL_0:2;
then A110:
DataLoc ((s . (intpos 4)),0) <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),4)
by XTUPLE_0:1;
A111: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0)) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0))
by A40, SCMPDS_5:41
.=
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),5))
by SCMPDS_2:47
.=
s . (DataLoc ((s . (intpos 4)),(- 1)))
by A49, A109, SCMP_GCD:1
;
A112: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0)) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:41
.=
s . (DataLoc ((s . (intpos 4)),(- 1)))
by A111, A110, SCMPDS_2:48
;
|.((s . (intpos 4)) + (- 1)).| <> |.(((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + 0).|
by A50, A41;
then A113:
DataLoc ((s . (intpos 4)),(- 1)) <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),0)
by XTUPLE_0:1;
A114: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1))) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:41
.=
s . (DataLoc ((s . (intpos 4)),0))
by A22, A113, SCMPDS_2:47
;
A115: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1))) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:41
.=
s . (DataLoc ((s . (intpos 4)),0))
by A114, A63, SCMPDS_2:48
;
hereby ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0)) implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 ) )
A116:
DataLoc (
(s . (intpos 4)),
(- 1))
<> DataLoc (
((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),6)
by A27, A35, A50, A59, XTUPLE_0:1;
assume
s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (intpos 4)),0))
;
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 )then A117:
(s . (DataLoc ((s . (intpos 4)),(- 1)))) - (s . (DataLoc ((s . (intpos 4)),0))) > (s . (DataLoc ((s . (intpos 4)),0))) - (s . (DataLoc ((s . (intpos 4)),0)))
by XREAL_1:9;
then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1))) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1)))
by A104, SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:41
.=
s . (DataLoc ((s . (intpos 4)),0))
by A115, A116, SCMPDS_2:48
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:35;
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 )
|.((s . (intpos 4)) + 0).| <> |.(((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP) + 6).|
by A1, A4, A5, A60, XXREAL_0:2;
then A118:
DataLoc (
(s . (intpos 4)),
0)
<> DataLoc (
((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP),6)
by XTUPLE_0:1;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0)) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0))
by A104, A117, SCMPDS_6:73
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:41
.=
s . (DataLoc ((s . (intpos 4)),(- 1)))
by A112, A118, SCMPDS_2:48
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:35;
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 )thus
(
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = (s . (intpos 6)) - 1 &
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 )
by A16, A103, A74, A117, SCMP_GCD:1;
verum
end;
A119:
|.(((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP) + 6).| = 0 + 6
by A33, XTUPLE_0:1;
hereby verum
A120:
DataLoc (
(s . (intpos 4)),
(- 1))
<> DataLoc (
((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),6)
by A27, A35, A50, A33, XTUPLE_0:1;
assume
s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (intpos 4)),0))
;
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1))) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 )then A121:
(s . (DataLoc ((s . (intpos 4)),(- 1)))) - (s . (DataLoc ((s . (intpos 4)),0))) <= (s . (DataLoc ((s . (intpos 4)),0))) - (s . (DataLoc ((s . (intpos 4)),0)))
by XREAL_1:9;
then (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1))) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1)))
by A104, SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:40
.=
s . (DataLoc ((s . (intpos 4)),(- 1)))
by A106, A120, SCMPDS_2:46
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (intpos 4)),(- 1)))
by SCMPDS_5:35;
( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0)) & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 )
|.((s . (intpos 4)) + 0).| <> |.(((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP) + 6).|
by A1, A4, A5, A119, XXREAL_0:2;
then A122:
DataLoc (
(s . (intpos 4)),
0)
<> DataLoc (
((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),6)
by XTUPLE_0:1;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0)) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0))
by A104, A121, SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:40
.=
s . (DataLoc ((s . (intpos 4)),0))
by A15, A122, SCMPDS_2:46
;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (intpos 4)),0))
by SCMPDS_5:35;
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0 thus
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),P,s)) . (intpos 6) = 0
by A16, A103, A34, A121, SCMP_GCD:1;
verum
end;