let P be Instruction-Sequence of SCMPDS; 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:6;
set t0 = s;
set t1 = Exec (((GBP,5) := ((intpos 4),(- 1))),s);
set t2 = IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s);
set Q2 = P;
A5:
DataLoc ((s . GBP),5) = intpos (0 + 5)
by A2, SCMP_GCD:1;
then A6:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP = 0
by A2, AMI_3:10, SCMPDS_2:47;
then A7:
DataLoc (((Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:1;
A8:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 4) = s . (intpos 4)
by A5, AMI_3:10, SCMPDS_2:47;
A9:
s . (intpos 4) >= 1 + (6 + (s . (intpos 6)))
by A1;
then A10:
(s . (intpos 4)) - 1 >= 6 + (s . (intpos 6))
by XREAL_1:19;
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,(Initialize (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,(Initialize (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,(Initialize (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))));
(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))),s)))) . GBP
by SCMPDS_5:42
.=
0
by A6, A7, AMI_3:10, SCMPDS_2:50
;
then A11:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP = 0
by SCMPDS_5:15;
then A12:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:1;
then A13:
(Exec (((GBP,5) := ((intpos 4),(- 1))),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP = 0
by A11, AMI_3:10, SCMPDS_2:47;
(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))),s)))) . (intpos 4)
by SCMPDS_5:42
.=
s . (intpos 4)
by A8, A7, AMI_3:10, SCMPDS_2:50
;
then
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:15;
then A14:
(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 A12, AMI_3:10, SCMPDS_2:47;
A15:
6 + (s . (intpos 6)) > 6 + 0
by A3, XREAL_1:6;
then
0 <> |.(((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 A10, A14, ABSVALUE:def 1;
then A16:
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 XTUPLE_0:1;
(s . (intpos 4)) - 1 > 0
by A3, A9, XREAL_1:19;
then A17:
|.(((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 A14, ABSVALUE:def 1;
then
4 <> |.(((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 A10, A15, XXREAL_0:2;
then A18:
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 XTUPLE_0:1;
A19: (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))))) . (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 SCMPDS_5:42
.=
s . (intpos 4)
by A14, A18, SCMPDS_2:47
;
then
0 <> |.(((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))))) . (intpos 4)) + 0).|
by A1, A4, ABSVALUE:def 1;
then A20:
GBP <> DataLoc (((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))))) . (intpos 4)),0)
by XTUPLE_0:1;
A21: (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))))) . 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 SCMPDS_5:42
.=
0
by A13, A16, SCMPDS_2:47
;
A22: (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))))) . GBP =
(Exec ((((intpos 4),0) := (GBP,5)),(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))))))) . GBP
by SCMPDS_5:41
.=
0
by A21, A20, SCMPDS_2:47
;
then A23:
GBP <> DataLoc (((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))))) . GBP),4)
by AMI_3:10, SCMP_GCD:1;
A24:
(Exec (((GBP,5) := ((intpos 4),(- 1))),s)) . (intpos 1) = s . (intpos 1)
by A5, AMI_3:10, SCMPDS_2:47;
(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))),s)))) . (intpos 1)
by SCMPDS_5:42
.=
s . (intpos 1)
by A24, A7, AMI_3:10, SCMPDS_2:50
;
then A25:
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:15;
then A26:
(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 A12, AMI_3:10, SCMPDS_2:47;
A27: (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))))) . GBP =
(Exec ((AddTo (GBP,4,(- 1))),(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))))))) . GBP
by SCMPDS_5:41
.=
0
by A22, A23, SCMPDS_2:48
;
then A28:
DataLoc (((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))))) . GBP),6) = intpos (0 + 6)
by SCMP_GCD:1;
A29:
DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),6) = intpos (0 + 6)
by A11, SCMP_GCD:1;
now (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP = 0 per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (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,(Initialize (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP
by SCMPDS_5:40
.=
0
by A11, A29, AMI_3:10, SCMPDS_2:46
;
verum end; suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (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,(Initialize (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,(Initialize (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . GBP
by SCMPDS_6:73
.=
(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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . GBP
by SCMPDS_5:41
.=
0
by A27, A28, AMI_3:10, SCMPDS_2:48
;
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:35; (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)
A30:
intpos 1 <> DataLoc (((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))))) . GBP),4)
by A22, AMI_3:10, SCMP_GCD:1;
|.(((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))))) . (intpos 4)) + 0).| = s . (intpos 4)
by A1, A4, A19, ABSVALUE:def 1;
then
1 <> |.(((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))))) . (intpos 4)) + 0).|
by A1, A4, XXREAL_0:2;
then A31:
intpos 1 <> DataLoc (((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))))) . (intpos 4)),0)
by XTUPLE_0:1;
1 <> |.(((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 A10, A15, A17, XXREAL_0:2;
then A32:
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 XTUPLE_0:1;
A33: (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))))) . (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 SCMPDS_5:42
.=
s . (intpos 1)
by A26, A32, SCMPDS_2:47
;
A34: (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))))) . (intpos 1) =
(Exec ((((intpos 4),0) := (GBP,5)),(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))))))) . (intpos 1)
by SCMPDS_5:41
.=
s . (intpos 1)
by A33, A31, SCMPDS_2:47
;
A35: (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))))) . (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 1)
by SCMPDS_5:41
.=
s . (intpos 1)
by A34, A30, SCMPDS_2:48
;
now (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1) = s . (intpos 1)per cases
( (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) <= 0 or (Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . GBP),5)) > 0 )
;
suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (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,(Initialize (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1) =
(IExec ((Load ((GBP,6) := 0)),P,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1)
by SCMPDS_6:74
.=
(Exec (((GBP,6) := 0),(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1)
by SCMPDS_5:40
.=
s . (intpos 1)
by A25, A29, AMI_3:10, SCMPDS_2:46
;
verum end; suppose
(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))) . (DataLoc (((Initialize (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,(Initialize (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,(Initialize (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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))) . (intpos 1)
by SCMPDS_6:73
.=
(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,(Initialize (IExec ((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))),P,s))))))) . (intpos 1)
by SCMPDS_5:41
.=
s . (intpos 1)
by A35, A28, AMI_3:10, SCMPDS_2:48
;
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:35; verum