let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (intpos 6) > 0 holds
( (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))))),P,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))))),P,s)) . (intpos 1) = s . (intpos 1) )
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))))),P,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))))),P,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))))),P,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))))),P,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))),P,s);
set Q2 = P;
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))),P,s));
set Q02 = P;
set t3 = IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)));
set t4 = IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)));
set t5 = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)));
set t6 = Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))));
A12:
IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) = IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))
by SCMPDS_5:48;
A13:
IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) = IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))
by SCMPDS_5:48;
A14:
IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))
by SCMPDS_5:48;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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 A15:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP = 0
by SCMPDS_5:40;
then A16:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:5;
then A17:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP = 0
by A15, AMI_3:52, SCMPDS_2:59;
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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))),P,s))) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:40;
then A18:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4) = s . (intpos 4)
by A16, AMI_3:52, SCMPDS_2:59;
A19:
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))),P,s))))) . (intpos 4)) + (- 1))
by A11, A18, ABSVALUE:def 1;
then A20:
GBP <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by ZFMISC_1:33;
(s . (intpos 4)) - 1 > 0
by A3, A10, XREAL_1:21;
then A21:
abs (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)) + (- 1)) = (s . (intpos 4)) - 1
by A18, 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))),P,s))))) . (intpos 4)) + (- 1))
by A11, A19, XXREAL_0:2;
then A22:
intpos 4 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by ZFMISC_1:33;
A23:
Initialize (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) = Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))
;
A24: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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))),P,s))))))) . (intpos 4)
by A14, A23, SCMPDS_5:47
.=
s . (intpos 4)
by A18, A22, SCMPDS_2:59
;
then
0 <> abs (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 4)) + 0)
by A1, A4, ABSVALUE:def 1;
then A25:
GBP <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 4)),0)
by ZFMISC_1:33;
A26: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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))),P,s))))))) . GBP
by A14, A23, SCMPDS_5:47
.=
0
by A17, A20, SCMPDS_2:59
;
A27: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))))) . GBP
by A13, A14, SCMPDS_5:46
.=
0
by A26, A25, SCMPDS_2:59
;
then A28:
GBP <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP),4)
by AMI_3:52, SCMP_GCD:5;
(Initialize s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A29:
(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))),P,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 A29, A8, AMI_3:52, SCMPDS_2:62
;
then A30:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A31:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1) = s . (intpos 1)
by A16, AMI_3:52, SCMPDS_2:59;
A32: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP =
(Exec ((AddTo (GBP,4,(- 1))),(IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))))) . GBP
by A12, A13, SCMPDS_5:46
.=
0
by A27, A28, SCMPDS_2:60
;
then A33:
DataLoc (((IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP),6) = intpos (0 + 6)
by SCMP_GCD:5;
A34:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),6) = intpos (0 + 6)
by A15, SCMP_GCD:5;
A35:
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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))
by SCMPDS_5:48;
now per cases
( (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . GBP),5)) <= 0 or (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . GBP),5)) > 0 )
;
suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP =
(IExec ((Load ((GBP,6) := 0)),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP
by SCMPDS_6:88
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP
by SCMPDS_5:45
.=
0
by A15, A34, AMI_3:52, SCMPDS_2:58
;
verum end; suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))))) . GBP
by A12, A35, SCMPDS_5:46
.=
0
by A32, A33, 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))))),P,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))))),P,s)) . (intpos 1) = s . (intpos 1)
A36:
intpos 1 <> DataLoc (((IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . GBP),4)
by A27, AMI_3:52, SCMP_GCD:5;
abs (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 4)) + 0) = s . (intpos 4)
by A1, A4, A24, ABSVALUE:def 1;
then
1 <> abs (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 4)) + 0)
by A1, A4, XXREAL_0:2;
then A37:
intpos 1 <> DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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))),P,s))))) . (intpos 4)) + (- 1))
by A11, A19, A21, XXREAL_0:2;
then A38:
intpos 1 <> DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 4)),(- 1))
by ZFMISC_1:33;
A39: (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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))),P,s))))))) . (intpos 1)
by A14, A23, SCMPDS_5:47
.=
s . (intpos 1)
by A31, A38, SCMPDS_2:59
;
A40: (IExec (((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 1) =
(Exec ((((intpos 4),0) := (GBP,5)),(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))))) . (intpos 1)
by A13, A14, SCMPDS_5:46
.=
s . (intpos 1)
by A39, A37, SCMPDS_2:59
;
A41: (IExec ((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))))) . (intpos 1)
by A12, A13, SCMPDS_5:46
.=
s . (intpos 1)
by A40, A36, SCMPDS_2:60
;
now per cases
( (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . GBP),5)) <= 0 or (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . GBP),5)) > 0 )
;
suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 1) =
(IExec ((Load ((GBP,6) := 0)),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))) . (intpos 1)
by SCMPDS_6:88
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1)
by SCMPDS_5:45
.=
s . (intpos 1)
by A30, A34, AMI_3:52, SCMPDS_2:58
;
verum end; suppose
(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)) . (DataLoc (((IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,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)))),P,(IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s)))))) . (intpos 1)
by A12, A35, SCMPDS_5:46
.=
s . (intpos 1)
by A41, A33, 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))))),P,s)) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:39; verum