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 ;
A8: intpos pD <> intpos pp by ;
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 ;
then A11: DataLoc ((s . (intpos sp)),fr) <> intpos sp by XTUPLE_0:1;
A12: DataLoc ((s . (intpos sp)),fr) <> intpos pD by ;
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
.= s . (intpos pD) by ;
n <= n + fr by NAT_1:12;
then sp <> pp by ;
then A14: intpos sp <> intpos pp by XTUPLE_0:1;
A15: intpos (n + fr) <> intpos pp by ;
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
.= n by ;
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
.= 0 by ;
A18: n + fr < pD by ;
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 ;
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 ;
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 ;
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
.= (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
.= s . (intpos (m + k)) by
.= s . (DataLoc ((s . (intpos pD)),k)) by SCMP_GCD:1
.= f . (k + 1) by ; :: thesis: verum
end;
|.((s . (intpos sp)) + fr).| <> n + cv by ;
then A23: DataLoc ((s . (intpos sp)),fr) <> intpos (n + cv) by XTUPLE_0:1;
n + cv <> pp by ;
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
.= (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
.= s . (intpos (n + cv)) by
.= len f by ;
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