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 pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),result)) = 0 & 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 ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),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 pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),result)) = 0 & 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 ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),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 pp) = pD & (s . (intpos sp)) + fr < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),fr)) = 0 & 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 ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = Sum f

let f be FinSequence of NAT ; :: thesis: ( s . (intpos sp) > sp & cv < fr & s . (intpos pp) = pD & (s . (intpos sp)) + fr < pp & pp < pD & pD < s . (intpos pD) & s . (DataLoc ((s . (intpos sp)),fr)) = 0 & 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 ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),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 pp) = pD and
A4: (s . (intpos sp)) + fr < pp and
A5: pp < pD and
A6: pD < s . (intpos pD) and
A7: s . (DataLoc ((s . (intpos sp)),fr)) = 0 and
A8: len f = s . (DataLoc ((s . (intpos sp)),cv)) and
A9: for k being Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ; :: thesis: (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = Sum f
reconsider n = s . (intpos sp) as Element of NAT by ;
A10: n + fr < pD by ;
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 a = DataLoc ((s . (intpos sp)),fr);
defpred S1[ Nat] means for Q being Instruction-Sequence of SCMPDS
for t being 0 -started State of SCMPDS
for f being FinSequence of NAT st t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = \$1 & ( for k being Nat st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ) holds
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)));
n <= n + fr by NAT_1:11;
then A11: sp < n + fr by ;
A12: n + fr > n + cv by ;
then n + cv < pp by ;
then A13: n + cv < pD by ;
A14: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A15: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for t being 0 -started State of SCMPDS
for f being FinSequence of NAT
for Q being Instruction-Sequence of SCMPDS st t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = k + 1 & ( for i being Nat st i < len f holds
f . (i + 1) = t . (DataLoc ((t . (intpos pD)),i)) ) holds
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))
let t be 0 -started State of SCMPDS; :: thesis: for f being FinSequence of NAT
for Q being Instruction-Sequence of SCMPDS st t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = k + 1 & ( for i being Nat st i < len f holds
f . (i + 1) = t . (DataLoc ((t . (intpos pD)),i)) ) holds
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))

let f be FinSequence of NAT ; :: thesis: for Q being Instruction-Sequence of SCMPDS st t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = k + 1 & ( for i being Nat st i < len f holds
f . (i + 1) = t . (DataLoc ((t . (intpos pD)),i)) ) holds
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = k + 1 & ( for i being Nat st i < len f holds
f . (i + 1) = t . (DataLoc ((t . (intpos pD)),i)) ) implies (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr))) )

assume that
A16: t . (intpos sp) = s . (intpos sp) and
A17: t . (intpos pp) = pD and
A18: pD < t . (intpos pD) and
A19: len f = t . (DataLoc ((t . (intpos sp)),cv)) and
A20: len f = k + 1 and
A21: for i being Nat st i < len f holds
f . (i + 1) = t . (DataLoc ((t . (intpos pD)),i)) ; :: thesis: (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))
A22: f is FinSequence of REAL by ;
A23: now :: thesis: for u being 0 -started State of SCMPDS
for U being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in {(intpos sp),(intpos pp)} holds
u . x = t . x ) & u . (intpos sp) = t . (intpos sp) holds
( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (intpos sp) = u . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (DataLoc ((t . (intpos sp)),cv)) = u . (DataLoc ((t . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . y = u . y ) )
set Dv = DataLoc ((t . (intpos sp)),cv);
let u be 0 -started State of SCMPDS; :: thesis: for U being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in {(intpos sp),(intpos pp)} holds
u . x = t . x ) & u . (intpos sp) = t . (intpos sp) holds
( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (intpos sp) = u . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (DataLoc ((t . (intpos sp)),cv)) = u . (DataLoc ((t . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b4,b3)) . b5 = b3 . b5 ) )

let U be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in {(intpos sp),(intpos pp)} holds
u . x = t . x ) & u . (intpos sp) = t . (intpos sp) implies ( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (intpos sp) = u . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (DataLoc ((t . (intpos sp)),cv)) = u . (DataLoc ((t . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b3,b2)) . b4 = b2 . b4 ) ) )

A24: Initialize u = u by MEMSTR_0:44;
assume that
A25: for x being Int_position st x in {(intpos sp),(intpos pp)} holds
u . x = t . x and
A26: u . (intpos sp) = t . (intpos sp) ; :: thesis: ( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (intpos sp) = u . (intpos sp) & (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (DataLoc ((t . (intpos sp)),cv)) = u . (DataLoc ((t . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b3,b2)) . b4 = b2 . b4 ) )

set t0 = Initialize u;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),());
A27: DataLoc ((() . (intpos sp)),fr) = DataLoc (n,fr) by
.= intpos (n + fr) by SCMP_GCD:1 ;
then A28: |.((() . (intpos sp)) + fr).| = n + fr by XTUPLE_0:1;
then A29: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp) = () . (intpos pp) by
.= u . (intpos pp) by SCMPDS_5:15 ;
intpos pp in {(intpos sp),(intpos pp)} by TARSKI:def 2;
then A30: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp) = pD by ;
then ((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0 <> sp by ;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0).| <> sp by ;
then A31: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)),0) <> intpos sp by XTUPLE_0:1;
A32: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos sp) = () . (intpos sp) by
.= u . (intpos sp) by SCMPDS_5:15 ;
thus A33: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (intpos sp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())))) . (intpos sp) by
.= u . (intpos sp) by ; :: thesis: ( (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (DataLoc ((t . (intpos sp)),cv)) = u . (DataLoc ((t . (intpos sp)),cv)) & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b3,b2)) . b4 = b2 . b4 ) )

DataLoc ((t . (intpos sp)),cv) = intpos (n + cv) by ;
then A34: |.((t . (intpos sp)) + cv).| = n + cv by XTUPLE_0:1;
then |.((() . (intpos sp)) + fr).| <> |.((t . (intpos sp)) + cv).| by ;
then A35: DataLoc ((() . (intpos sp)),fr) <> DataLoc ((t . (intpos sp)),cv) by XTUPLE_0:1;
A36: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)),0) = intpos (pD + 0) by ;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0).| = pD + 0 by XTUPLE_0:1;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)) + 0).| <> |.((t . (intpos sp)) + cv).| by ;
then A37: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (intpos pp)),0) <> DataLoc ((t . (intpos sp)),cv) by XTUPLE_0:1;
thus (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (DataLoc ((t . (intpos sp)),cv)) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())))) . (DataLoc ((t . (intpos sp)),cv)) by
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())) . (DataLoc ((t . (intpos sp)),cv)) by
.= () . (DataLoc ((t . (intpos sp)),cv)) by
.= u . (DataLoc ((t . (intpos sp)),cv)) by SCMPDS_5:15 ; :: thesis: ( (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U & ( for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b3,b2)) . b4 = b2 . b4 ) )

thus ( (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_closed_on u,U & (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)) is_halting_on u,U ) by ; :: thesis: for y being Int_position st y in {(intpos sp),(intpos pp)} holds
(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b3,b2)) . b4 = b2 . b4

A38: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,())) . (intpos pp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),())))) . (intpos pp) by SCMPDS_5:42
.= u . (intpos pp) by ;
let y be Int_position; :: thesis: ( y in {(intpos sp),(intpos pp)} implies (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b2,b1)) . b3 = b1 . b3 )
assume A39: y in {(intpos sp),(intpos pp)} ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b2,b1)) . b3 = b1 . b3
per cases ( y = intpos sp or y = intpos pp ) by ;
suppose y = intpos sp ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b2,b1)) . b3 = b1 . b3
hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . y = u . y by A33; :: thesis: verum
end;
suppose y = intpos pp ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),b2,b1)) . b3 = b1 . b3
hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . y = u . y by ; :: thesis: verum
end;
end;
end;
A40: DataLoc ((s . (intpos sp)),fr) = intpos (n + fr) by SCMP_GCD:1;
set t0 = t;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t);
set j = AddTo ((intpos sp),cv,(- 1));
set s2 = IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t);
set P2 = Q;
set g = Del (f,1);
set It = IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t);
DataLoc ((t . (intpos sp)),fr) = intpos (n + fr) by ;
then A41: |.((t . (intpos sp)) + fr).| = n + fr by XTUPLE_0:1;
A42: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos sp) = t . (intpos sp) by ;
(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp) = t . (intpos pp) by ;
then A43: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)),0) = intpos (pD + 0) by ;
then A44: |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)) + 0).| = pD + 0 by XTUPLE_0:1;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)) + 0).| <> sp by ;
then A45: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)),0) <> intpos sp by XTUPLE_0:1;
A46: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)))) . (intpos sp) by SCMPDS_5:42
.= t . (intpos sp) by ;
then A47: DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) = intpos (n + cv) by ;
then A48: |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| = n + cv by XTUPLE_0:1;
then pD <> |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| by ;
then A49: intpos pD <> DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) by XTUPLE_0:1;
A50: f . (0 + 1) = t . (DataLoc ((t . (intpos pD)),0)) by ;
n + fr <> |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| by ;
then A51: DataLoc ((s . (intpos sp)),fr) <> DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) by ;
A52: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)))) . (DataLoc ((s . (intpos sp)),fr)) by SCMPDS_5:42
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (DataLoc ((s . (intpos sp)),fr)) by
.= (t . (DataLoc ((s . (intpos sp)),fr))) + (f . 1) by ;
A53: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Exec ((AddTo ((intpos sp),cv,(- 1))),(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)))) . (DataLoc ((s . (intpos sp)),fr)) by SCMPDS_5:41
.= (f . 1) + (t . (DataLoc ((s . (intpos sp)),fr))) by ;
n + cv <> sp by ;
then |.(n + cv).| <> sp by ABSVALUE:def 1;
then A54: DataLoc ((t . (intpos sp)),cv) <> intpos sp by ;
A55: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD) = (Exec ((AddTo ((intpos sp),cv,(- 1))),(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)))) . (intpos pD) by SCMPDS_5:41
.= (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos pD) by
.= (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)))) . (intpos pD) by SCMPDS_5:42
.= ((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pD)) + 1 by
.= (t . (intpos pD)) + 1 by ;
then t . (intpos pD) < (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD) by XREAL_1:29;
then A56: pD < (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD) by ;
1 <= k + 1 by NAT_1:11;
then 1 in Seg (k + 1) by FINSEQ_1:1;
then A57: 1 in dom f by ;
then A58: (len (Del (f,1))) + 1 = len f by WSIERP_1:def 1;
A59: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD) by SCMPDS_5:15;
A61: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pp) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pp) by SCMPDS_5:15;
A62: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos sp) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos sp) by SCMPDS_5:15;
A63: for k being Nat st k < len (Del (f,1)) holds
(Del (f,1)) . (k + 1) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),k))
proof
reconsider m = t . (intpos pD) as Element of NAT by ;
let i be Nat; :: thesis: ( i < len (Del (f,1)) implies (Del (f,1)) . (i + 1) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i)) )
set SD = DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i);
assume i < len (Del (f,1)) ; :: thesis: (Del (f,1)) . (i + 1) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i))
then A64: i + 1 < (len (Del (f,1))) + 1 by XREAL_1:6;
DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i) = intpos (m + (1 + i)) by ;
then A66: |.(((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD)) + i).| = m + (1 + i) by ;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)) + 0).| <> |.(((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD)) + i).| by ;
then A67: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)),0) <> DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i) by ;
m <= m + (1 + i) by NAT_1:11;
then |.((t . (intpos sp)) + fr).| <> |.(((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD)) + i).| by ;
then A68: DataLoc ((t . (intpos sp)),fr) <> DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i) by ;
n + cv < m by ;
then |.(((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD)) + i).| <> |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| by ;
then A69: DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i) <> DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) by ;
.= (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i)) by
.= (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)))) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i)) by SCMPDS_5:42
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i)) by
.= t . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i)) by ;
0 + 1 <= i + 1 by XREAL_1:6;
hence (Del (f,1)) . (i + 1) = f . ((i + 1) + 1) by
.= t . (DataLoc ((t . (intpos pD)),(i + 1))) by
.= (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (intpos pD)),i)) by ;
:: thesis: verum
end;
|.((t . (intpos sp)) + fr).| <> n + cv by ;
then A71: DataLoc ((t . (intpos sp)),fr) <> intpos (n + cv) by XTUPLE_0:1;
|.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)) + 0).| <> n + cv by ;
then A72: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)),0) <> intpos (n + cv) by XTUPLE_0:1;
A73: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos (n + cv)) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)))) . (intpos (n + cv)) by SCMPDS_5:42
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos (n + cv)) by
.= t . (intpos (n + cv)) by
.= k + 1 by ;
|.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| <> sp by ;
then A74: DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) <> intpos sp by XTUPLE_0:1;
A75: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos sp) = (Exec ((AddTo ((intpos sp),cv,(- 1))),(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)))) . (intpos sp) by SCMPDS_5:41
.= s . (intpos sp) by ;
then DataLoc (((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos sp)),cv) = intpos (n + cv) by SCMP_GCD:1;
then A76: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (DataLoc (((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos sp)),cv)) = (Exec ((AddTo ((intpos sp),cv,(- 1))),(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)))) . (intpos (n + cv)) by SCMPDS_5:41
.= ((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos (n + cv))) + (- 1) by
.= len (Del (f,1)) by ;
pp <> |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| by ;
then A77: intpos pp <> DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) by XTUPLE_0:1;
A78: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pp) = (Exec ((AddTo ((intpos sp),cv,(- 1))),(IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)))) . (intpos pp) by SCMPDS_5:41
.= (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos pp) by
.= (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)))) . (intpos pp) by SCMPDS_5:42
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp) by
.= pD by ;
1 <= len f by ;
then A79: 1 in dom f by FINSEQ_3:25;
n + cv <> pp by ;
then |.(n + cv).| <> pp by ABSVALUE:def 1;
then DataLoc ((s . (intpos sp)),cv) <> intpos pp by XTUPLE_0:1;
then not DataLoc ((t . (intpos sp)),cv) in {(intpos sp),(intpos pp)} by ;
hence (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,(Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))))) . (DataLoc ((s . (intpos sp)),fr)) by A19, A20, A54, A23, Th47
.= (Sum (Del (f,1))) + ((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t))) . (DataLoc ((s . (intpos sp)),fr))) by A15, A20, A75, A58, A76, A78, A56, A63, A59, A60, A61, A62
.= (Sum (Del (f,1))) + ((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (DataLoc ((s . (intpos sp)),fr))) by SCMPDS_5:15
.= ((Sum (Del (f,1))) + (f . 1)) + (t . (DataLoc ((s . (intpos sp)),fr))) by A53
.= (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr))) by ;
:: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
now :: thesis: for t being 0 -started State of SCMPDS
for f being FinSequence of NAT st t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = 0 & ( for k being Nat st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ) holds
for Q being Instruction-Sequence of SCMPDS holds (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))
let t be 0 -started State of SCMPDS; :: thesis: for f being FinSequence of NAT st t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = 0 & ( for k being Nat st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ) holds
for Q being Instruction-Sequence of SCMPDS holds (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))

let f be FinSequence of NAT ; :: thesis: ( t . (intpos sp) = s . (intpos sp) & t . (intpos pp) = pD & pD < t . (intpos pD) & len f = t . (DataLoc ((t . (intpos sp)),cv)) & len f = 0 & ( for k being Nat st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ) implies for Q being Instruction-Sequence of SCMPDS holds (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr))) )

assume that
t . (intpos sp) = s . (intpos sp) and
t . (intpos pp) = pD and
pD < t . (intpos pD) and
A80: len f = t . (DataLoc ((t . (intpos sp)),cv)) and
A81: len f = 0 and
for k being Nat st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ; :: thesis: for Q being Instruction-Sequence of SCMPDS holds (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr)))
A82: Initialize t = t by MEMSTR_0:44;
f = <*> NAT by A81;
hence for Q being Instruction-Sequence of SCMPDS holds (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),Q,t)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + (t . (DataLoc ((s . (intpos sp)),fr))) by ; :: thesis: verum
end;
then A83: S1[ 0 ] ;
for k being Nat holds S1[k] from hence (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = (Sum f) + 0 by A3, A6, A7, A8, A9
.= Sum f ;
:: thesis: verum