let P be Instruction-Sequence of SCMPDS; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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 :: thesis: ( (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 ; :: thesis: (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; :: thesis: 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 :: thesis: (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 ; :: thesis: (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 ;
:: thesis: 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 ; :: thesis: (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 ;
:: thesis: verum

end;

end;

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; :: thesis: ( (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 :: thesis: (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 ; :: thesis: (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 ;
:: thesis: 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 ; :: thesis: (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 ;
:: thesis: verum

end;

end;

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; :: thesis: ( (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 :: thesis: ( (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 ; :: thesis: ( (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; :: thesis: (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; :: thesis: verum

end;

hereby :: thesis: ( (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 ; :: thesis: (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; :: thesis: 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 ; :: thesis: (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; :: thesis: verum

end;

end;

end;

hereby :: thesis: ( ( 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 ; :: thesis: (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; :: thesis: 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 ; :: thesis: (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; :: thesis: verum

end;

end;

end;

A78: now :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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; :: thesis: verum

end;

A80: now :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: (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 ; :: thesis: verum

end;

A84: now :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: (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 ;
:: thesis: verum

end;

A87: now :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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)) ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum

end;

A92: now :: thesis: 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; :: thesis: ( 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) ; :: thesis: (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) ; :: thesis: 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; :: thesis: 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 ; :: thesis: verum

end;

A96: now :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: (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 ; :: thesis: verum

end;

hereby :: thesis: ( ( 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; :: thesis: ( 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 b₁) = s . (intpos b₁) )
set xi = intpos i;
assume that
A100: i >= 7 and
A101: ( i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) ) ; :: thesis: (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 b₁) = s . (intpos b₁)
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 ; :: thesis: (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 b₁) = s . (intpos b₁)

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; :: thesis: 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 ; :: thesis: (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 b₁) = s . (intpos b₁)

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; :: thesis: verum

end;

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 :: thesis: ( 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)) ; :: thesis: ( (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; :: thesis: ( (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; :: thesis: ( (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; :: thesis: 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 :: thesis: 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)) ; :: thesis: ( (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; :: thesis: ( (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; :: thesis: (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; :: thesis: verum

end;