set a = GBP ;
let s be 0 -started State of SCMPDS; :: thesis:
let md, me be Element of NAT ; :: thesis:
assume that
A1: s . (intpos 2) = md and
A2: s . (intpos 4) = me and
A3: md >= 8 and
A4: me >= 8 and
A5: s . GBP = 0 ; :: thesis:
set t0 = Initialize s;
set t1 = IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s);
set t2 = IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s);
set t3 = IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s);
set t4 = Exec (((GBP,7) := (GBP,5)),(Initialize s));
A6: (Initialize s) . GBP = 0 by A5, SCMPDS_5:40;
then A7: DataLoc (((Initialize s) . GBP),7) = intpos (0 + 7) by SCMP_GCD:5;
then A8: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . GBP = 0 by A6, AMI_3:52, SCMPDS_2:59;
then A9: DataLoc (((Exec (((GBP,7) := (GBP,5)),(Initialize s))) . GBP),5) = intpos (0 + 5) by SCMP_GCD:5;
(Initialize s) . (intpos 4) = me by A2, SCMPDS_5:40;
then A10: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 4) = me by A7, AMI_3:52, SCMPDS_2:59;
A11: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 4) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos 4) by SCMPDS_5:47
.= me by A10, A9, AMI_3:52, SCMPDS_2:60 ;
then A12: DataLoc (((IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 4)),0) = intpos (me + 0) by SCMP_GCD:5;
A13: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . GBP = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . GBP by SCMPDS_5:47
.= 0 by A8, A9, AMI_3:52, SCMPDS_2:60 ;
then A14: DataLoc (((IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:5;
(Initialize s) . (intpos 2) = md by A1, SCMPDS_5:40;
then A15: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 2) = md by A7, AMI_3:52, SCMPDS_2:59;
A16: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 2) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos 2) by SCMPDS_5:47
.= md by A15, A9, AMI_3:52, SCMPDS_2:60 ;
A17: (Initialize s) . (intpos 5) = s . (intpos 5) by SCMPDS_5:40;
then A18: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 5) = s . (intpos 5) by A7, AMI_3:52, SCMPDS_2:59;
set t01 = Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s));
set ii7 = (GBP,5) := 0;
set t5 = Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))));
A19: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 2) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 2) by SCMPDS_5:46
.= md by A16, A14, AMI_3:52, SCMPDS_2:59 ;
A20: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . GBP = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . GBP by SCMPDS_5:46
.= 0 by A13, A14, AMI_3:52, SCMPDS_2:59 ;
then A21: DataLoc (((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:5;
DataLoc (((Initialize s) . GBP),5) = intpos (0 + 5) by A6, SCMP_GCD:5;
then A22: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 7) = s . (intpos 5) by A17, A7, SCMPDS_2:59;
A23: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 7) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos 7) by SCMPDS_5:47
.= s . (intpos 5) by A22, A9, AMI_3:52, SCMPDS_2:60 ;
A24: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 7) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 7) by SCMPDS_5:46
.= s . (intpos 5) by A23, A14, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 7) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 7) by SCMPDS_5:46
.= s . (intpos 5) by A24, A21, AMI_3:52, SCMPDS_2:62 ;
then A25: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 7) = s . (intpos 5) by SCMPDS_5:40;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 2) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 2) by SCMPDS_5:46
.= md by A19, A21, AMI_3:52, SCMPDS_2:62 ;
then A26: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 2) = s . (intpos 2) by A1, SCMPDS_5:40;

A27: now

let i be Element of NAT ; :: thesis:
assume i >= 8 ; :: thesis:
then i > 7 by XXREAL_0:2;
hence (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos i) = (Initialize s) . (intpos i) by A7, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by SCMPDS_5:40 ;
:: thesis:

end;

A28: now

let i be Element of NAT ; :: thesis:
assume A29: i >= 8 ; :: thesis:
then A30: i > 5 by XXREAL_0:2;
thus (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos i) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos i) by SCMPDS_5:47
.= (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos i) by A9, A30, AMI_3:52, SCMPDS_2:60
.= s . (intpos i) by A27, A29 ; :: thesis:

end;

A31: now

let i be Element of NAT ; :: thesis:
assume A32: i >= 8 ; :: thesis:
then A33: i > 6 by XXREAL_0:2;
thus (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos i) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos i) by SCMPDS_5:46
.= (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos i) by A14, A33, AMI_3:52, SCMPDS_2:59
.= s . (intpos i) by A28, A32 ; :: thesis:

end;

A34: now

let i be Element of NAT ; :: thesis:
assume A35: i >= 8 ; :: thesis:
then A36: i > 6 by XXREAL_0:2;
thus (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos i) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos i) by SCMPDS_5:46
.= (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos i) by A21, A36, AMI_3:52, SCMPDS_2:62
.= s . (intpos i) by A31, A35 ; :: thesis:

end;

(Initialize s) . (intpos 3) = s . (intpos 3) by SCMPDS_5:40;
then A37: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 3) = s . (intpos 3) by A7, AMI_3:52, SCMPDS_2:59;
A38: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 3) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos 3) by SCMPDS_5:47
.= s . (intpos 3) by A37, A9, AMI_3:52, SCMPDS_2:60 ;
(Initialize s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
then A39: (Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 1) = s . (intpos 1) by A7, AMI_3:52, SCMPDS_2:59;
A40: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 1) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos 1) by SCMPDS_5:47
.= s . (intpos 1) by A39, A9, AMI_3:52, SCMPDS_2:60 ;
A41: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 1) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A40, A14, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 1) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A41, A21, AMI_3:52, SCMPDS_2:62 ;
then A42: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
A43: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 3) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 3) by SCMPDS_5:46
.= s . (intpos 3) by A38, A14, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 3) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 3) by SCMPDS_5:46
.= s . (intpos 3) by A43, A21, AMI_3:52, SCMPDS_2:62 ;
then A44: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 3) = s . (intpos 3) by SCMPDS_5:40;
A45: (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . GBP = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . GBP by SCMPDS_5:46
.= 0 by A20, A21, AMI_3:52, SCMPDS_2:62 ;
then A46: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP = 0 by SCMPDS_5:40;
then A47: DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),5) = intpos (0 + 5) by SCMP_GCD:5;
intpos 3 <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
then A48: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 3) = s . (intpos 3) by A44, SCMPDS_2:60;
intpos 2 <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
then A49: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 2) = s . (intpos 2) by A26, SCMPDS_2:60;
GBP <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
then A50: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . GBP = 0 by A46, SCMPDS_2:60;
then A51: DataLoc (((Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . GBP),7) = intpos (0 + 7) by SCMP_GCD:5;
A52: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 6) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 6) by SCMPDS_5:46
.= (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos me) by A14, A12, SCMPDS_2:59
.= s . (intpos me) by A4, A28 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 6) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 6) by SCMPDS_5:46
.= ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 6)) - ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (DataLoc (((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 2)),0))) by A21, SCMPDS_2:62
.= ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 6)) - ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos (md + 0))) by A19, SCMP_GCD:5
.= (s . (intpos me)) - (s . (intpos md)) by A3, A52, A31 ;
then A53: (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . GBP),6)) = (s . (intpos me)) - (s . (intpos md)) by A45, SCMP_GCD:5;
intpos 1 <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
then A54: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 1) = s . (intpos 1) by A42, SCMPDS_2:60;
X4: IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) = IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) by SCMPDS_5:48;

A55: now

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

suppose A56: (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . GBP),6)) <= 0 ; :: thesis:

hence (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . GBP = (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . GBP by SCMPDS_6:88
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . GBP by SCMPDS_5:45
.= 0 by A46, A47, AMI_3:52, SCMPDS_2:58 ;
:: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 1) = (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 1) by A56, SCMPDS_6:88
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 1) by SCMPDS_5:45
.= s . (intpos 1) by A42, A47, AMI_3:52, SCMPDS_2:58 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 2) = (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 2) by A56, SCMPDS_6:88
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 2) by SCMPDS_5:45
.= s . (intpos 2) by A26, A47, AMI_3:52, SCMPDS_2:58 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 3) = (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 3) by A56, SCMPDS_6:88
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 3) by SCMPDS_5:45
.= s . (intpos 3) by A44, A47, AMI_3:52, SCMPDS_2:58 ; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A57: i >= 8 ; :: thesis:
then A58: i > 5 by XXREAL_0:2;
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos i) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos i) by SCMPDS_5:39
.= (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos i) by A56, SCMPDS_6:88
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos i) by SCMPDS_5:45
.= (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos i) by A47, A58, AMI_3:52, SCMPDS_2:58
.= (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos i) by SCMPDS_5:40
.= s . (intpos i) by A34, A57 ; :: thesis:

end;

suppose A59: (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . GBP),6)) > 0 ; :: thesis:

thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . GBP = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . GBP by A59, SCMPDS_6:87
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . GBP by X4, SCMPDS_5:47
.= 0 by A50, A51, AMI_3:52, SCMPDS_2:60 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 1) = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 1) by A59, SCMPDS_6:87
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos 1) by X4, SCMPDS_5:47
.= s . (intpos 1) by A54, A51, AMI_3:52, SCMPDS_2:60 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 2) = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 2) by A59, SCMPDS_6:87
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos 2) by X4, SCMPDS_5:47
.= s . (intpos 2) by A49, A51, AMI_3:52, SCMPDS_2:60 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 3) = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 3) by A59, SCMPDS_6:87
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos 3) by X4, SCMPDS_5:47
.= s . (intpos 3) by A48, A51, AMI_3:52, SCMPDS_2:60 ; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A60: i >= 8 ; :: thesis:
then A61: i > 7 by XXREAL_0:2;
i > 4 by A60, XXREAL_0:2;
then A62: intpos i <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos i) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos i) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos i) by A59, SCMPDS_6:87
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos i) by X4, SCMPDS_5:47
.= (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos i) by A51, A61, AMI_3:52, SCMPDS_2:60
.= (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos i) by A62, SCMPDS_2:60
.= (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos i) by SCMPDS_5:40
.= s . (intpos i) by A34, A60 ; :: thesis:

end;

hence ( (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . GBP = 0 & (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 1) = s . (intpos 1) & (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 2) = s . (intpos 2) & (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 3) = s . (intpos 3) ) by SCMPDS_5:39; :: thesis:
thus for i being Element of NAT st i >= 8 holds
(IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos i) = s . (intpos i) by A55; :: thesis:
A63: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)) . (intpos 5) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),(Initialize s))))) . (intpos 5) by SCMPDS_5:47
.= ((Exec (((GBP,7) := (GBP,5)),(Initialize s))) . (intpos 5)) + (- 1) by A9, SCMPDS_2:60
.= (s . (intpos 5)) - 1 by A18 ;
A64: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 5) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 5) by SCMPDS_5:46
.= (s . (intpos 5)) - 1 by A63, A14, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 5) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 5) by SCMPDS_5:46
.= (s . (intpos 5)) - 1 by A64, A21, AMI_3:52, SCMPDS_2:62 ;
then A65: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 5) = (s . (intpos 5)) - 1 by SCMPDS_5:40;
A66: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)) . (intpos 4) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),s)))) . (intpos 4) by SCMPDS_5:46
.= me by A11, A14, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)) . (intpos 4) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),s)))) . (intpos 4) by SCMPDS_5:46
.= me by A66, A21, AMI_3:52, SCMPDS_2:62 ;
then A67: (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 4) = s . (intpos 4) by A2, SCMPDS_5:40;
A68: DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) = intpos (0 + 4) by A46, SCMP_GCD:5;

hereby :: thesis:

A69: intpos 5 <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
assume A70: s . (intpos md) < s . (intpos me) ; :: thesis:
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 5) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 5) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 5) by A53, A70, SCMPDS_6:87, XREAL_1:52
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos 5) by X4, SCMPDS_5:47
.= (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 5) by A51, AMI_3:52, SCMPDS_2:60
.= (s . (intpos 5)) - 1 by A65, A69, SCMPDS_2:60 ; :: thesis:
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 4) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 4) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 4) by A53, A70, SCMPDS_6:87, XREAL_1:52
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos 4) by X4, SCMPDS_5:47
.= (Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 4) by A51, AMI_3:52, SCMPDS_2:60
.= ((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . (intpos 4)) + (- 1) by A68, SCMPDS_2:60
.= (s . (intpos 4)) - 1 by A67 ; :: thesis:
A71: intpos 7 <> DataLoc (((Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))) . GBP),4) by A46, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 7) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 7) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 7) by A53, A70, SCMPDS_6:87, XREAL_1:52
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))))) . (intpos 7) by X4, SCMPDS_5:47
.= ((Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 7)) + (- 1) by A51, SCMPDS_2:60
.= ((Exec ((AddTo (GBP,4,(- 1))),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 7)) - 1
.= (s . (intpos 5)) - 1 by A25, A71, SCMPDS_2:60 ; :: thesis:

end;

hereby :: thesis:

assume A72: s . (intpos md) >= s . (intpos me) ; :: thesis:
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 5) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 5) by SCMPDS_5:39
.= (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 5) by A53, A72, SCMPDS_6:88, XREAL_1:49
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 5) by SCMPDS_5:45
.= 0 by A47, SCMPDS_2:58 ; :: thesis:
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 4) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 4) by SCMPDS_5:39
.= (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 4) by A53, A72, SCMPDS_6:88, XREAL_1:49
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 4) by SCMPDS_5:45
.= s . (intpos 4) by A47, A67, AMI_3:52, SCMPDS_2:58 ; :: thesis:
thus (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),s)) . (intpos 7) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 7) by SCMPDS_5:39
.= (IExec ((Load ((GBP,5) := 0)),(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s)))) . (intpos 7) by A53, A72, SCMPDS_6:88, XREAL_1:49
.= (Exec (((GBP,5) := 0),(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),s))))) . (intpos 7) by SCMPDS_5:45
.= s . (intpos 5) by A25, A47, AMI_3:52, SCMPDS_2:58 ; :: thesis:

end;