let s be 0 -started State of SCMPDS; ( s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 implies ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . GBP = 0 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . (intpos 1) = s . (intpos 1) ) )
set a = GBP ;
set x = DataLoc ((s . (intpos 4)),(- 1));
set y = DataLoc ((s . (intpos 4)),0);
assume that
A1:
s . (intpos 4) >= 7 + (s . (intpos 6))
and
A2:
s . GBP = 0
and
A3:
s . (intpos 6) > 0
; ( (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . GBP = 0 & (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . (intpos 1) = s . (intpos 1) )
A4:
7 + (s . (intpos 6)) > 7 + 0
by A3, XREAL_1:8;
set t0 = Initialize s;
set t1 = Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s));
set t2 = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s);
A5:
(Initialize s) . GBP = 0
by A2, SCMPDS_5:40;
then A6:
DataLoc (((Initialize s) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:5;
then A7:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))) . GBP = 0
by A5, AMI_3:52, SCMPDS_2:59;
then A8:
DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:5;
(Initialize s) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:40;
then A9:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))) . (intpos 4) = s . (intpos 4)
by A6, AMI_3:52, SCMPDS_2:59;
A10:
s . (intpos 4) >= 1 + (6 + (s . (intpos 6)))
by A1;
then A11:
(s . (intpos 4)) - 1 >= 6 + (s . (intpos 6))
by XREAL_1:21;
set Fi = (GBP,6) := 0;
set t02 = Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s));
set t3 = IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)));
set t4 = IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)));
set t5 = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)));
set t6 = Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))));
X1:
IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) = IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))
by SCMPDS_5:48;
X2:
IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) = IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))
by SCMPDS_5:48;
X3:
IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))
by SCMPDS_5:48;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))))) . GBP
by SCMPDS_5:47
.=
0
by A7, A8, AMI_3:52, SCMPDS_2:62
;
then A12:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) . GBP = 0
by SCMPDS_5:40;
then A13:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:5;
then A14:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . GBP = 0
by A12, AMI_3:52, SCMPDS_2:59;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (intpos 4) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))))) . (intpos 4)
by SCMPDS_5:47
.=
s . (intpos 4)
by A9, A8, AMI_3:52, SCMPDS_2:62
;
then
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:40;
then A15:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4) = s . (intpos 4)
by A13, AMI_3:52, SCMPDS_2:59;
A16:
6 + (s . (intpos 6)) > 6 + 0
by A3, XREAL_1:8;
then
0 <> abs (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)) + (- 1))
by A11, A15, ABSVALUE:def 1;
then A17:
GBP <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)),(- 1))
by ZFMISC_1:33;
(s . (intpos 4)) - 1 > 0
by A3, A10, XREAL_1:21;
then A18:
abs (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)) + (- 1)) = (s . (intpos 4)) - 1
by A15, ABSVALUE:def 1;
then
4 <> abs (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)) + (- 1))
by A11, A16, XXREAL_0:2;
then A19:
intpos 4 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)),(- 1))
by ZFMISC_1:33;
X4:
Initialize (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) = Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))
;
A20: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 4) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))))) . (intpos 4)
by X3, X4, SCMPDS_5:47
.=
s . (intpos 4)
by A15, A19, SCMPDS_2:59
;
then
0 <> abs (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 4)) + 0)
by A1, A4, ABSVALUE:def 1;
then A21:
GBP <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 4)),0)
by ZFMISC_1:33;
A22: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))))) . GBP
by X3, X4, SCMPDS_5:47
.=
0
by A14, A17, SCMPDS_2:59
;
A23: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))))) . GBP
by X2, X3, SCMPDS_5:46
.=
0
by A22, A21, SCMPDS_2:59
;
then A24:
GBP <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP),4)
by AMI_3:52, SCMP_GCD:5;
(Initialize s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A25:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))) . (intpos 1) = s . (intpos 1)
by A6, AMI_3:52, SCMPDS_2:59;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (intpos 1) =
(Exec ((SubFrom (GBP,5,(intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize s))))) . (intpos 1)
by SCMPDS_5:47
.=
s . (intpos 1)
by A25, A8, AMI_3:52, SCMPDS_2:62
;
then A26:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A27:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 1) = s . (intpos 1)
by A13, AMI_3:52, SCMPDS_2:59;
A28: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))))) . GBP
by X1, X2, SCMPDS_5:46
.=
0
by A23, A24, SCMPDS_2:60
;
then A29:
DataLoc (((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP),6) = intpos (0 + 6)
by SCMP_GCD:5;
A30:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) . GBP),6) = intpos (0 + 6)
by A12, SCMP_GCD:5;
X5:
IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))) = IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))
by SCMPDS_5:48;
now per cases
( (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) <= 0 or (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) > 0 )
;
suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) <= 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP = 0 hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP =
(IExec ((Load ((GBP,6) := 0)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP
by SCMPDS_6:88
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . GBP
by SCMPDS_5:45
.=
0
by A12, A30, AMI_3:52, SCMPDS_2:58
;
verum end; suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) > 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP = 0 hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP
by SCMPDS_6:87
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))))) . GBP
by X1, X5, SCMPDS_5:46
.=
0
by A28, A29, AMI_3:52, SCMPDS_2:60
;
verum end;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . GBP = 0
by SCMPDS_5:39; (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . (intpos 1) = s . (intpos 1)
A31:
intpos 1 <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . GBP),4)
by A23, AMI_3:52, SCMP_GCD:5;
abs (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 4)) + 0) = s . (intpos 4)
by A1, A4, A20, ABSVALUE:def 1;
then
1 <> abs (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 4)) + 0)
by A1, A4, XXREAL_0:2;
then A32:
intpos 1 <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 4)),0)
by ZFMISC_1:33;
1 <> abs (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)) + (- 1))
by A11, A16, A18, XXREAL_0:2;
then A33:
intpos 1 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 4)),(- 1))
by ZFMISC_1:33;
A34: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) =
(Exec ((((intpos 4),(- 1)) := ((intpos 4),0)),(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))))) . (intpos 1)
by X3, X4, SCMPDS_5:47
.=
s . (intpos 1)
by A27, A33, SCMPDS_2:59
;
A35: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))))) . (intpos 1)
by X2, X3, SCMPDS_5:46
.=
s . (intpos 1)
by A34, A32, SCMPDS_2:59
;
A36: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))))) . (intpos 1)
by X1, X2, SCMPDS_5:46
.=
s . (intpos 1)
by A35, A31, SCMPDS_2:60
;
now per cases
( (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) <= 0 or (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) > 0 )
;
suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) <= 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) = s . (intpos 1)hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) =
(IExec ((Load ((GBP,6) := 0)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1)
by SCMPDS_6:88
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s))))) . (intpos 1)
by SCMPDS_5:45
.=
s . (intpos 1)
by A26, A30, AMI_3:52, SCMPDS_2:58
;
verum end; suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)) . GBP),5)) > 0
;
(IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) = s . (intpos 1)hence (IExec ((if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1) =
(IExec (((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))) . (intpos 1)
by SCMPDS_6:87
.=
(Exec ((AddTo (GBP,6,(- 1))),(IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),s)))))) . (intpos 1)
by X1, X5, SCMPDS_5:46
.=
s . (intpos 1)
by A36, A29, AMI_3:52, SCMPDS_2:60
;
verum end;
hence
(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))),s)) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:39; verum