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