let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCMPDS
for n being Element of NAT holds (IExec ((sum n),P,s)) . (intpos 3) = n
let s be 0 -started State of SCMPDS; :: thesis: for n being Element of NAT holds (IExec ((sum n),P,s)) . (intpos 3) = n
let n be Element of 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),(Initialize 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:34;
A2: ((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0) is_halting_on s,P 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)),P,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)),P,s)) . GBP),3) = intpos (0 + 3) by SCMP_GCD:5;
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:40;
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: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)),P,s)),P by Th69, 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:140;
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:46
.= (IExec (((GBP := 0) ';' ((GBP,2) := n)),P,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 ;
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:46
.= 0 by A6, SCMPDS_2:58 ;
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:40;
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:40;
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:40;
A15: IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(Initialize (IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)))) = IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,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)),P,s)),P by A8, Th69, 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:139;
hence (IExec ((sum n),P,s)) . (intpos 3) = (IExec ((for-down (GBP,2,1,(Load (AddTo (GBP,3,1))))),P,(IExec ((((GBP := 0) ';' ((GBP,2) := n)) ';' ((GBP,3) := 0)),P,s)))) . (intpos 3) by A1, A2, A9, Th49
.= n by A11, A8, A10, Th70, A12, A13, A14, A15 ;
:: thesis: verum