set a = GBP ;
let s be State of SCMPDS ; for md, me being Element of NAT st s . (intpos 2) = md & s . (intpos 4) = me & md >= 8 & me >= 8 & s . GBP = 0 holds
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . GBP = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 1) = s . (intpos 1) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 ) ) & ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) ) )
let md, me be Element of NAT ; ( s . (intpos 2) = md & s . (intpos 4) = me & md >= 8 & me >= 8 & s . GBP = 0 implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . GBP = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 1) = s . (intpos 1) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 ) ) & ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) ) ) )
assume that
A1:
s . (intpos 2) = md
and
A2:
s . (intpos 4) = me
and
A3:
md >= 8
and
A4:
me >= 8
and
A5:
s . GBP = 0
; ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . GBP = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 1) = s . (intpos 1) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 ) ) & ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) ) )
set t0 = Initialized s;
set t1 = IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s;
set t2 = IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s;
set t3 = IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s;
set t4 = Exec (GBP ,7 := GBP ,5),(Initialized s);
A6:
(Initialized s) . GBP = 0
by A5, SCMPDS_5:40;
then A7:
DataLoc ((Initialized s) . GBP ),7 = intpos (0 + 7)
by SCMP_GCD:5;
then A8:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . GBP = 0
by A6, AMI_3:52, SCMPDS_2:59;
then A9:
DataLoc ((Exec (GBP ,7 := GBP ,5),(Initialized s)) . GBP ),5 = intpos (0 + 5)
by SCMP_GCD:5;
(Initialized s) . (intpos 4) = me
by A2, SCMPDS_5:40;
then A10:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 4) = me
by A7, AMI_3:52, SCMPDS_2:59;
A11: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 4) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos 4)
by SCMPDS_5:47
.=
me
by A10, A9, AMI_3:52, SCMPDS_2:60
;
then A12:
DataLoc ((IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 4)),0 = intpos (me + 0 )
by SCMP_GCD:5;
A13: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . GBP =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . GBP
by SCMPDS_5:47
.=
0
by A8, A9, AMI_3:52, SCMPDS_2:60
;
then A14:
DataLoc ((IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . GBP ),6 = intpos (0 + 6)
by SCMP_GCD:5;
(Initialized s) . (intpos 2) = md
by A1, SCMPDS_5:40;
then A15:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 2) = md
by A7, AMI_3:52, SCMPDS_2:59;
A16: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 2) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos 2)
by SCMPDS_5:47
.=
md
by A15, A9, AMI_3:52, SCMPDS_2:60
;
A17:
(Initialized s) . (intpos 5) = s . (intpos 5)
by SCMPDS_5:40;
then A18:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 5) = s . (intpos 5)
by A7, AMI_3:52, SCMPDS_2:59;
set t01 = Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s);
set ii7 = GBP ,5 := 0 ;
set t5 = Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s));
A19: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 2) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 2)
by SCMPDS_5:46
.=
md
by A16, A14, AMI_3:52, SCMPDS_2:59
;
A20: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . GBP =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . GBP
by SCMPDS_5:46
.=
0
by A13, A14, AMI_3:52, SCMPDS_2:59
;
then A21:
DataLoc ((IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . GBP ),6 = intpos (0 + 6)
by SCMP_GCD:5;
DataLoc ((Initialized s) . GBP ),5 = intpos (0 + 5)
by A6, SCMP_GCD:5;
then A22:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 7) = s . (intpos 5)
by A17, A7, SCMPDS_2:59;
A23: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 7) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos 7)
by SCMPDS_5:47
.=
s . (intpos 5)
by A22, A9, AMI_3:52, SCMPDS_2:60
;
A24: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 7) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 7)
by SCMPDS_5:46
.=
s . (intpos 5)
by A23, A14, AMI_3:52, SCMPDS_2:59
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 7) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 7)
by SCMPDS_5:46
.=
s . (intpos 5)
by A24, A21, AMI_3:52, SCMPDS_2:62
;
then A25:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 7) = s . (intpos 5)
by SCMPDS_5:40;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 2) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 2)
by SCMPDS_5:46
.=
md
by A19, A21, AMI_3:52, SCMPDS_2:62
;
then A26:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2)
by A1, SCMPDS_5:40;
A27:
now let i be
Element of
NAT ;
( i >= 8 implies (Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos i) = s . (intpos i) )assume
i >= 8
;
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos i) = s . (intpos i)then
i > 7
by XXREAL_0:2;
hence (Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos i) =
(Initialized s) . (intpos i)
by A7, AMI_3:52, SCMPDS_2:59
.=
s . (intpos i)
by SCMPDS_5:40
;
verum end;
A28:
now let i be
Element of
NAT ;
( i >= 8 implies (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos i) = s . (intpos i) )assume A29:
i >= 8
;
(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos i) = s . (intpos i)then A30:
i > 5
by XXREAL_0:2;
thus (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos i) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos i)
by SCMPDS_5:47
.=
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos i)
by A9, A30, AMI_3:52, SCMPDS_2:60
.=
s . (intpos i)
by A27, A29
;
verum end;
A31:
now let i be
Element of
NAT ;
( i >= 8 implies (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos i) = s . (intpos i) )assume A32:
i >= 8
;
(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos i) = s . (intpos i)then A33:
i > 6
by XXREAL_0:2;
thus (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos i) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos i)
by SCMPDS_5:46
.=
(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos i)
by A14, A33, AMI_3:52, SCMPDS_2:59
.=
s . (intpos i)
by A28, A32
;
verum end;
A34:
now let i be
Element of
NAT ;
( i >= 8 implies (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos i) = s . (intpos i) )assume A35:
i >= 8
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos i) = s . (intpos i)then A36:
i > 6
by XXREAL_0:2;
thus (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos i) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos i)
by SCMPDS_5:46
.=
(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos i)
by A21, A36, AMI_3:52, SCMPDS_2:62
.=
s . (intpos i)
by A31, A35
;
verum end;
(Initialized s) . (intpos 3) = s . (intpos 3)
by SCMPDS_5:40;
then A37:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 3) = s . (intpos 3)
by A7, AMI_3:52, SCMPDS_2:59;
A38: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 3) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos 3)
by SCMPDS_5:47
.=
s . (intpos 3)
by A37, A9, AMI_3:52, SCMPDS_2:60
;
(Initialized s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
then A39:
(Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 1) = s . (intpos 1)
by A7, AMI_3:52, SCMPDS_2:59;
A40: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 1) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos 1)
by SCMPDS_5:47
.=
s . (intpos 1)
by A39, A9, AMI_3:52, SCMPDS_2:60
;
A41: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 1) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 1)
by SCMPDS_5:46
.=
s . (intpos 1)
by A40, A14, AMI_3:52, SCMPDS_2:59
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 1) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 1)
by SCMPDS_5:46
.=
s . (intpos 1)
by A41, A21, AMI_3:52, SCMPDS_2:62
;
then A42:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:40;
A43: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 3) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 3)
by SCMPDS_5:46
.=
s . (intpos 3)
by A38, A14, AMI_3:52, SCMPDS_2:59
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 3) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 3)
by SCMPDS_5:46
.=
s . (intpos 3)
by A43, A21, AMI_3:52, SCMPDS_2:62
;
then A44:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3)
by SCMPDS_5:40;
A45: (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . GBP =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . GBP
by SCMPDS_5:46
.=
0
by A20, A21, AMI_3:52, SCMPDS_2:62
;
then A46:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP = 0
by SCMPDS_5:40;
then A47:
DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),5 = intpos (0 + 5)
by SCMP_GCD:5;
intpos 3 <> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
then A48:
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 3) = s . (intpos 3)
by A44, SCMPDS_2:60;
intpos 2 <> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
then A49:
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 2) = s . (intpos 2)
by A26, SCMPDS_2:60;
GBP <> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
then A50:
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . GBP = 0
by A46, SCMPDS_2:60;
then A51:
DataLoc ((Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . GBP ),7 = intpos (0 + 7)
by SCMP_GCD:5;
A52: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 6) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 6)
by SCMPDS_5:46
.=
(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos me)
by A14, A12, SCMPDS_2:59
.=
s . (intpos me)
by A4, A28
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 6) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 6)
by SCMPDS_5:46
.=
((IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 6)) - ((IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (DataLoc ((IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 2)),0 ))
by A21, SCMPDS_2:62
.=
((IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 6)) - ((IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos (md + 0 )))
by A19, SCMP_GCD:5
.=
(s . (intpos me)) - (s . (intpos md))
by A3, A52, A31
;
then A53:
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (DataLoc ((IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . GBP ),6) = (s . (intpos me)) - (s . (intpos md))
by A45, SCMP_GCD:5;
intpos 1 <> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
then A54:
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 1) = s . (intpos 1)
by A42, SCMPDS_2:60;
A55:
now per cases
( (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (DataLoc ((IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . GBP ),6) <= 0 or (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (DataLoc ((IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . GBP ),6) > 0 )
;
suppose A56:
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (DataLoc ((IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . GBP ),6) <= 0
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP = 0 & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )hence (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP =
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP
by SCMPDS_6:88
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . GBP
by SCMPDS_5:45
.=
0
by A46, A47, AMI_3:52, SCMPDS_2:58
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )thus (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) =
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1)
by A56, SCMPDS_6:88
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 1)
by SCMPDS_5:45
.=
s . (intpos 1)
by A42, A47, AMI_3:52, SCMPDS_2:58
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )thus (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) =
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2)
by A56, SCMPDS_6:88
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 2)
by SCMPDS_5:45
.=
s . (intpos 2)
by A26, A47, AMI_3:52, SCMPDS_2:58
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )thus (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) =
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3)
by A56, SCMPDS_6:88
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 3)
by SCMPDS_5:45
.=
s . (intpos 3)
by A44, A47, AMI_3:52, SCMPDS_2:58
;
for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i)hereby verum
let i be
Element of
NAT ;
( i >= 8 implies (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) )assume A57:
i >= 8
;
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i)then A58:
i > 5
by XXREAL_0:2;
thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos i)
by SCMPDS_5:39
.=
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos i)
by A56, SCMPDS_6:88
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos i)
by SCMPDS_5:45
.=
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos i)
by A47, A58, AMI_3:52, SCMPDS_2:58
.=
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos i)
by SCMPDS_5:40
.=
s . (intpos i)
by A34, A57
;
verum
end; end; suppose A59:
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (DataLoc ((IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . GBP ),6) > 0
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP = 0 & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )hence (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP =
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP
by SCMPDS_6:87
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . GBP
by SCMPDS_5:47
.=
0
by A50, A51, AMI_3:52, SCMPDS_2:60
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) = s . (intpos 1) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )thus (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1) =
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 1)
by A59, SCMPDS_6:87
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos 1)
by SCMPDS_5:47
.=
s . (intpos 1)
by A54, A51, AMI_3:52, SCMPDS_2:60
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) = s . (intpos 2) & (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )thus (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2) =
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 2)
by A59, SCMPDS_6:87
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos 2)
by SCMPDS_5:47
.=
s . (intpos 2)
by A49, A51, AMI_3:52, SCMPDS_2:60
;
( (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) = s . (intpos 3) & ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) )thus (IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3) =
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 3)
by A59, SCMPDS_6:87
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos 3)
by SCMPDS_5:47
.=
s . (intpos 3)
by A48, A51, AMI_3:52, SCMPDS_2:60
;
for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i)hereby verum
let i be
Element of
NAT ;
( i >= 8 implies (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) )assume A60:
i >= 8
;
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i)then A61:
i > 7
by XXREAL_0:2;
i > 4
by A60, XXREAL_0:2;
then A62:
intpos i <> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos i)
by SCMPDS_5:39
.=
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos i)
by A59, SCMPDS_6:87
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos i)
by SCMPDS_5:47
.=
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos i)
by A51, A61, AMI_3:52, SCMPDS_2:60
.=
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos i)
by A62, SCMPDS_2:60
.=
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos i)
by SCMPDS_5:40
.=
s . (intpos i)
by A34, A60
;
verum
end; end;
hence
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . GBP = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 1) = s . (intpos 1) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 2) = s . (intpos 2) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 3) = s . (intpos 3) )
by SCMPDS_5:39; ( ( for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i) ) & ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 ) ) & ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) ) )
thus
for i being Element of NAT st i >= 8 holds
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos i) = s . (intpos i)
by A55; ( ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 ) ) & ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) ) )
A63: (IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s) . (intpos 5) =
(Exec (AddTo GBP ,5,(- 1)),(Exec (GBP ,7 := GBP ,5),(Initialized s))) . (intpos 5)
by SCMPDS_5:47
.=
((Exec (GBP ,7 := GBP ,5),(Initialized s)) . (intpos 5)) + (- 1)
by A9, SCMPDS_2:60
.=
(s . (intpos 5)) - 1
by A18
;
A64: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 5) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 5)
by SCMPDS_5:46
.=
(s . (intpos 5)) - 1
by A63, A14, AMI_3:52, SCMPDS_2:59
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 5) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 5)
by SCMPDS_5:46
.=
(s . (intpos 5)) - 1
by A64, A21, AMI_3:52, SCMPDS_2:62
;
then A65:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 5) = (s . (intpos 5)) - 1
by SCMPDS_5:40;
A66: (IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s) . (intpos 4) =
(Exec (GBP ,6 := (intpos 4),0 ),(IExec ((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))),s)) . (intpos 4)
by SCMPDS_5:46
.=
me
by A11, A14, AMI_3:52, SCMPDS_2:59
;
(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s) . (intpos 4) =
(Exec (SubFrom GBP ,6,(intpos 2),0 ),(IExec (((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )),s)) . (intpos 4)
by SCMPDS_5:46
.=
me
by A66, A21, AMI_3:52, SCMPDS_2:62
;
then A67:
(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 4) = s . (intpos 4)
by A2, SCMPDS_5:40;
A68:
DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4 = intpos (0 + 4)
by A46, SCMP_GCD:5;
hereby ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) ) )
A69:
intpos 5
<> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
assume A70:
s . (intpos md) < s . (intpos me)
;
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = (s . (intpos 5)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 )thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 5)
by SCMPDS_5:39
.=
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 5)
by A53, A70, SCMPDS_6:87, XREAL_1:52
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos 5)
by SCMPDS_5:47
.=
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 5)
by A51, AMI_3:52, SCMPDS_2:60
.=
(s . (intpos 5)) - 1
by A65, A69, SCMPDS_2:60
;
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = (s . (intpos 4)) - 1 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1 )thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 4)
by SCMPDS_5:39
.=
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 4)
by A53, A70, SCMPDS_6:87, XREAL_1:52
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos 4)
by SCMPDS_5:47
.=
(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 4)
by A51, AMI_3:52, SCMPDS_2:60
.=
((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 4)) + (- 1)
by A68, SCMPDS_2:60
.=
(s . (intpos 4)) - 1
by A67
;
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = (s . (intpos 5)) - 1A71:
intpos 7
<> DataLoc ((Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . GBP ),4
by A46, AMI_3:52, SCMP_GCD:5;
thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 7)
by SCMPDS_5:39
.=
(IExec ((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 7)
by A53, A70, SCMPDS_6:87, XREAL_1:52
.=
(Exec (AddTo GBP ,7,(- 1)),(Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)))) . (intpos 7)
by SCMPDS_5:47
.=
((Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 7)) + (- 1)
by A51, SCMPDS_2:60
.=
((Exec (AddTo GBP ,4,(- 1)),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 7)) - 1
.=
(s . (intpos 5)) - 1
by A25, A71, SCMPDS_2:60
;
verum
end;
hereby verum
assume A72:
s . (intpos md) >= s . (intpos me)
;
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) = 0 & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) )thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 5) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 5)
by SCMPDS_5:39
.=
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 5)
by A53, A72, SCMPDS_6:88, XREAL_1:49
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 5)
by SCMPDS_5:45
.=
0
by A47, SCMPDS_2:58
;
( (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) = s . (intpos 4) & (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5) )thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 4) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 4)
by SCMPDS_5:39
.=
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 4)
by A53, A72, SCMPDS_6:88, XREAL_1:49
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 4)
by SCMPDS_5:45
.=
s . (intpos 4)
by A47, A67, AMI_3:52, SCMPDS_2:58
;
(IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) = s . (intpos 5)thus (IExec (((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )) ';' (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 )))),s) . (intpos 7) =
(IExec (if>0 GBP ,6,((AddTo GBP ,4,(- 1)) ';' (AddTo GBP ,7,(- 1))),(Load (GBP ,5 := 0 ))),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 7)
by SCMPDS_5:39
.=
(IExec (Load (GBP ,5 := 0 )),(IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s)) . (intpos 7)
by A53, A72, SCMPDS_6:88, XREAL_1:49
.=
(Exec (GBP ,5 := 0 ),(Initialized (IExec ((((GBP ,7 := GBP ,5) ';' (AddTo GBP ,5,(- 1))) ';' (GBP ,6 := (intpos 4),0 )) ';' (SubFrom GBP ,6,(intpos 2),0 )),s))) . (intpos 7)
by SCMPDS_5:45
.=
s . (intpos 5)
by A25, A47, AMI_3:52, SCMPDS_2:58
;
verum
end;