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)) . (intpos 3) = n
let s be 0 -started State of SCMPDS; :: thesis: for n being Nat holds (IExec ((sum n),P,s)) . (intpos 3) = n
let n be Nat; :: thesis: (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 ;
:: thesis: verum