let s be 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) ) )
set t0 = Initialize s;
set t1 = Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s);
set t2 = IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s;
A4: 7 + (s . (intpos 6)) > 7 + 0 by A3, XREAL_1:8;
then A5: abs (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 )),s);
set t3 = IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s);
set t4 = IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s);
set t5 = IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s);
set t6 = Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s));
A6: (Initialize s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:40;
A7: (Initialize s) . GBP = 0 by A2, SCMPDS_5:40;
then A8: DataLoc ((Initialize s) . GBP ),5 = intpos (0 + 5) by SCMP_GCD:5;
then A9: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP = 0 by A7, AMI_3:52, SCMPDS_2:59;
then A10: DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP ),5 = intpos (0 + 5) by SCMP_GCD:5;
then A11: abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP ) + 5) = 0 + 5 by ZFMISC_1:33;
then abs ((s . (intpos 4)) + 0 ) <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP ) + 5) by A1, A4, A5, XXREAL_0:2;
then A12: DataLoc (s . (intpos 4)),0 <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP ),5 by ZFMISC_1:33;
A13: abs (((Initialize s) . GBP ) + 5) = 0 + 5 by A8, ZFMISC_1:33;
then abs ((s . (intpos 4)) + 0 ) <> abs (((Initialize s) . GBP ) + 5) by A1, A4, A5, XXREAL_0:2;
then ( (Initialize s) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),0 ) & DataLoc (s . (intpos 4)),0 <> DataLoc ((Initialize s) . GBP ),5 ) by SCMPDS_5:40, ZFMISC_1:33;
then A14: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_2:59;
A15: (Initialize s) . (intpos 4) = s . (intpos 4) by SCMPDS_5:40;
then A16: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos 5) = s . (DataLoc (s . (intpos 4)),(- 1)) by A6, A8, SCMPDS_2:59;
A17: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos 4) = s . (intpos 4) by A15, A8, AMI_3:52, SCMPDS_2:59;
(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc (s . (intpos 4)),0 ) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:47
.= s . (DataLoc (s . (intpos 4)),0 ) by A14, A12, SCMPDS_2:62 ;
then A18: (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:40;
A19: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . GBP by SCMPDS_5:47
.= 0 by A9, A10, AMI_3:52, SCMPDS_2:62 ;
then A20: (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP = 0 by SCMPDS_5:40;
then A21: DataLoc ((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),5 = intpos (0 + 5) by SCMP_GCD:5;
then A22: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . GBP = 0 by A20, AMI_3:52, SCMPDS_2:59;
abs (((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 5) = 0 + 5 by A21, ZFMISC_1:33;
then abs ((s . (intpos 4)) + 0 ) <> abs (((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)) . GBP ),5 by ZFMISC_1:33;
then A23: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),0 ) by A18, SCMPDS_2:59;
(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos 4) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (intpos 4) by SCMPDS_5:47
.= s . (intpos 4) by A17, A10, AMI_3:52, SCMPDS_2:62 ;
then A24: (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4) = s . (intpos 4) by SCMPDS_5:40;
then A25: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4) = s . (intpos 4) by A21, AMI_3:52, SCMPDS_2:59;
then A26: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1)) by SCMPDS_5:47
.= s . (DataLoc (s . (intpos 4)),0 ) by A25, A23, SCMPDS_2:59 ;
(Initialize s) . (intpos 3) = s . (intpos 3) by SCMPDS_5:40;
then A27: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos 3) = s . (intpos 3) by A8, AMI_3:52, SCMPDS_2:59;
(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos 3) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (intpos 3) by SCMPDS_5:47
.= s . (intpos 3) by A27, A10, AMI_3:52, SCMPDS_2:62 ;
then A28: (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 3) = s . (intpos 3) by SCMPDS_5:40;
then A29: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 3) = s . (intpos 3) by A21, AMI_3:52, SCMPDS_2:59;
A30: s . (intpos 4) >= 1 + (6 + (s . (intpos 6))) by A1;
then A31: (s . (intpos 4)) - 1 >= 6 + (s . (intpos 6)) by XREAL_1:21;
(Initialize s) . (intpos 2) = s . (intpos 2) by SCMPDS_5:40;
then A32: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos 2) = s . (intpos 2) by A8, AMI_3:52, SCMPDS_2:59;
(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos 2) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (intpos 2) by SCMPDS_5:47
.= s . (intpos 2) by A32, A10, AMI_3:52, SCMPDS_2:62 ;
then A33: (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 2) = s . (intpos 2) by SCMPDS_5:40;
then A34: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 2) = s . (intpos 2) by A21, AMI_3:52, SCMPDS_2:59;
(Initialize s) . (intpos 6) = s . (intpos 6) by SCMPDS_5:40;
then A35: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos 6) = s . (intpos 6) by A8, AMI_3:52, SCMPDS_2:59;
(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos 6) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (intpos 6) by SCMPDS_5:47
.= s . (intpos 6) by A35, A10, AMI_3:52, SCMPDS_2:62 ;
then (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 6) = s . (intpos 6) by SCMPDS_5:40;
then A36: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 6) = s . (intpos 6) by A21, AMI_3:52, SCMPDS_2:59;
A37: DataLoc ((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 = intpos (0 + 6) by A20, SCMP_GCD:5;

A38: now

assume (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 6) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 6) by SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 6) by SCMPDS_5:45
.= 0 by A37, SCMPDS_2:58 ;
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 )))),s) . (intpos 6) = 0 by SCMPDS_5:39; :: thesis: verum

end;

A39: 6 + (s . (intpos 6)) > 6 + 0 by A3, XREAL_1:8;
then 0 <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by A31, A25, ABSVALUE:def 1;
then A40: GBP <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1) by ZFMISC_1:33;
A41: (s . (intpos 4)) - 1 > 0 by A3, A30, XREAL_1:21;
then A42: abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) = (s . (intpos 4)) - 1 by A25, ABSVALUE:def 1;
then 4 <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by A31, A39, XXREAL_0:2;
then A43: intpos 4 <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1) by ZFMISC_1:33;
A44: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (intpos 4) by SCMPDS_5:47
.= s . (intpos 4) by A25, A43, SCMPDS_2:59 ;
then A45: abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) = s . (intpos 4) by A1, A4, ABSVALUE:def 1;
then 4 <> abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by A1, A4, XXREAL_0:2;
then A46: intpos 4 <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 by ZFMISC_1:33;
3 <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by A31, A39, A42, XXREAL_0:2;
then A47: intpos 3 <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1) by ZFMISC_1:33;
3 <> abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by A1, A4, A45, XXREAL_0:2;
then A48: intpos 3 <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 by ZFMISC_1:33;
A49: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (intpos 3) by SCMPDS_5:47
.= s . (intpos 3) by A29, A47, SCMPDS_2:59 ;
A50: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 3) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 3) by SCMPDS_5:46
.= s . (intpos 3) by A49, A48, SCMPDS_2:59 ;
2 <> abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by A1, A4, A45, XXREAL_0:2;
then A51: intpos 2 <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 by ZFMISC_1:33;
A52: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4) by SCMPDS_5:46
.= s . (intpos 4) by A44, A46, SCMPDS_2:59 ;
A53: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . GBP by SCMPDS_5:47
.= 0 by A22, A40, SCMPDS_2:59 ;
A54: (2 * (abs ((s . (intpos 4)) + (- 1)))) + 1 = (2 * ((s . (intpos 4)) - 1)) + 1 by A31, A39, ABSVALUE:def 1;
then abs ((s . (intpos 4)) + (- 1)) <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP ) + 5) by A3, A31, A11, XREAL_1:8;
then A55: DataLoc (s . (intpos 4)),(- 1) <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . GBP ),5 by ZFMISC_1:33;
0 <> abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by A1, A4, A44, ABSVALUE:def 1;
then A56: GBP <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 by ZFMISC_1:33;
A57: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . GBP by SCMPDS_5:46
.= 0 by A53, A56, SCMPDS_2:59 ;
then A58: GBP <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by AMI_3:52, SCMP_GCD:5;
2 <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by A31, A39, A42, XXREAL_0:2;
then A59: intpos 2 <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1) by ZFMISC_1:33;
A60: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (intpos 2) by SCMPDS_5:47
.= s . (intpos 2) by A34, A59, SCMPDS_2:59 ;
A61: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 2) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A60, A51, SCMPDS_2:59 ;
A62: intpos 2 <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by A57, AMI_3:52, SCMP_GCD:5;
(IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP = (Exec (AddTo GBP ,4,(- 1)),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . GBP by SCMPDS_5:46
.= 0 by A57, A58, SCMPDS_2:60 ;
then A63: DataLoc ((IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 = intpos (0 + 6) by SCMP_GCD:5;
then A64: abs (((IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 6) = 0 + 6 by ZFMISC_1:33;
A65: DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 = intpos (0 + 4) by A57, SCMP_GCD:5;
then A66: abs (((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 4) = 0 + 4 by ZFMISC_1:33;
then abs ((s . (intpos 4)) + (- 1)) <> abs (((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 4) by A31, A39, A54, XXREAL_0:2;
then A67: DataLoc (s . (intpos 4)),(- 1) <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by ZFMISC_1:33;
A68: (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A61, A62, SCMPDS_2:60 ;

now

per cases ( (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) <= 0 or (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) > 0 ) ;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 2) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 2) by SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 2) by SCMPDS_5:45
.= s . (intpos 2) by A33, A37, AMI_3:52, SCMPDS_2:58 ;
:: thesis: verum

end;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 2) by SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 2) by SCMPDS_5:46
.= s . (intpos 2) by A68, A63, AMI_3:52, SCMPDS_2:60 ;
:: 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 )))),s) . (intpos 2) = s . (intpos 2) by SCMPDS_5:39; :: 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) ) )
A69: intpos 3 <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by A57, AMI_3:52, SCMP_GCD:5;
A70: (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 3) by SCMPDS_5:46
.= s . (intpos 3) by A50, A69, SCMPDS_2:60 ;

now

per cases ( (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) <= 0 or (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) > 0 ) ;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 3) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 3) by SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 3) by SCMPDS_5:45
.= s . (intpos 3) by A28, A37, AMI_3:52, SCMPDS_2:58 ;
:: thesis: verum

end;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 3) by SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 3) by SCMPDS_5:46
.= s . (intpos 3) by A70, A63, AMI_3:52, SCMPDS_2:60 ;
:: 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 )))),s) . (intpos 3) = s . (intpos 3) by SCMPDS_5:39; :: 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) ) )
A71: intpos 6 <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by A57, AMI_3:52, SCMP_GCD:5;
6 <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by A30, A39, A42, XREAL_1:21;
then A72: intpos 6 <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1) by ZFMISC_1:33;
A73: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (intpos 6) by SCMPDS_5:47
.= s . (intpos 6) by A36, A72, SCMPDS_2:59 ;
6 <> abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by A1, A4, A45, XXREAL_0:2;
then A74: intpos 6 <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 by ZFMISC_1:33;
A75: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 6) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 6) by SCMPDS_5:46
.= s . (intpos 6) by A73, A74, SCMPDS_2:59 ;
A76: (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 6) by SCMPDS_5:46
.= s . (intpos 6) by A75, A71, SCMPDS_2:60 ;
A77: (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4) by SCMPDS_5:46
.= ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + (- 1) by A65, SCMPDS_2:60
.= (s . (intpos 4)) - 1 by A52 ;

A78: now

assume A79: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 )))),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 6) by SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 6) by SCMPDS_5:46
.= (s . (intpos 6)) + (- 1) by A76, A63, SCMPDS_2:60
.= (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 )))),s) . (intpos 6) = (s . (intpos 6)) - 1 by SCMPDS_5:39; :: 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 )))),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4) by A79, SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4) by SCMPDS_5:46
.= (s . (intpos 4)) - 1 by A77, A63, AMI_3:52, SCMPDS_2:60 ;
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 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 by SCMPDS_5:39; :: 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) ) )

per cases ( (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) <= 0 or (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) > 0 ) ;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 )))),s) . (intpos 6) < s . (intpos 6) by A3, A38; :: thesis: verum

end;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 )))),s) . (intpos 6) < s . (intpos 6) by A78, XREAL_1:148; :: 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) ) )

per cases ( (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) <= 0 or (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) > 0 ) ;

suppose A80: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 )))),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4) by SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4) by SCMPDS_5:45
.= s . (intpos 4) by A24, A37, AMI_3:52, SCMPDS_2:58 ;
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 )))),s) . (intpos 4) = s . (intpos 4) by SCMPDS_5:39;
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 )))),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 )))),s) . (intpos 6)) by A1, A4, A38, A80, XXREAL_0:2; :: thesis: verum

end;

suppose A81: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 )))),s) . (intpos 6))

(s . (intpos 4)) - 1 >= (7 + (s . (intpos 6))) - 1 by A1, XREAL_1:11;
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 )))),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 )))),s) . (intpos 6)) by A78, A81; :: thesis: verum

end;

end;

end;

A82: now

let i be Element of NAT ; :: thesis: ( i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) implies (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos i) = s . (intpos i) )
assume that
A83: i >= 7 and
i <> (s . (intpos 4)) - 1 and
i <> s . (intpos 4) ; :: thesis: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos i) = s . (intpos i)
i > 5 by A83, XXREAL_0:2;
hence (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos i) = (Initialize s) . (intpos i) by A8, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by SCMPDS_5:40 ;
:: thesis: verum

end;

A84: now

let i be Element of 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 )),s) . (intpos i) = s . (intpos i) )
assume that
A85: i >= 7 and
A86: ( i <> (s . (intpos 4)) - 1 & i <> s . (intpos 4) ) ; :: thesis: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos i) = s . (intpos i)
A87: i > 5 by A85, XXREAL_0:2;
thus (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos i) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (intpos i) by SCMPDS_5:47
.= (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (intpos i) by A10, A87, AMI_3:52, SCMPDS_2:62
.= s . (intpos i) by A82, A85, A86 ; :: thesis: verum

end;

A88: now

let i be Element of 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 )),s))) . (intpos i) = s . (intpos i) )
assume that
A89: i >= 7 and
A90: ( 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 )),s))) . (intpos i) = s . (intpos i)
i > 5 by A89, XXREAL_0:2;
hence (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos i) = (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by A21, AMI_3:52, SCMPDS_2:59
.= (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos i) by SCMPDS_5:40
.= s . (intpos i) by A84, A89, A90 ;
:: thesis: verum

end;

A91: now

let i be Element of 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 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = s . (intpos i) )
assume that
A92: i >= 7 and
A93: i <> (s . (intpos 4)) - 1 and
A94: i <> s . (intpos 4) ; :: thesis: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = s . (intpos i)
A95: intpos i <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s))) . (intpos 4)),(- 1) ; :: thesis: contradiction
then i = abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by ZFMISC_1:33;
hence contradiction by A41, A25, A93, ABSVALUE:def 1; :: thesis: verum

end;

thus (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (intpos i) by SCMPDS_5:47
.= (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos i) by A95, SCMPDS_2:59
.= s . (intpos i) by A88, A92, A93, A94 ; :: thesis: verum

end;

A96: now

let i be Element of 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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = s . (intpos i) )
assume that
A97: ( i >= 7 & i <> (s . (intpos 4)) - 1 ) and
A98: i <> s . (intpos 4) ; :: thesis: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = s . (intpos i)
A99: intpos i <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0

proof

assume intpos i = DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 ; :: thesis: contradiction
then i = abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by ZFMISC_1:33;
hence contradiction by A1, A4, A44, A98, ABSVALUE:def 1; :: thesis: verum

end;

thus (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos i) by SCMPDS_5:46
.= (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by A99, SCMPDS_2:59
.= s . (intpos i) by A91, A97, A98 ; :: thesis: verum

end;

A100: now

let i be Element of 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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = s . (intpos i) )
assume that
A101: i >= 7 and
A102: ( 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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = s . (intpos i)
i > 4 by A101, XXREAL_0:2;
then A103: intpos i <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by A57, AMI_3:52, SCMP_GCD:5;
thus (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos i) by SCMPDS_5:46
.= (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by A103, SCMPDS_2:60
.= s . (intpos i) by A96, A101, A102 ; :: 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos b₁) = s . (intpos b₁) )
A104: i in NAT by ORDINAL1:def 13;
set xi = intpos i;
assume that
A105: i >= 7 and
A106: ( 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 )))),s) . (intpos b₁) = s . (intpos b₁)
A107: i > 6 by A105, XXREAL_0:2;

per cases ( (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) <= 0 or (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) > 0 ) ;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos i) by SCMPDS_5:45
.= (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by A37, A107, AMI_3:52, SCMPDS_2:58
.= (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos i) by SCMPDS_5:40
.= s . (intpos i) by A84, A104, A105, A106 ;
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 )))),s) . (intpos i) = s . (intpos i) by SCMPDS_5:39; :: thesis: verum

end;

suppose (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )))),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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos i) by SCMPDS_5:46
.= (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos i) by A63, A107, AMI_3:52, SCMPDS_2:60
.= s . (intpos i) by A100, A104, A105, A106 ;
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 )))),s) . (intpos i) = s . (intpos i) by SCMPDS_5:39; :: thesis: verum

end;

end;

end;

A108: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (intpos 5) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (intpos 5) by SCMPDS_5:47
.= (s . (DataLoc (s . (intpos 4)),(- 1))) - (s . (DataLoc (s . (intpos 4)),0 )) by A17, A16, A14, A10, SCMPDS_2:62 ;
then A109: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . GBP ),5) = (s . (DataLoc (s . (intpos 4)),(- 1))) - (s . (DataLoc (s . (intpos 4)),0 )) by A19, SCMP_GCD:5;
abs ((s . (intpos 4)) + (- 1)) <> abs (((Initialize s) . GBP ) + 5) by A3, A31, A54, A13, XREAL_1:8;
then DataLoc (s . (intpos 4)),(- 1) <> DataLoc ((Initialize s) . GBP ),5 by ZFMISC_1:33;
then A110: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s)) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),(- 1)) by A6, SCMPDS_2:59;
(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s) . (DataLoc (s . (intpos 4)),(- 1)) = (Exec (SubFrom GBP ,5,(intpos 4),0 ),(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize s))) . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:47
.= s . (DataLoc (s . (intpos 4)),(- 1)) by A110, A55, SCMPDS_2:62 ;
then A111: (Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:40;
then A112: (Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 5) = s . (DataLoc (s . (intpos 4)),(- 1)) by A24, A21, SCMPDS_2:59;
5 <> abs (((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)) + (- 1)) by A31, A39, A42, XXREAL_0:2;
then A113: intpos 5 <> DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1) by ZFMISC_1:33;
A114: (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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 )),s)))) . (intpos 5) by SCMPDS_5:47
.= s . (DataLoc (s . (intpos 4)),(- 1)) by A112, A113, SCMPDS_2:59 ;
abs ((s . (intpos 4)) + 0 ) <> abs (((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 4) by A1, A4, A5, A66, XXREAL_0:2;
then A115: DataLoc (s . (intpos 4)),0 <> DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),4 by ZFMISC_1:33;
A116: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),0 ) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 ) by A44, SCMPDS_5:46
.= (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),5) by SCMPDS_2:59
.= s . (DataLoc (s . (intpos 4)),(- 1)) by A53, A114, SCMP_GCD:5 ;
A117: (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:46
.= s . (DataLoc (s . (intpos 4)),(- 1)) by A116, A115, SCMPDS_2:60 ;
abs ((s . (intpos 4)) + (- 1)) <> abs (((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)) + 0 ) by A54, A45;
then A118: DataLoc (s . (intpos 4)),(- 1) <> DataLoc ((IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (intpos 4)),0 by ZFMISC_1:33;
A119: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),(- 1)) = (Exec ((intpos 4),0 := GBP ,5),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:46
.= s . (DataLoc (s . (intpos 4)),0 ) by A26, A118, SCMPDS_2:59 ;
A120: (IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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)),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:46
.= s . (DataLoc (s . (intpos 4)),0 ) by A119, A67, SCMPDS_2:60 ;

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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) )

A121: 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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 by A31, A39, A54, A63, ZFMISC_1:33;
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 )))),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 )))),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 )))),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 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 )
then A122: (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:11;
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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),(- 1)) by A109, SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:46
.= s . (DataLoc (s . (intpos 4)),0 ) by A120, A121, SCMPDS_2:60 ;
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 )))),s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:39; :: 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 )))),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 )))),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 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 )
abs ((s . (intpos 4)) + 0 ) <> abs (((IExec ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 6) by A1, A4, A5, A64, XXREAL_0:2;
then A123: 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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 by ZFMISC_1:33;
(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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),0 ) by A109, A122, SCMPDS_6:87
.= (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))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:46
.= s . (DataLoc (s . (intpos 4)),(- 1)) by A117, A123, SCMPDS_2:60 ;
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 )))),s) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:39; :: 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 )))),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 )))),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 )))),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 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 ) by A19, A108, A78, A122, SCMP_GCD:5; :: thesis: verum

end;

A124: abs (((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 6) = 0 + 6 by A37, ZFMISC_1:33;

hereby :: thesis: verum

A125: DataLoc (s . (intpos 4)),(- 1) <> DataLoc ((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 by A31, A39, A54, A37, ZFMISC_1:33;
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 )))),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 )))),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 )))),s) . (intpos 6) = 0 )
then A126: (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:11;
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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),(- 1)) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),(- 1)) by A109, SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:45
.= s . (DataLoc (s . (intpos 4)),(- 1)) by A111, A125, SCMPDS_2:58 ;
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 )))),s) . (DataLoc (s . (intpos 4)),(- 1)) = s . (DataLoc (s . (intpos 4)),(- 1)) by SCMPDS_5:39; :: 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 )))),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 )))),s) . (intpos 6) = 0 )
abs ((s . (intpos 4)) + 0 ) <> abs (((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ) + 6) by A1, A4, A5, A124, XXREAL_0:2;
then A127: DataLoc (s . (intpos 4)),0 <> DataLoc ((Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 by ZFMISC_1:33;
(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 ))),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),0 ) = (IExec (Load (GBP ,6 := 0 )),(IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . (DataLoc (s . (intpos 4)),0 ) by A109, A126, SCMPDS_6:88
.= (Exec (GBP ,6 := 0 ),(Initialize (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:45
.= s . (DataLoc (s . (intpos 4)),0 ) by A18, A127, SCMPDS_2:58 ;
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 )))),s) . (DataLoc (s . (intpos 4)),0 ) = s . (DataLoc (s . (intpos 4)),0 ) by SCMPDS_5:39; :: 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 )))),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 )))),s) . (intpos 6) = 0 by A19, A108, A38, A126, SCMP_GCD:5; :: thesis: verum

end;