let s be 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 = Initialized s;
set t1 = Exec (GBP ,5 := (intpos 4),(- 1)),(Initialized s);
set t2 = IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s;
A5:
(Initialized s) . GBP = 0
by A2, SCMPDS_5:40;
then A6:
DataLoc ((Initialized s) . GBP ),5 = intpos (0 + 5)
by SCMP_GCD:5;
then A7:
(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialized s)) . GBP = 0
by A5, AMI_3:52, SCMPDS_2:59;
then A8:
DataLoc ((Exec (GBP ,5 := (intpos 4),(- 1)),(Initialized s)) . GBP ),5 = intpos (0 + 5)
by SCMP_GCD:5;
(Initialized s) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:40;
then A9:
(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialized 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 = Initialized (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)),(Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s));
(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)),(Initialized s))) . GBP
by SCMPDS_5:47
.=
0
by A7, A8, AMI_3:52, SCMPDS_2:62
;
then A12:
(Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP = 0
by SCMPDS_5:40;
then A13:
DataLoc ((Initialized (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)),(Initialized (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)),(Initialized s))) . (intpos 4)
by SCMPDS_5:47
.=
s . (intpos 4)
by A9, A8, AMI_3:52, SCMPDS_2:62
;
then
(Initialized (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)),(Initialized (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)),(Initialized (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)),(Initialized (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)),(Initialized (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)),(Initialized (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)),(Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s))) . (intpos 4)),(- 1)
by ZFMISC_1:33;
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)),(Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)))) . (intpos 4)
by 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)),(Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)))) . GBP
by 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 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;
(Initialized s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A25:
(Exec (GBP ,5 := (intpos 4),(- 1)),(Initialized 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)),(Initialized s))) . (intpos 1)
by SCMPDS_5:47
.=
s . (intpos 1)
by A25, A8, AMI_3:52, SCMPDS_2:62
;
then A26:
(Initialized (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)),(Initialized (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 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 ((Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)) . GBP ),6 = intpos (0 + 6)
by A12, SCMP_GCD:5;
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 ),(Initialized (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 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)),(Initialized (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)),(Initialized (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)),(Initialized (IExec ((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )),s)))) . (intpos 1)
by 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 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 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 ),(Initialized (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 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