let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Nat
for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
let s be 0 -started State of SCMPDS; :: thesis: for sp, cv, result, pp, pD being Nat
for f being FinSequence of NAT st s . (intpos sp) > sp & cv < result & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
let sp, cv, fr, pp, pD be Nat; :: thesis: for f being FinSequence of NAT st s . (intpos sp) > sp & cv < fr & (s . (intpos sp)) + fr < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,fr,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = Sum f
let f be FinSequence of NAT ; :: thesis: ( s . (intpos sp) > sp & cv < fr & (s . (intpos sp)) + fr < pp & pp < pD & pD < s . (intpos pD) & len f = s . (DataLoc ((s . (intpos sp)),cv)) & ( for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) implies (IExec ((sum (sp,cv,fr,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = Sum f )
set BP = intpos sp;
set PD = intpos pD;
set PP = intpos pp;
assume that
A1: s . (intpos sp) > sp and
A2: cv < fr and
A3: (s . (intpos sp)) + fr < pp and
A4: pp < pD and
A5: pD < s . (intpos pD) and
A6: len f = s . (DataLoc ((s . (intpos sp)),cv)) and
A7: for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ; :: thesis: (IExec ((sum (sp,cv,fr,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = Sum f
reconsider n = s . (intpos sp) as Element of NAT by A1, INT_1:3;
A8: intpos pD <> intpos pp by A4, XTUPLE_0:1;
set i0 = ((intpos sp),fr) := 0;
set i1 = (intpos pp) := pD;
set Hi = (((intpos sp),fr) := 0) ';' ((intpos pp) := pD);
set i2 = AddTo ((intpos sp),fr,(intpos pD),0);
set i3 = AddTo ((intpos pp),0,1);
set FD = for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))));
set s2 = IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s);
set P2 = P;
set s0 = s;
set s1 = Exec ((((intpos sp),fr) := 0),s);
set a = DataLoc ((s . (intpos sp)),fr);
set a1 = DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr);
A9: DataLoc ((s . (intpos sp)),fr) = intpos (n + fr) by SCMP_GCD:1;
then A10: |.((s . (intpos sp)) + fr).| = n + fr by XTUPLE_0:1;
then |.((s . (intpos sp)) + fr).| <> sp by A1, NAT_1:12;
then A11: DataLoc ((s . (intpos sp)),fr) <> intpos sp by XTUPLE_0:1;
A12: DataLoc ((s . (intpos sp)),fr) <> intpos pD by A3, A4, A9, XTUPLE_0:1;
A13: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD) = (Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos pD) by SCMPDS_5:42
.= (Exec ((((intpos sp),fr) := 0),s)) . (intpos pD) by A8, SCMPDS_2:45
.= s . (intpos pD) by A12, SCMPDS_2:46 ;
n <= n + fr by NAT_1:12;
then sp <> pp by A1, A3, XXREAL_0:2;
then A14: intpos sp <> intpos pp by XTUPLE_0:1;
A15: intpos (n + fr) <> intpos pp by A3, XTUPLE_0:1;
A16: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp) = (Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos sp) by SCMPDS_5:42
.= (Exec ((((intpos sp),fr) := 0),s)) . (intpos sp) by A14, SCMPDS_2:45
.= n by A11, SCMPDS_2:46 ;
then A17: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr)) = (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos (n + fr)) by SCMP_GCD:1
.= (Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos (n + fr)) by SCMPDS_5:42
.= (Exec ((((intpos sp),fr) := 0),s)) . (intpos (n + fr)) by A15, SCMPDS_2:45
.= 0 by A9, SCMPDS_2:46 ;
A18: n + fr < pD by A3, A4, XXREAL_0:2;

A19: now :: thesis: for k being Nat st k < len f holds
(Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) = f . (k + 1)

reconsider m = s . (intpos pD) as Element of NAT by A5, INT_1:3;
let k be Nat; :: thesis: ( k < len f implies (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) = f . (k + 1) )
assume A20: k < len f ; :: thesis: (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) = f . (k + 1)
pp < m by A4, A5, XXREAL_0:2;
then m + k <> pp by NAT_1:11;
then A21: intpos (m + k) <> intpos pp by XTUPLE_0:1;
m <= m + k by NAT_1:11;
then |.((s . (intpos sp)) + fr).| <> m + k by A5, A10, A18, XXREAL_0:2;
then A22: DataLoc ((s . (intpos sp)),fr) <> intpos (m + k) by XTUPLE_0:1;
thus (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) = (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) by SCMPDS_5:15
.= (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos (m + k)) by A13, SCMP_GCD:1
.= (Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos (m + k)) by SCMPDS_5:42
.= (Exec ((((intpos sp),fr) := 0),s)) . (intpos (m + k)) by A21, SCMPDS_2:45
.= s . (intpos (m + k)) by A22, SCMPDS_2:46
.= s . (DataLoc ((s . (intpos pD)),k)) by SCMP_GCD:1
.= f . (k + 1) by A7, A20 ; :: thesis: verum

end;

|.((s . (intpos sp)) + fr).| <> n + cv by A2, A10;
then A23: DataLoc ((s . (intpos sp)),fr) <> intpos (n + cv) by XTUPLE_0:1;
n + cv <> pp by A2, A3, XREAL_1:6;
then A24: intpos (n + cv) <> intpos pp by XTUPLE_0:1;
A25: (((intpos sp),fr) := 0) ';' ((intpos pp) := pD) is_halting_on s,P by SCMPDS_6:21;
A26: (((intpos sp),fr) := 0) ';' ((intpos pp) := pD) is_closed_on s,P by SCMPDS_6:20;
A27: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pp) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (intpos pp) by SCMPDS_5:15;
A28: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (intpos sp) by SCMPDS_5:15;
A29: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (intpos pD) by SCMPDS_5:15;
A30: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pp) = (Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos pp) by SCMPDS_5:42
.= pD by SCMPDS_2:45 ;
then for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)),P by A1, A2, A3, A4, A5, A16, A13, Th51, A27, A28, A29;
then A31: for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s),P by SCMPDS_6:126;
A32: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),cv)) = (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos (n + cv)) by A16, SCMP_GCD:1
.= (Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos (n + cv)) by SCMPDS_5:42
.= (Exec ((((intpos sp),fr) := 0),s)) . (intpos (n + cv)) by A24, SCMPDS_2:45
.= s . (intpos (n + cv)) by A23, SCMPDS_2:46
.= len f by A6, SCMP_GCD:1 ;
A33: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr)) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr)) by SCMPDS_5:15;
A34: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),cv)) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),cv)) by SCMPDS_5:15;
for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)),P by A1, A2, A3, A4, A5, A16, A30, A13, Th51, A27, A28, A29;
then for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s),P by SCMPDS_6:125;
hence (IExec ((sum (sp,cv,fr,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,(Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr)) by A16, A26, A25, A31, Th28
.= Sum f by A1, A2, A3, A4, A5, A16, A30, A13, A17, A32, A19, Th52, A27, A28, A29, A33, A34 ;
:: thesis: verum