A22: now :: thesis:

per cases ;

suppose A23: intpos m4 <> DataLoc (((IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos 3)),0) ; :: thesis:

thus (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos m4) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos m4) by SCMPDS_5:41
.= s . (intpos m3) by A21, A23, SCMPDS_2:47 ; :: thesis:

end;

suppose A24: intpos m4 = DataLoc (((IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos 3)),0) ; :: thesis:

end;

(Initialize s) . (intpos 2) = s . (intpos 2) by SCMPDS_5:15;
then A25: (Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))) . (intpos 2) = s . (intpos 2) by A9, AMI_3:10, SCMPDS_2:47;
A26: m4 > 2 by A6, XXREAL_0:2;
A27: m3 > 5 by A5, XXREAL_0:2;
A28: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . GBP = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . GBP by SCMPDS_5:41
.= 0 by A5, A14, A19, AMI_3:10, SCMPDS_2:47 ;
then A29: DataLoc (((IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . GBP),5) = intpos (0 + 5) by SCMP_GCD:1;
A30: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . GBP by SCMPDS_5:41
.= 0 by A28, A29, AMI_3:10, SCMPDS_2:48 ;
then A31: GBP <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by AMI_3:10, SCMP_GCD:1;
A32: m3 > 3 by A5, XXREAL_0:2;
then A33: intpos m3 <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A30, AMI_3:10, SCMP_GCD:1;
A34: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos 3) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos 3) by SCMPDS_5:41
.= m3 by A32, A18, A19, AMI_3:10, SCMPDS_2:47 ;
A35: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos 3) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos 3) by SCMPDS_5:41
.= m3 by A34, A29, AMI_3:10, SCMPDS_2:48 ;
A36: DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) = intpos (0 + 3) by A30, SCMP_GCD:1;
A37: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos 3) by SCMPDS_5:41
.= m3 + 1 by A35, A36, SCMPDS_2:48 ;
A38: m3 > 2 by A5, XXREAL_0:2;
A39: m4 > 5 by A6, XXREAL_0:2;
A40: (IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos 2) = (Exec ((((intpos 4),0) := ((intpos 3),0)),(Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))))) . (intpos 2) by SCMPDS_5:42
.= s . (intpos 2) by A25, A13, A26, AMI_3:10, SCMPDS_2:47 ;
A41: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos m3) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos m3) by SCMPDS_5:41
.= s . (intpos m4) by A19, A16, SCMPDS_2:47 ;
A42: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos m3) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos m3) by SCMPDS_5:41
.= s . (intpos m4) by A27, A41, A29, AMI_3:10, SCMPDS_2:48 ;
A43: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos m3) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos m3) by SCMPDS_5:41
.= s . (intpos m4) by A42, A33, SCMPDS_2:48 ;
A44: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos m4) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos m4) by SCMPDS_5:41
.= s . (intpos m3) by A39, A22, A29, AMI_3:10, SCMPDS_2:48 ;
A45: intpos m4 <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A7, A30, AMI_3:10, SCMP_GCD:1;
A46: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos m4) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos m4) by SCMPDS_5:41
.= s . (intpos m3) by A44, A45, SCMPDS_2:48 ;
A47: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos 2) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos 2) by SCMPDS_5:41
.= s . (intpos 2) by A40, A19, A38, AMI_3:10, SCMPDS_2:47 ;
A48: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos 2) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos 2) by SCMPDS_5:41
.= s . (intpos 2) by A47, A29, AMI_3:10, SCMPDS_2:48 ;
A49: intpos 2 <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A30, AMI_3:10, SCMP_GCD:1;
A50: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos 2) by SCMPDS_5:41
.= s . (intpos 2) by A48, A49, SCMPDS_2:48 ;
A51: m4 > 1 by A6, XXREAL_0:2;
A52: DataLoc ((s . GBP),5) = intpos (0 + 5) by A1, SCMP_GCD:1;
(Initialize s) . (intpos 5) = s . (intpos 5) by SCMPDS_5:15;
then A53: (Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))) . (intpos 5) = s . (intpos 5) by A9, AMI_3:10, SCMPDS_2:47;
A54: (IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos 5) = (Exec ((((intpos 4),0) := ((intpos 3),0)),(Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))))) . (intpos 5) by SCMPDS_5:42
.= s . (intpos 5) by A39, A53, A13, AMI_3:10, SCMPDS_2:47 ;
A55: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos 5) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos 5) by SCMPDS_5:41
.= s . (intpos 5) by A27, A54, A19, AMI_3:10, SCMPDS_2:47 ;
A56: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos 5) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos 5) by SCMPDS_5:41
.= ((IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos 5)) + (- 2) by A29, SCMPDS_2:48
.= (s . (intpos 5)) - 2 by A55 ;
A57: intpos 5 <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A30, AMI_3:10, SCMP_GCD:1;
A58: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos 5) by SCMPDS_5:41
.= (s . (intpos 5)) - 2 by A56, A57, SCMPDS_2:48 ;
(Initialize s) . (intpos 1) = s . (intpos 1) by SCMPDS_5:15;
then A59: (Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))) . (intpos 1) = s . (intpos 1) by A9, AMI_3:10, SCMPDS_2:47;
A60: m3 > 1 by A5, XXREAL_0:2;
A61: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . GBP by SCMPDS_5:41
.= 0 by A30, A31, SCMPDS_2:48 ;
then A62: GBP <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by AMI_3:10, SCMP_GCD:1;
A63: m4 > 4 by A6, XXREAL_0:2;
then A64: intpos m4 <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
A65: m3 > 4 by A5, XXREAL_0:2;
then A66: intpos m3 <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
A67: intpos 4 <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A30, AMI_3:10, SCMP_GCD:1;
A68: (IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos 4) = (Exec ((((intpos 4),0) := ((intpos 3),0)),(Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))))) . (intpos 4) by SCMPDS_5:42
.= m4 by A63, A12, A13, AMI_3:10, SCMPDS_2:47 ;
A69: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos 4) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos 4) by SCMPDS_5:41
.= m4 by A65, A68, A19, AMI_3:10, SCMPDS_2:47 ;
A70: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos 4) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos 4) by SCMPDS_5:41
.= m4 by A69, A29, AMI_3:10, SCMPDS_2:48 ;
A71: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos 4) by SCMPDS_5:41
.= m4 by A70, A67, SCMPDS_2:48 ;
A72: intpos 3 <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
A73: (IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos 1) = (Exec ((((intpos 4),0) := ((intpos 3),0)),(Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))))) . (intpos 1) by SCMPDS_5:42
.= s . (intpos 1) by A59, A13, A51, AMI_3:10, SCMPDS_2:47 ;
A74: (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos 1) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos 1) by SCMPDS_5:41
.= s . (intpos 1) by A73, A19, A60, AMI_3:10, SCMPDS_2:47 ;
A75: (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos 1) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos 1) by SCMPDS_5:41
.= s . (intpos 1) by A74, A29, AMI_3:10, SCMPDS_2:48 ;
A76: intpos 1 <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A30, AMI_3:10, SCMP_GCD:1;
A77: (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos 1) by SCMPDS_5:41
.= s . (intpos 1) by A75, A76, SCMPDS_2:48 ;
A78: intpos 1 <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . GBP = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . GBP by SCMPDS_5:41
.= 0 by A61, A62, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . GBP = 0 by A2, A52, SCMPDS_6:83; :: thesis:
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos 1) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos 1) by SCMPDS_5:41
.= s . (intpos 1) by A77, A78, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) by A2, A52, SCMPDS_6:83; :: thesis:
A79: intpos 2 <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos 2) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos 2) by SCMPDS_5:41
.= s . (intpos 2) by A50, A79, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) by A2, A52, SCMPDS_6:83; :: thesis:
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos m3) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos m3) by SCMPDS_5:41
.= s . (intpos m4) by A43, A66, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos m3) = s . (intpos m4) by A2, A52, SCMPDS_6:83; :: thesis:
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos m4) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos m4) by SCMPDS_5:41
.= s . (intpos m3) by A46, A64, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos m4) = s . (intpos m3) by A2, A52, SCMPDS_6:83; :: thesis:
A80: DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) = intpos (0 + 4) by A61, SCMP_GCD:1;
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos 3) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos 3) by SCMPDS_5:41
.= m3 + 1 by A37, A72, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 3) = (s . (intpos 3)) + 1 by A2, A3, A52, SCMPDS_6:83; :: thesis:
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos 4) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos 4) by SCMPDS_5:41
.= ((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4)) + (- 1) by A80, SCMPDS_2:48
.= (s . (intpos 4)) - 1 by A4, A71 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 4) = (s . (intpos 4)) - 1 by A2, A52, SCMPDS_6:83; :: thesis:
A81: intpos 5 <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
(IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos 5) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos 5) by SCMPDS_5:41
.= (s . (intpos 5)) - 2 by A58, A81, SCMPDS_2:48 ;
hence (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 5) = (s . (intpos 5)) - 2 by A2, A52, SCMPDS_6:83; :: thesis:

A82: now :: thesis:

let i be Nat; :: thesis:
assume that
A83: i >= 8 and
i <> m3 and
i <> m4 ; :: thesis:
i > 6 by A83, XXREAL_0:2;
hence (Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))) . (intpos i) = (Initialize s) . (intpos i) by A9, AMI_3:10, SCMPDS_2:47
.= s . (intpos i) by SCMPDS_5:15 ;
:: thesis:

end;

A84: now :: thesis:

let i be Nat; :: thesis:
assume that
A85: i >= 8 and
A86: i <> m3 and
A87: i <> m4 ; :: thesis:
thus (IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos i) = (Exec ((((intpos 4),0) := ((intpos 3),0)),(Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))))) . (intpos i) by SCMPDS_5:42
.= (Exec (((GBP,6) := ((intpos 4),0)),(Initialize s))) . (intpos i) by A13, A87, AMI_3:10, SCMPDS_2:47
.= s . (intpos i) by A82, A85, A86, A87 ; :: thesis:

end;

A88: now :: thesis:

let i be Nat; :: thesis:
assume that
A89: i >= 8 and
A90: i <> m3 and
A91: i <> m4 ; :: thesis:
thus (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos i) = (Exec ((((intpos 3),0) := (GBP,6)),(IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))))) . (intpos i) by SCMPDS_5:41
.= (IExec ((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))),P,(Initialize s))) . (intpos i) by A19, A90, AMI_3:10, SCMPDS_2:47
.= s . (intpos i) by A84, A89, A90, A91 ; :: thesis:

end;

A92: now :: thesis:

let i be Nat; :: thesis:
assume that
A93: i >= 8 and
A94: i <> m3 and
A95: i <> m4 ; :: thesis:
A96: i > 5 by A93, XXREAL_0:2;
thus (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos i) = (Exec ((AddTo (GBP,5,(- 2))),(IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))))) . (intpos i) by SCMPDS_5:41
.= (IExec (((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))),P,(Initialize s))) . (intpos i) by A29, A96, AMI_3:10, SCMPDS_2:48
.= s . (intpos i) by A88, A93, A94, A95 ; :: thesis:

end;

A97: now :: thesis:

let i be Nat; :: thesis:
assume that
A98: i >= 8 and
A99: i <> m3 and
A100: i <> m4 ; :: thesis:
i > 3 by A98, XXREAL_0:2;
then A101: intpos i <> DataLoc (((IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . GBP),3) by A30, AMI_3:10, SCMP_GCD:1;
thus (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = (Exec ((AddTo (GBP,3,1)),(IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))))) . (intpos i) by SCMPDS_5:41
.= (IExec ((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))),P,(Initialize s))) . (intpos i) by A101, SCMPDS_2:48
.= s . (intpos i) by A92, A98, A99, A100 ; :: thesis:

end;

A102: now :: thesis:

let i be Nat; :: thesis:
assume that
A103: i >= 8 and
A104: i <> m3 and
A105: i <> m4 ; :: thesis:
i > 4 by A103, XXREAL_0:2;
then A106: intpos i <> DataLoc (((IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP),4) by A61, AMI_3:10, SCMP_GCD:1;
thus (IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos i) = (Exec ((AddTo (GBP,4,(- 1))),(IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))))) . (intpos i) by SCMPDS_5:41
.= (IExec (((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) by A106, SCMPDS_2:48
.= s . (intpos i) by A97, A103, A104, A105 ; :: thesis:

end;

hereby :: thesis:

let i be Nat; :: thesis:
assume that
A107: i >= 8 and
A108: i <> m3 and
A109: i <> m4 ; :: thesis:
thus (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos i) = (IExec ((((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize s))) . (intpos i) by A2, A52, SCMPDS_6:83
.= s . (intpos i) by A102, A107, A108, A109 ; :: thesis:

end;