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 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 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) ) ) )
A1:
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 A2:
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 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 A3:
(Initialize s) . GBP = 0
by SCMPDS_5:15;
then A4:
DataLoc (((Initialize s) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
then A5:
(Exec ((AddTo (GBP,3,1)),s)) . GBP = 0
by A3, A2, AMI_3:10, SCMPDS_2:48;
then A6:
DataLoc (((Exec ((AddTo (GBP,3,1)),s)) . GBP),4) = intpos (0 + 4)
by SCMP_GCD:1;
A7:
(Exec ((AddTo (GBP,3,1)),s)) . (intpos 2) = s . (intpos 2)
by A4, A2, A3, AMI_3:10, SCMPDS_2:48;
A8: (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 A7, A6, AMI_3:10, SCMPDS_2:47
;
A9:
(Exec ((AddTo (GBP,3,1)),s)) . (intpos 1) = s . (intpos 1)
by A4, A2, A3, AMI_3:10, SCMPDS_2:48;
A10: (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 A9, A6, AMI_3:10, SCMPDS_2:47
;
A11:
(Exec ((AddTo (GBP,3,1)),s)) . (intpos 3) = (s . (intpos 3)) + 1
by A4, A1, SCMPDS_2:48;
A12: (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 A5, A6, AMI_3:10, SCMPDS_2:47
;
then A13:
DataLoc (((IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . GBP),1) = intpos (0 + 1)
by SCMP_GCD:1;
A14:
DataLoc (((Exec ((AddTo (GBP,3,1)),s)) . GBP),3) = intpos (0 + 3)
by A5, SCMP_GCD:1;
A15: (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 A11, A6, A14, SCMPDS_2:47
;
A16: (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 A15, A13, AMI_3:10, SCMPDS_2:48
;
A17: (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 A8, A13, AMI_3:10, SCMPDS_2:48
;
A18: (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 A10, A13, SCMPDS_2:48
;
A19: (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 A11, A6, AMI_3:10, SCMPDS_2:47
;
A20: (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 A19, A13, AMI_3:10, SCMPDS_2:48
;
A21: (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 A12, A13, AMI_3:10, SCMPDS_2:48
;
then A22:
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 A21, A22, 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 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 A18, A22, 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 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 A17, A22, 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 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) ) )
A23:
DataLoc (((IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . GBP),1) = intpos (0 + 1)
by A21, 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 A20, A22, 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 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 A16, A22, 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 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 A18, A22, A23, SCMPDS_2:47
; for i being 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)
A24:
now for i being Nat st i >= 7 holds
(Exec ((AddTo (GBP,3,1)),s)) . (intpos i) = s . (intpos i)let i be
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 A4, A1, AMI_3:10, SCMPDS_2:48
.=
s . (intpos i)
by SCMPDS_5:15
;
verum end;
A25:
now for i being Nat st i >= 7 holds
(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = s . (intpos i)let i be
Nat;
( i >= 7 implies (IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = s . (intpos i) )assume A26:
i >= 7
;
(IExec (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))),P,s)) . (intpos i) = s . (intpos i)then A27:
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 A6, A27, AMI_3:10, SCMPDS_2:47
.=
s . (intpos i)
by A24, A26
;
verum end;
A28:
now for i being Nat st i >= 7 holds
(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) = s . (intpos i)let i be
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 A29:
i >= 7
;
(IExec ((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))),P,s)) . (intpos i) = s . (intpos i)then A30:
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 A13, A30, AMI_3:10, SCMPDS_2:48
.=
s . (intpos i)
by A25, A29
;
verum end;
hereby verum
let i be
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 A31:
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 A32:
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 A22, A32, AMI_3:10, SCMPDS_2:47
.=
s . (intpos i)
by A28, A31
;
verum
end;