let P be Instruction-Sequence of SCMPDS; :: thesis:
set a = GBP ;
let s be 0 -started State of SCMPDS; :: thesis:
let md, me be 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 = s;
set Q0 = P;
set t1 = IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s);
set Q1 = P;
set t2 = IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s);
set t3 = IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s);
set Q2 = P;
set t4 = Exec (((GBP,7) := (GBP,5)),s);
set Q4 = P;
A6: s . GBP = 0 by A5;
A7: DataLoc ((s . GBP),7) = intpos (0 + 7) by A5, SCMP_GCD:1;
then A8: (Exec (((GBP,7) := (GBP,5)),s)) . GBP = 0 by A6, AMI_3:10, SCMPDS_2:47;
then A9: DataLoc (((Exec (((GBP,7) := (GBP,5)),s)) . GBP),5) = intpos (0 + 5) by SCMP_GCD:1;
A10: (Exec (((GBP,7) := (GBP,5)),s)) . (intpos 4) = me by A7, A2, AMI_3:10, SCMPDS_2:47;
A11: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 4) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos 4) by SCMPDS_5:42
.= me by A10, A9, AMI_3:10, SCMPDS_2:48 ;
then A12: DataLoc (((IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 4)),0) = intpos (me + 0) by SCMP_GCD:1;
A13: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . GBP = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . GBP by SCMPDS_5:42
.= 0 by A8, A9, AMI_3:10, SCMPDS_2:48 ;
then A14: DataLoc (((IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:1;
A15: (Exec (((GBP,7) := (GBP,5)),s)) . (intpos 2) = md by A7, A1, AMI_3:10, SCMPDS_2:47;
A16: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 2) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos 2) by SCMPDS_5:42
.= md by A15, A9, AMI_3:10, SCMPDS_2:48 ;
A17: (Exec (((GBP,7) := (GBP,5)),s)) . (intpos 5) = s . (intpos 5) by A7, AMI_3:10, SCMPDS_2:47;
set t01 = Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)));
set ii7 = (GBP,5) := 0;
set t5 = Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))));
A18: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 2) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 2) by SCMPDS_5:41
.= md by A16, A14, AMI_3:10, SCMPDS_2:47 ;
A19: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . GBP = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . GBP by SCMPDS_5:41
.= 0 by A13, A14, AMI_3:10, SCMPDS_2:47 ;
then A20: DataLoc (((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:1;
DataLoc ((s . GBP),5) = intpos (0 + 5) by A6, SCMP_GCD:1;
then A21: (Exec (((GBP,7) := (GBP,5)),s)) . (intpos 7) = s . (intpos 5) by A7, SCMPDS_2:47;
A22: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 7) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos 7) by SCMPDS_5:42
.= s . (intpos 5) by A21, A9, AMI_3:10, SCMPDS_2:48 ;
A23: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 7) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 7) by SCMPDS_5:41
.= s . (intpos 5) by A22, A14, AMI_3:10, SCMPDS_2:47 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 7) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 7) by SCMPDS_5:41
.= s . (intpos 5) by A23, A20, AMI_3:10, SCMPDS_2:50 ;
then A24: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 7) = s . (intpos 5) by SCMPDS_5:15;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 2) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 2) by SCMPDS_5:41
.= md by A18, A20, AMI_3:10, SCMPDS_2:50 ;
then A25: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 2) = s . (intpos 2) by A1, SCMPDS_5:15;

A26: now :: thesis:

let i be Nat; :: thesis:
assume i >= 8 ; :: thesis:
then i > 7 by XXREAL_0:2;
hence (Exec (((GBP,7) := (GBP,5)),s)) . (intpos i) = s . (intpos i) by A7, AMI_3:10, SCMPDS_2:47; :: thesis:

end;

A27: now :: thesis:

let i be Nat; :: thesis:
assume A28: i >= 8 ; :: thesis:
then A29: i > 5 by XXREAL_0:2;
thus (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos i) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos i) by SCMPDS_5:42
.= (Exec (((GBP,7) := (GBP,5)),s)) . (intpos i) by A9, A29, AMI_3:10, SCMPDS_2:48
.= s . (intpos i) by A26, A28 ; :: thesis:

end;

A30: now :: thesis:

let i be Nat; :: thesis:
assume A31: i >= 8 ; :: thesis:
then A32: i > 6 by XXREAL_0:2;
thus (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos i) by SCMPDS_5:41
.= (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos i) by A14, A32, AMI_3:10, SCMPDS_2:47
.= s . (intpos i) by A27, A31 ; :: thesis:

end;

A33: now :: thesis:

let i be Nat; :: thesis:
assume A34: i >= 8 ; :: thesis:
then A35: 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))),P,s)) . (intpos i) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos i) by SCMPDS_5:41
.= (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos i) by A20, A35, AMI_3:10, SCMPDS_2:50
.= s . (intpos i) by A30, A34 ; :: thesis:

end;

A36: (Exec (((GBP,7) := (GBP,5)),s)) . (intpos 3) = s . (intpos 3) by A7, AMI_3:10, SCMPDS_2:47;
A37: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 3) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos 3) by SCMPDS_5:42
.= s . (intpos 3) by A36, A9, AMI_3:10, SCMPDS_2:48 ;
A38: (Exec (((GBP,7) := (GBP,5)),s)) . (intpos 1) = s . (intpos 1) by A7, AMI_3:10, SCMPDS_2:47;
A39: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 1) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos 1) by SCMPDS_5:42
.= s . (intpos 1) by A38, A9, AMI_3:10, SCMPDS_2:48 ;
A40: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 1) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 1) by SCMPDS_5:41
.= s . (intpos 1) by A39, A14, AMI_3:10, SCMPDS_2:47 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 1) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 1) by SCMPDS_5:41
.= s . (intpos 1) by A40, A20, AMI_3:10, SCMPDS_2:50 ;
then A41: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 1) = s . (intpos 1) by SCMPDS_5:15;
A42: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 3) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 3) by SCMPDS_5:41
.= s . (intpos 3) by A37, A14, AMI_3:10, SCMPDS_2:47 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 3) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 3) by SCMPDS_5:41
.= s . (intpos 3) by A42, A20, AMI_3:10, SCMPDS_2:50 ;
then A43: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 3) = s . (intpos 3) by SCMPDS_5:15;
A44: (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . GBP = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . GBP by SCMPDS_5:41
.= 0 by A19, A20, AMI_3:10, SCMPDS_2:50 ;
then A45: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP = 0 by SCMPDS_5:15;
then A46: DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),5) = intpos (0 + 5) by SCMP_GCD:1;
intpos 3 <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
then A47: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 3) = s . (intpos 3) by A43, SCMPDS_2:48;
intpos 2 <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
then A48: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 2) = s . (intpos 2) by A25, SCMPDS_2:48;
GBP <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
then A49: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . GBP = 0 by A45, SCMPDS_2:48;
then A50: DataLoc (((Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . GBP),7) = intpos (0 + 7) by SCMP_GCD:1;
A51: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 6) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 6) by SCMPDS_5:41
.= (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos me) by A14, A12, SCMPDS_2:47
.= s . (intpos me) by A4, A27 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 6) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 6) by SCMPDS_5:41
.= ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 6)) - ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (DataLoc (((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 2)),0))) by A20, SCMPDS_2:50
.= ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 6)) - ((IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos (md + 0))) by A18, SCMP_GCD:1
.= (s . (intpos me)) - (s . (intpos md)) by A3, A51, A30 ;
then A52: (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . GBP),6)) = (s . (intpos me)) - (s . (intpos md)) by A44, SCMP_GCD:1;
intpos 1 <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
then A53: (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 1) = s . (intpos 1) by A41, SCMPDS_2:48;

A54: now :: thesis:

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

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

hence (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . GBP = (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . GBP by SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . GBP by SCMPDS_5:40
.= 0 by A45, A46, AMI_3:10, SCMPDS_2:46 ;
:: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 1) = (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 1) by A55, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 1) by SCMPDS_5:40
.= s . (intpos 1) by A41, A46, AMI_3:10, SCMPDS_2:46 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 2) = (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 2) by A55, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 2) by SCMPDS_5:40
.= s . (intpos 2) by A25, A46, AMI_3:10, SCMPDS_2:46 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 3) = (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 3) by A55, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 3) by SCMPDS_5:40
.= s . (intpos 3) by A43, A46, AMI_3:10, SCMPDS_2:46 ; :: thesis:
let i be Nat; :: thesis:
assume A56: i >= 8 ; :: thesis:
then A57: 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))))),P,s)) . (intpos i) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos i) by SCMPDS_5:35
.= (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos i) by A55, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos i) by SCMPDS_5:40
.= (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos i) by A46, A57, AMI_3:10, SCMPDS_2:46
.= (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos i) by SCMPDS_5:15
.= s . (intpos i) by A33, A56 ; :: thesis:

end;

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

thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . GBP = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . GBP by A58, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . GBP by SCMPDS_5:42
.= 0 by A49, A50, AMI_3:10, SCMPDS_2:48 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 1) = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 1) by A58, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos 1) by SCMPDS_5:42
.= s . (intpos 1) by A53, A50, AMI_3:10, SCMPDS_2:48 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 2) = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 2) by A58, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos 2) by SCMPDS_5:42
.= s . (intpos 2) by A48, A50, AMI_3:10, SCMPDS_2:48 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 3) = (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 3) by A58, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos 3) by SCMPDS_5:42
.= s . (intpos 3) by A47, A50, AMI_3:10, SCMPDS_2:48 ; :: thesis:
let i be Nat; :: thesis:
assume A59: i >= 8 ; :: thesis:
then A60: i > 7 by XXREAL_0:2;
i > 4 by A59, XXREAL_0:2;
then A61: intpos i <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
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))))),P,s)) . (intpos i) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos i) by SCMPDS_5:35
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos i) by A58, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos i) by SCMPDS_5:42
.= (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos i) by A50, A60, AMI_3:10, SCMPDS_2:48
.= (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos i) by A61, SCMPDS_2:48
.= (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos i) by SCMPDS_5:15
.= s . (intpos i) by A33, A59 ; :: 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))))),P,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))))),P,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))))),P,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))))),P,s)) . (intpos 3) = s . (intpos 3) ) by SCMPDS_5:35; :: thesis:
thus for i being 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))))),P,s)) . (intpos i) = s . (intpos i) by A54; :: thesis:
A62: (IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)) . (intpos 5) = (Exec ((AddTo (GBP,5,(- 1))),(Exec (((GBP,7) := (GBP,5)),s)))) . (intpos 5) by SCMPDS_5:42
.= ((Exec (((GBP,7) := (GBP,5)),s)) . (intpos 5)) + (- 1) by A9, SCMPDS_2:48
.= (s . (intpos 5)) - 1 by A17 ;
A63: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 5) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 5) by SCMPDS_5:41
.= (s . (intpos 5)) - 1 by A62, A14, AMI_3:10, SCMPDS_2:47 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 5) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 5) by SCMPDS_5:41
.= (s . (intpos 5)) - 1 by A63, A20, AMI_3:10, SCMPDS_2:50 ;
then A64: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 5) = (s . (intpos 5)) - 1 by SCMPDS_5:15;
A65: (IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)) . (intpos 4) = (Exec (((GBP,6) := ((intpos 4),0)),(IExec ((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))),P,s)))) . (intpos 4) by SCMPDS_5:41
.= me by A11, A14, AMI_3:10, SCMPDS_2:47 ;
(IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (intpos 4) = (Exec ((SubFrom (GBP,6,(intpos 2),0)),(IExec (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))),P,s)))) . (intpos 4) by SCMPDS_5:41
.= me by A65, A20, AMI_3:10, SCMPDS_2:50 ;
then A66: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 4) = s . (intpos 4) by A2, SCMPDS_5:15;
A67: DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) = intpos (0 + 4) by A45, SCMP_GCD:1;
A68: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),6)) = (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . GBP),6)) by SCMPDS_5:15
.= (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . GBP),6)) by SCMPDS_5:15 ;

hereby :: thesis:

A69: intpos 5 <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
assume s . (intpos md) < s . (intpos me) ; :: thesis:
then A70: 0 < (s . (intpos me)) - (s . (intpos md)) by XREAL_1:50;
A71: (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),6)) = (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . GBP),6)) by SCMPDS_5:15
.= (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . (DataLoc (((IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)) . GBP),6)) by SCMPDS_5:15 ;
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))))),P,s)) . (intpos 5) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 5) by SCMPDS_5:35
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 5) by A52, A70, A71, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos 5) by SCMPDS_5:42
.= (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 5) by A50, AMI_3:10, SCMPDS_2:48
.= (s . (intpos 5)) - 1 by A64, A69, SCMPDS_2:48 ; :: 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))))),P,s)) . (intpos 4) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))))) . (intpos 4) by SCMPDS_5:35
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))))) . (intpos 4) by A52, A71, A70, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos 4) by SCMPDS_5:42
.= (Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 4) by A50, AMI_3:10, SCMPDS_2:48
.= ((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . (intpos 4)) + (- 1) by A67, SCMPDS_2:48
.= (s . (intpos 4)) - 1 by A66 ; :: thesis:
A72: intpos 7 <> DataLoc (((Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))) . GBP),4) by A45, AMI_3:10, SCMP_GCD:1;
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))))),P,s)) . (intpos 7) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 7) by SCMPDS_5:35
.= (IExec (((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 7) by A52, A71, A70, SCMPDS_6:73
.= (Exec ((AddTo (GBP,7,(- 1))),(Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))))) . (intpos 7) by SCMPDS_5:42
.= ((Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 7)) + (- 1) by A50, SCMPDS_2:48
.= ((Exec ((AddTo (GBP,4,(- 1))),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 7)) - 1
.= (s . (intpos 5)) - 1 by A24, A72, SCMPDS_2:48 ; :: thesis:

end;

assume s . (intpos md) >= s . (intpos me) ; :: thesis:
then A73: (s . (intpos me)) - (s . (intpos md)) <= 0 by XREAL_1:47;
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))))),P,s)) . (intpos 5) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 5) by SCMPDS_5:35
.= (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 5) by A52, A68, A73, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 5) by SCMPDS_5:40
.= 0 by A46, SCMPDS_2:46 ; :: 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))))),P,s)) . (intpos 4) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 4) by SCMPDS_5:35
.= (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 4) by A52, A68, A73, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 4) by SCMPDS_5:40
.= s . (intpos 4) by A46, A66, AMI_3:10, SCMPDS_2:46 ; :: 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))))),P,s)) . (intpos 7) = (IExec ((if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 7) by SCMPDS_5:35
.= (IExec ((Load ((GBP,5) := 0)),P,(Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s))))) . (intpos 7) by A52, A68, A73, SCMPDS_6:74
.= (Exec (((GBP,5) := 0),(Initialize (Initialize (IExec ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))),P,s)))))) . (intpos 7) by SCMPDS_5:40
.= s . (intpos 5) by A24, A46, AMI_3:10, SCMPDS_2:46 ; :: thesis: