let s be 0 -started State of SCMPDS; for n being Element of NAT holds (IExec ((sum n),s)) . (intpos 3) = n
let n be Element of NAT ; (IExec ((sum n),s)) . (intpos 3) = n
set i1 = GBP := 0;
set i2 = (GBP,2) := n;
set i3 = (GBP,3) := 0;
set i4 = AddTo (GBP,3,1);
set FD = for-down (GBP,2,1,(Load (AddTo (GBP,3,1))));
set a = intpos 3;
set I2 = (GBP := 0) ';' ((GBP,2) := n);
set s1 = IExec (((GBP := 0) ';' ((GBP,2) := n)),s);
set s2 = Exec ((GBP := 0),(Initialize s));
set I3 = ((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0);
set s3 = IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s);
A1:
((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0) is_closed_on s
by SCMPDS_6:34;
A2:
((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0) is_halting_on s
by SCMPDS_6:35;
A3:
(Exec ((GBP := 0),(Initialize s))) . GBP = 0
by SCMPDS_2:57;
then A4:
DataLoc (((Exec ((GBP := 0),(Initialize s))) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:5;
A5: (IExec (((GBP := 0) ';' ((GBP,2) := n)),s)) . GBP =
(Exec (((GBP,2) := n),(Exec ((GBP := 0),(Initialize s))))) . GBP
by SCMPDS_5:47
.=
0
by A3, A4, AMI_3:52, SCMPDS_2:58
;
then A6:
DataLoc (((IExec (((GBP := 0) ';' ((GBP,2) := n)),s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:5;
X3:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s))) . GBP = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . GBP
by SCMPDS_5:40;
A7: (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . GBP =
(Exec (((GBP,3) := 0),(IExec (((GBP := 0) ';' ((GBP,2) := n)),s)))) . GBP
by SCMPDS_5:46
.=
0
by A5, A6, AMI_3:52, SCMPDS_2:58
;
then
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s))
by Th69, X3;
then A8:
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)
by SCMPDS_6:140;
A9: (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . (intpos 2) =
(Exec (((GBP,3) := 0),(IExec (((GBP := 0) ';' ((GBP,2) := n)),s)))) . (intpos 2)
by SCMPDS_5:46
.=
(IExec (((GBP := 0) ';' ((GBP,2) := n)),s)) . (intpos 2)
by A6, AMI_3:52, SCMPDS_2:58
.=
(Exec (((GBP,2) := n),(Exec ((GBP := 0),(Initialize s))))) . (intpos 2)
by SCMPDS_5:47
.=
n
by A4, SCMPDS_2:58
;
A10: (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . (intpos 3) =
(Exec (((GBP,3) := 0),(IExec (((GBP := 0) ';' ((GBP,2) := n)),s)))) . (intpos 3)
by SCMPDS_5:46
.=
0
by A6, SCMPDS_2:58
;
X1:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s))) . (intpos 2) = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . (intpos 2)
by SCMPDS_5:40;
X2:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s))) . (intpos 3) = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . (intpos 3)
by SCMPDS_5:40;
X3:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s))) . GBP = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)) . GBP
by SCMPDS_5:40;
X4:
IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)))) = IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),(IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)))
by SCMPDS_5:48;
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s))
by A7, Th69, X3;
then
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)
by SCMPDS_6:139;
hence (IExec ((sum n),s)) . (intpos 3) =
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),(IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),s)))) . (intpos 3)
by A1, A2, A8, Th49
.=
n
by A10, A7, A9, Th70, X1, X2, X3, X4
;
verum