let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
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 3) = me and
A3: md >= 8 and
A4: me >= 8 and
A5: s . GBP = 0 ; :: thesis:
set t0 = Initialize s;
set t1 = IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s);
set Q1 = P;
set t2 = IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s);
set t3 = IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s);
set t4 = Exec (((GBP,5) := (GBP,7)),(Initialize s));
A6: IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) = IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) by SCMPDS_5:48;
A7: (Initialize s) . GBP = 0 by A5, SCMPDS_5:40;
then A8: DataLoc (((Initialize s) . GBP),5) = intpos (0 + 5) by SCMP_GCD:5;
then A9: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . GBP = 0 by A7, AMI_3:52, SCMPDS_2:59;
then A10: DataLoc (((Exec (((GBP,5) := (GBP,7)),(Initialize s))) . GBP),7) = intpos (0 + 7) by SCMP_GCD:5;
(Initialize s) . (intpos 2) = md by A1, SCMPDS_5:40;
then A11: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 2) = md by A8, AMI_3:52, SCMPDS_2:59;
A12: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 2) = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . (intpos 2) by SCMPDS_5:47
.= md by A11, A10, AMI_3:52, SCMPDS_2:60 ;
then A13: DataLoc (((IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 2)),0) = intpos (md + 0) by SCMP_GCD:5;
A14: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . GBP = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . GBP by SCMPDS_5:47
.= 0 by A9, A10, AMI_3:52, SCMPDS_2:60 ;
then A15: DataLoc (((IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:5;
(Initialize s) . (intpos 3) = me by A2, SCMPDS_5:40;
then A16: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 3) = me by A8, AMI_3:52, SCMPDS_2:59;
A17: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 3) = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . (intpos 3) by SCMPDS_5:47
.= me by A16, A10, AMI_3:52, SCMPDS_2:60 ;
A18: (Initialize s) . (intpos 7) = s . (intpos 7) by SCMPDS_5:40;
then A19: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 7) = s . (intpos 7) by A8, AMI_3:52, SCMPDS_2:59;
set t01 = Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s));
set jj7 = (GBP,7) := 0;
set t5 = Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))));
U: Initialize (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) = Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) ;
A20: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 3) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 3) by SCMPDS_5:46
.= me by A17, A15, AMI_3:52, SCMPDS_2:59 ;
A21: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . GBP = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . GBP by SCMPDS_5:46
.= 0 by A14, A15, AMI_3:52, SCMPDS_2:59 ;
then A22: DataLoc (((IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . GBP),6) = intpos (0 + 6) by SCMP_GCD:5;
(Initialize s) . (intpos 4) = s . (intpos 4) by SCMPDS_5:40;
then A23: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 4) = s . (intpos 4) by A8, AMI_3:52, SCMPDS_2:59;
A24: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 4) = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . (intpos 4) by SCMPDS_5:47
.= s . (intpos 4) by A23, A10, AMI_3:52, SCMPDS_2:60 ;
(Initialize s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
then A25: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 1) = s . (intpos 1) by A8, AMI_3:52, SCMPDS_2:59;
A26: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 1) = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . (intpos 1) by SCMPDS_5:47
.= s . (intpos 1) by A25, A10, AMI_3:52, SCMPDS_2:60 ;
A27: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 1) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A26, A15, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 1) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 1) by SCMPDS_5:46
.= s . (intpos 1) by A27, A22, AMI_3:52, SCMPDS_2:62 ;
then A28: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos 1) = s . (intpos 1) by SCMPDS_5:40;
A29: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 4) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 4) by SCMPDS_5:46
.= s . (intpos 4) by A24, A15, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 4) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 4) by SCMPDS_5:46
.= s . (intpos 4) by A29, A22, AMI_3:52, SCMPDS_2:62 ;
then A30: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos 4) = s . (intpos 4) by SCMPDS_5:40;
A31: (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . GBP = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . GBP by SCMPDS_5:46
.= 0 by A21, A22, AMI_3:52, SCMPDS_2:62 ;
then A32: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP = 0 by SCMPDS_5:40;
then A33: DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),7) = intpos (0 + 7) by SCMP_GCD:5;
DataLoc (((Initialize s) . GBP),7) = intpos (0 + 7) by A7, SCMP_GCD:5;
then A34: (Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 5) = s . (intpos 7) by A18, A8, SCMPDS_2:59;
A35: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 5) = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . (intpos 5) by SCMPDS_5:47
.= s . (intpos 7) by A34, A10, AMI_3:52, SCMPDS_2:60 ;
A36: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 5) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 5) by SCMPDS_5:46
.= s . (intpos 7) by A35, A15, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 5) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 5) by SCMPDS_5:46
.= s . (intpos 7) by A36, A22, AMI_3:52, SCMPDS_2:62 ;
then A37: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos 5) = s . (intpos 7) by SCMPDS_5:40;
A38: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 2) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 2) by SCMPDS_5:46
.= md by A12, A15, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 2) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 2) by SCMPDS_5:46
.= md by A38, A22, AMI_3:52, SCMPDS_2:62 ;
then A39: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos 2) = s . (intpos 2) by A1, SCMPDS_5:40;
intpos 4 <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
then A40: (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 4) = s . (intpos 4) by A30, SCMPDS_2:60;
intpos 2 <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
then A41: (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 2) = s . (intpos 2) by A39, SCMPDS_2:60;
GBP <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
then A42: (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . GBP = 0 by A32, SCMPDS_2:60;
then A43: DataLoc (((Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . GBP),5) = intpos (0 + 5) by SCMP_GCD:5;

A44: now

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

end;

A45: now

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

end;

A48: now

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

end;

A51: now

let i be Element of NAT ; :: thesis:
assume A52: i >= 8 ; :: thesis:
then A53: i > 6 by XXREAL_0:2;
thus (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos i) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos i) by SCMPDS_5:46
.= (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos i) by A22, A53, AMI_3:52, SCMPDS_2:62
.= s . (intpos i) by A48, A52 ; :: thesis:

end;

A54: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 6) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 6) by SCMPDS_5:46
.= (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos md) by A15, A13, SCMPDS_2:59
.= s . (intpos md) by A3, A45 ;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 6) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 6) by SCMPDS_5:46
.= ((IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 6)) - ((IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (DataLoc (((IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 3)),0))) by A22, SCMPDS_2:62
.= ((IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 6)) - ((IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos (me + 0))) by A20, SCMP_GCD:5
.= (s . (intpos md)) - (s . (intpos me)) by A4, A54, A48 ;
then A55: (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (DataLoc (((IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . GBP),6)) = (s . (intpos md)) - (s . (intpos me)) by A31, SCMP_GCD:5;
intpos 1 <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
then A56: (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 1) = s . (intpos 1) by A28, SCMPDS_2:60;

A57: now

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

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

hence (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . GBP = (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . GBP by SCMPDS_6:88
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . GBP by SCMPDS_5:45
.= 0 by A32, A33, AMI_3:52, SCMPDS_2:58 ;
:: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 1) = (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 1) by A58, SCMPDS_6:88
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 1) by SCMPDS_5:45
.= s . (intpos 1) by A28, A33, AMI_3:52, SCMPDS_2:58 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 2) = (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 2) by A58, SCMPDS_6:88
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 2) by SCMPDS_5:45
.= s . (intpos 2) by A39, A33, AMI_3:52, SCMPDS_2:58 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 4) = (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 4) by A58, SCMPDS_6:88
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 4) by SCMPDS_5:45
.= s . (intpos 4) by A30, A33, AMI_3:52, SCMPDS_2:58 ; :: thesis:

hereby :: thesis:

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

end;

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

hence (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . GBP = (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . GBP by SCMPDS_6:87
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . GBP by A6, SCMPDS_5:47, U
.= 0 by A42, A43, AMI_3:52, SCMPDS_2:60 ;
:: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 1) = (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 1) by A61, SCMPDS_6:87
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos 1) by A6, SCMPDS_5:47, U
.= s . (intpos 1) by A56, A43, AMI_3:52, SCMPDS_2:60 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 2) = (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 2) by A61, SCMPDS_6:87
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos 2) by A6, SCMPDS_5:47, U
.= s . (intpos 2) by A41, A43, AMI_3:52, SCMPDS_2:60 ; :: thesis:
thus (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 4) = (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 4) by A61, SCMPDS_6:87
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos 4) by A6, SCMPDS_5:47, U
.= s . (intpos 4) by A40, A43, AMI_3:52, SCMPDS_2:60 ; :: thesis:

hereby :: thesis:

let i be Element of NAT ; :: thesis:
assume A62: i >= 8 ; :: thesis:
then A63: i > 5 by XXREAL_0:2;
i > 3 by A62, XXREAL_0:2;
then A64: intpos i <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos i) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos i) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos i) by A61, SCMPDS_6:87
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos i) by A6, SCMPDS_5:47, U
.= (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos i) by A43, A63, AMI_3:52, SCMPDS_2:60
.= (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos i) by A64, SCMPDS_2:60
.= (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos i) by SCMPDS_5:40
.= s . (intpos i) by A51, A62 ; :: thesis:

end;

hence ( (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . GBP = 0 & (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 1) = s . (intpos 1) & (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 4) = s . (intpos 4) ) by SCMPDS_5:39; :: thesis:
thus for i being Element of NAT st i >= 8 holds
(IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos i) = s . (intpos i) by A57; :: thesis:
A65: (IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)) . (intpos 7) = (Exec ((AddTo (GBP,7,(- 1))),(Exec (((GBP,5) := (GBP,7)),(Initialize s))))) . (intpos 7) by SCMPDS_5:47
.= ((Exec (((GBP,5) := (GBP,7)),(Initialize s))) . (intpos 7)) + (- 1) by A10, SCMPDS_2:60
.= (s . (intpos 7)) - 1 by A19 ;
A66: (IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)) . (intpos 7) = (Exec (((GBP,6) := ((intpos 2),0)),(IExec ((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))),P,s)))) . (intpos 7) by SCMPDS_5:46
.= (s . (intpos 7)) - 1 by A65, A15, AMI_3:52, SCMPDS_2:59 ;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 7) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 7) by SCMPDS_5:46
.= (s . (intpos 7)) - 1 by A66, A22, AMI_3:52, SCMPDS_2:62 ;
then A67: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos 7) = (s . (intpos 7)) - 1 by SCMPDS_5:40;
(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)) . (intpos 3) = (Exec ((SubFrom (GBP,6,(intpos 3),0)),(IExec (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))),P,s)))) . (intpos 3) by SCMPDS_5:46
.= me by A20, A22, AMI_3:52, SCMPDS_2:62 ;
then A68: (Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . (intpos 3) = s . (intpos 3) by A2, SCMPDS_5:40;
A69: DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) = intpos (0 + 3) by A32, SCMP_GCD:5;

hereby :: thesis:

A70: intpos 7 <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
assume A71: s . (intpos md) > s . (intpos me) ; :: thesis:
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 7) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 7) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 7) by A55, A71, SCMPDS_6:87, XREAL_1:52
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos 7) by A6, SCMPDS_5:47, U
.= (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 7) by A43, AMI_3:52, SCMPDS_2:60
.= (s . (intpos 7)) - 1 by A67, A70, SCMPDS_2:60 ; :: thesis:
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 3) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 3) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 3) by A55, A71, SCMPDS_6:87, XREAL_1:52
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos 3) by A6, SCMPDS_5:47, U
.= (Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 3) by A43, AMI_3:52, SCMPDS_2:60
.= (s . (intpos 3)) + 1 by A69, A68, SCMPDS_2:60 ; :: thesis:
A72: intpos 5 <> DataLoc (((Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))) . GBP),3) by A32, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 5) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 5) by SCMPDS_5:39
.= (IExec (((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 5) by A55, A71, SCMPDS_6:87, XREAL_1:52
.= (Exec ((AddTo (GBP,5,(- 1))),(Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))))) . (intpos 5) by A6, SCMPDS_5:47, U
.= ((Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 5)) + (- 1) by A43, SCMPDS_2:60
.= ((Exec ((AddTo (GBP,3,1)),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 5)) - 1
.= (s . (intpos 7)) - 1 by A37, A72, SCMPDS_2:60 ; :: thesis:

end;

hereby :: thesis:

assume A73: s . (intpos md) <= s . (intpos me) ; :: thesis:
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 7) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 7) by SCMPDS_5:39
.= (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 7) by A55, A73, SCMPDS_6:88, XREAL_1:49
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 7) by SCMPDS_5:45
.= 0 by A33, SCMPDS_2:58 ; :: thesis:
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 3) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 3) by SCMPDS_5:39
.= (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 3) by A55, A73, SCMPDS_6:88, XREAL_1:49
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 3) by SCMPDS_5:45
.= s . (intpos 3) by A33, A68, AMI_3:52, SCMPDS_2:58 ; :: thesis:
thus (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 5) = (IExec ((if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 5) by SCMPDS_5:39
.= (IExec ((Load ((GBP,7) := 0)),P,(IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s)))) . (intpos 5) by A55, A73, SCMPDS_6:88, XREAL_1:49
.= (Exec (((GBP,7) := 0),(Initialize (IExec ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))),P,s))))) . (intpos 5) by SCMPDS_5:45
.= s . (intpos 7) by A37, A33, AMI_3:52, SCMPDS_2:58 ; :: thesis:

end;