let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS st s . GBP = 0 holds
( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP = 0 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
set a = GBP ;
let s be 0 -started State of SCMPDS; ( s . GBP = 0 implies ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP = 0 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) ) )
set t0 = Initialize s;
set t1 = IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s));
set t2 = IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s));
set t3 = IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s));
set t4 = Exec (((GBP,5) := (GBP,4)),(Initialize s));
assume
s . GBP = 0
; ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP = 0 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
then A1:
(Initialize s) . GBP = 0
by SCMPDS_5:15;
then A2:
DataLoc (((Initialize s) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:1;
then A3: (Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos 5) =
(Initialize s) . (DataLoc (((Initialize s) . GBP),4))
by SCMPDS_2:47
.=
(Initialize s) . (intpos (0 + 4))
by A1, SCMP_GCD:1
.=
s . (intpos 4)
by SCMPDS_5:15
;
(Initialize s) . (intpos 4) = s . (intpos 4)
by SCMPDS_5:15;
then A4:
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos 4) = s . (intpos 4)
by A2, AMI_3:10, SCMPDS_2:47;
(Initialize s) . (intpos 1) = s . (intpos 1)
by SCMPDS_5:15;
then A5:
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos 1) = s . (intpos 1)
by A2, AMI_3:10, SCMPDS_2:47;
A6:
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . GBP = 0
by A1, A2, AMI_3:10, SCMPDS_2:47;
then A7:
DataLoc (((Exec (((GBP,5) := (GBP,4)),(Initialize s))) . GBP),5) = intpos (0 + 5)
by SCMP_GCD:1;
A8: (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . GBP =
(Exec ((SubFrom (GBP,5,GBP,2)),(Exec (((GBP,5) := (GBP,4)),(Initialize s))))) . GBP
by SCMPDS_5:42
.=
0
by A6, A7, AMI_3:10, SCMPDS_2:50
;
then A9:
DataLoc (((IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
A10: (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos 4) =
(Exec ((SubFrom (GBP,5,GBP,2)),(Exec (((GBP,5) := (GBP,4)),(Initialize s))))) . (intpos 4)
by SCMPDS_5:42
.=
s . (intpos 4)
by A4, A7, AMI_3:10, SCMPDS_2:50
;
A11: (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos 4) =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . (intpos 4)
by SCMPDS_5:41
.=
s . (intpos 4)
by A10, A9, AMI_3:10, SCMPDS_2:47
;
A12:
(Initialize s) . (intpos 2) = s . (intpos 2)
by SCMPDS_5:15;
then A13:
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos 2) = s . (intpos 2)
by A2, AMI_3:10, SCMPDS_2:47;
A14: (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos 5) =
(Exec ((SubFrom (GBP,5,GBP,2)),(Exec (((GBP,5) := (GBP,4)),(Initialize s))))) . (intpos 5)
by SCMPDS_5:42
.=
((Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos 5)) - ((Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (DataLoc (((Exec (((GBP,5) := (GBP,4)),(Initialize s))) . GBP),2)))
by A7, SCMPDS_2:50
.=
((Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos 5)) - ((Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos (0 + 2)))
by A6, SCMP_GCD:1
.=
(s . (intpos 4)) - (s . (intpos 2))
by A12, A2, A3, AMI_3:10, SCMPDS_2:47
;
A15: (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos 5) =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . (intpos 5)
by SCMPDS_5:41
.=
(s . (intpos 4)) - (s . (intpos 2))
by A14, A9, AMI_3:10, SCMPDS_2:47
;
A16: (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos 2) =
(Exec ((SubFrom (GBP,5,GBP,2)),(Exec (((GBP,5) := (GBP,4)),(Initialize s))))) . (intpos 2)
by SCMPDS_5:42
.=
s . (intpos 2)
by A13, A7, AMI_3:10, SCMPDS_2:50
;
A17: (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos 1) =
(Exec ((SubFrom (GBP,5,GBP,2)),(Exec (((GBP,5) := (GBP,4)),(Initialize s))))) . (intpos 1)
by SCMPDS_5:42
.=
s . (intpos 1)
by A5, A7, AMI_3:10, SCMPDS_2:50
;
A18: (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos 1) =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . (intpos 1)
by SCMPDS_5:41
.=
s . (intpos 1)
by A17, A9, AMI_3:10, SCMPDS_2:47
;
A19: (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . GBP =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . GBP
by SCMPDS_5:41
.=
0
by A8, A9, AMI_3:10, SCMPDS_2:47
;
then A20:
DataLoc (((IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
A21: (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos 3) =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . (intpos 3)
by SCMPDS_5:41
.=
(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (DataLoc (((IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . GBP),2))
by A9, SCMPDS_2:47
.=
s . (intpos 2)
by A8, A16, SCMP_GCD:1
;
A22: (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos 2) =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . (intpos 2)
by SCMPDS_5:41
.=
s . (intpos 2)
by A16, A9, AMI_3:10, SCMPDS_2:47
;
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . GBP =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . GBP
by SCMPDS_5:41
.=
0
by A19, A20, AMI_3:10, SCMPDS_2:48
; ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . (intpos 1)
by SCMPDS_5:41
.=
s . (intpos 1)
by A18, A20, AMI_3:10, SCMPDS_2:48
; ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . (intpos 2)
by SCMPDS_5:41
.=
s . (intpos 2)
by A22, A20, AMI_3:10, SCMPDS_2:48
; ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . (intpos 3)
by SCMPDS_5:41
.=
(s . (intpos 2)) + 1
by A21, A20, SCMPDS_2:48
; ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . (intpos 4)
by SCMPDS_5:41
.=
s . (intpos 4)
by A11, A20, AMI_3:10, SCMPDS_2:48
; ( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . (intpos 5)
by SCMPDS_5:41
.=
(s . (intpos 4)) - (s . (intpos 2))
by A15, A20, AMI_3:10, SCMPDS_2:48
; for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i)
A23:
now for i being Nat st i >= 8 holds
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 8 implies (Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos i) = s . (intpos i) )assume
i >= 8
;
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos i) = s . (intpos i)then
i > 5
by XXREAL_0:2;
hence (Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos i) =
(Initialize s) . (intpos i)
by A2, AMI_3:10, SCMPDS_2:47
.=
s . (intpos i)
by SCMPDS_5:15
;
verum end;
A24:
now for i being Nat st i >= 8 holds
(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 8 implies (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos i) = s . (intpos i) )assume A25:
i >= 8
;
(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos i) = s . (intpos i)then A26:
i > 5
by XXREAL_0:2;
thus (IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos i) =
(Exec ((SubFrom (GBP,5,GBP,2)),(Exec (((GBP,5) := (GBP,4)),(Initialize s))))) . (intpos i)
by SCMPDS_5:42
.=
(Exec (((GBP,5) := (GBP,4)),(Initialize s))) . (intpos i)
by A7, A26, AMI_3:10, SCMPDS_2:50
.=
s . (intpos i)
by A23, A25
;
verum end;
A27:
now for i being Nat st i >= 8 holds
(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 8 implies (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos i) = s . (intpos i) )assume A28:
i >= 8
;
(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos i) = s . (intpos i)then A29:
i > 3
by XXREAL_0:2;
thus (IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos i) =
(Exec (((GBP,3) := (GBP,2)),(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))))) . (intpos i)
by SCMPDS_5:41
.=
(IExec ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))),P,(Initialize s))) . (intpos i)
by A9, A29, AMI_3:10, SCMPDS_2:47
.=
s . (intpos i)
by A24, A28
;
verum end;
hereby verum
let i be
Nat;
( i >= 8 implies (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) )assume A30:
i >= 8
;
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i)then A31:
i > 3
by XXREAL_0:2;
thus (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) =
(Exec ((AddTo (GBP,3,1)),(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))))) . (intpos i)
by SCMPDS_5:41
.=
(IExec (((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))),P,(Initialize s))) . (intpos i)
by A20, A31, AMI_3:10, SCMPDS_2:48
.=
s . (intpos i)
by A27, A30
;
verum
end;