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