let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n
let s be 0 -started State of SCMPDS; for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n
let n be Nat; (IExec ((sum n),P,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)),P,s);
set s2 = Exec ((GBP := 0),s);
set I3 = ((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0);
set s3 = IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s);
set P3 = P;
A1:
((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0) is_closed_on s,P
by SCMPDS_6:20;
A2:
((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0) is_halting_on s,P
by SCMPDS_6:21;
A3:
(Exec ((GBP := 0),s)) . GBP = 0
by SCMPDS_2:45;
then A4:
DataLoc (((Exec ((GBP := 0),s)) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:1;
A5: (IExec (((GBP := 0) ';' ((GBP,2) := n)),P,s)) . GBP =
(Exec (((GBP,2) := n),(Exec ((GBP := 0),s)))) . GBP
by SCMPDS_5:42
.=
0
by A3, A4, AMI_3:10, SCMPDS_2:46
;
then A6:
DataLoc (((IExec (((GBP := 0) ';' ((GBP,2) := n)),P,s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
A7:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s))) . GBP = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . GBP
by SCMPDS_5:15;
A8: (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . GBP =
(Exec (((GBP,3) := 0),(IExec (((GBP := 0) ';' ((GBP,2) := n)),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A5, A6, AMI_3:10, SCMPDS_2:46
;
then
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)),P
by Th48, A7;
then A9:
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s),P
by SCMPDS_6:126;
A10: (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . (intpos 2) =
(Exec (((GBP,3) := 0),(IExec (((GBP := 0) ';' ((GBP,2) := n)),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
(IExec (((GBP := 0) ';' ((GBP,2) := n)),P,s)) . (intpos 2)
by A6, AMI_3:10, SCMPDS_2:46
.=
(Exec (((GBP,2) := n),(Exec ((GBP := 0),s)))) . (intpos 2)
by SCMPDS_5:42
.=
n
by A4, SCMPDS_2:46
;
A11: (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . (intpos 3) =
(Exec (((GBP,3) := 0),(IExec (((GBP := 0) ';' ((GBP,2) := n)),P,s)))) . (intpos 3)
by SCMPDS_5:41
.=
0
by A6, SCMPDS_2:46
;
A12:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s))) . (intpos 2) = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . (intpos 2)
by SCMPDS_5:15;
A13:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s))) . (intpos 3) = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . (intpos 3)
by SCMPDS_5:15;
A14:
(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s))) . GBP = (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)) . GBP
by SCMPDS_5:15;
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)),P
by A8, Th48, A14;
then
for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s),P
by SCMPDS_6:125;
hence (IExec ((sum n),P,s)) . (intpos 3) =
(IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s))))) . (intpos 3)
by A1, A2, A9, Th28
.=
n
by A11, A8, A10, Th49, A12, A13, A14
;
verum