let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for n being Nat holds (IExec ((sum n),P,s)) . () = n

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