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 A1, INT_1:3;
A10: n + fr < pD by A4, A5, XXREAL_0:2;
set i2 = AddTo ((intpos sp),fr,(intpos pD),0);
set i3 = AddTo ((intpos pp),0,1);
set I = (AddTo ((intpos sp),fr,(intpos pD),0)) ';' (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 A1, XXREAL_0:2;
A12: n + fr > n + cv by A2, XREAL_1:6;
then n + cv < pp by A4, XXREAL_0:2;
then A13: n + cv < pD by A5, XXREAL_0:2;
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 FINSEQ_2:24, NUMBERS:19;
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)),(Initialize u));
A27: DataLoc (((Initialize u) . (intpos sp)),fr) = DataLoc (n,fr) by A16, A26, SCMPDS_5:15
.= intpos (n + fr) by SCMP_GCD:1 ;
then A28: |.(((Initialize u) . (intpos sp)) + fr).| = n + fr by XTUPLE_0:1;
then A29: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp) = (Initialize u) . (intpos pp) by A3, A5, A7, A27, SCMPDS_2:49
.= 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)),(Initialize u))) . (intpos pp) = pD by A17, A25, A29;
then ((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0 <> sp by A4, A5, A11, XXREAL_0:2;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0).| <> sp by A30, ABSVALUE:def 1;
then A31: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)),0) <> intpos sp by XTUPLE_0:1;
A32: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos sp) = (Initialize u) . (intpos sp) by A1, A7, A27, A28, SCMPDS_2:49
.= 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)),(Initialize u))))) . (intpos sp) by A24, SCMPDS_5:42
.= u . (intpos sp) by A32, A31, SCMPDS_2:48 ; :: 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 A16, SCMP_GCD:1;
then A34: |.((t . (intpos sp)) + cv).| = n + cv by XTUPLE_0:1;
then |.(((Initialize u) . (intpos sp)) + fr).| <> |.((t . (intpos sp)) + cv).| by A2, A28;
then A35: DataLoc (((Initialize u) . (intpos sp)),fr) <> DataLoc ((t . (intpos sp)),cv) by XTUPLE_0:1;
A36: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)),0) = intpos (pD + 0) by A30, SCMP_GCD:1;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0).| = pD + 0 by XTUPLE_0:1;
then |.(((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0).| <> |.((t . (intpos sp)) + cv).| by A4, A5, A12, A34, XXREAL_0:2;
then A37: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (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)),(Initialize u))))) . (DataLoc ((t . (intpos sp)),cv)) by A24, SCMPDS_5:42
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (DataLoc ((t . (intpos sp)),cv)) by A37, SCMPDS_2:48
.= (Initialize u) . (DataLoc ((t . (intpos sp)),cv)) by A35, SCMPDS_2:49
.= 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 SCMPDS_6:20, SCMPDS_6:21; :: 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,(Initialize u))) . (intpos pp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))))) . (intpos pp) by SCMPDS_5:42
.= u . (intpos pp) by A3, A6, A29, A36, SCMPDS_2:48 ;
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 A39, TARSKI:def 2;
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 A38, MEMSTR_0:44; :: 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 A16, SCMP_GCD:1;
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 A1, A7, A16, SCMPDS_2:49;
(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp) = t . (intpos pp) by A3, A5, A7, A16, SCMPDS_2:49;
then A43: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),t)) . (intpos pp)),0) = intpos (pD + 0) by A17, SCMP_GCD:1;
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 A4, A5, A11, XXREAL_0:2;
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 A42, A45, SCMPDS_2:48 ;
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 A16, SCMP_GCD:1;
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 A4, A5, A12, XXREAL_0:2;
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 A20, A21;
n + fr <> |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| by A2, A48;
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 A40, XTUPLE_0:1;
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 A6, A7, A43, SCMPDS_2:48
.= (t . (DataLoc ((s . (intpos sp)),fr))) + (f . 1) by A16, A50, SCMPDS_2:49 ;
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 A51, A52, SCMPDS_2:48 ;
n + cv <> sp by A1, NAT_1:11;
then |.(n + cv).| <> sp by ABSVALUE:def 1;
then A54: DataLoc ((t . (intpos sp)),cv) <> intpos sp by A16, XTUPLE_0:1;
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 A49, SCMPDS_2:48
.= (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 A43, SCMPDS_2:48
.= (t . (intpos pD)) + 1 by A6, A7, A16, SCMPDS_2:49 ;
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 A18, XXREAL_0:2;
1 <= k + 1 by NAT_1:11;
then 1 in Seg (k + 1) by FINSEQ_1:1;
then A57: 1 in dom f by A20, FINSEQ_1:def 3;
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;
A60: (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)) = (Initialize (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)) 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 A18, INT_1:3;
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;
A65: (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)) = (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 SCMPDS_5:15;
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 A55, A59, SCMP_GCD:1;
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 A59, XTUPLE_0:1;
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 A18, A44, NAT_1:11;
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 A59, XTUPLE_0:1;
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 A10, A18, A41, A66, XXREAL_0:2;
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 A59, XTUPLE_0:1;
n + cv < m by A13, A18, XXREAL_0:2;
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 A48, A66, NAT_1:11;
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 A59, XTUPLE_0:1;
A70: (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)) = (Exec ((AddTo ((intpos sp),cv,(- 1))),(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 SCMPDS_5:41
.= (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 A69, SCMPDS_2:48
.= (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 A67, SCMPDS_2:48
.= 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 A68, SCMPDS_2:49 ;
0 + 1 <= i + 1 by XREAL_1:6;
hence (Del (f,1)) . (i + 1) = f . ((i + 1) + 1) by A57, WSIERP_1:def 1
.= t . (DataLoc ((t . (intpos pD)),(i + 1))) by A21, A58, A64
.= (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 A66, A70, A65, SCMPDS_5:15 ;
:: thesis: verum
end;
|.((t . (intpos sp)) + fr).| <> n + cv by A2, A41;
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 A4, A5, A12, A44, XXREAL_0:2;
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 A72, SCMPDS_2:48
.= t . (intpos (n + cv)) by A71, SCMPDS_2:49
.= k + 1 by A16, A19, A20, SCMP_GCD:1 ;
|.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| <> sp by A1, A48, NAT_1:11;
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 A16, A46, A74, SCMPDS_2:48 ;
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 A47, SCMPDS_2:48
.= len (Del (f,1)) by A20, A58, A73 ;
pp <> |.(((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv).| by A2, A4, A48, XREAL_1:6;
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 A77, SCMPDS_2:48
.= (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 A3, A6, A43, SCMPDS_2:48
.= pD by A17, A3, A5, A7, A16, SCMPDS_2:49 ;
1 <= len f by A20, NAT_1:11;
then A79: 1 in dom f by FINSEQ_3:25;
n + cv <> pp by A2, A4, XREAL_1:6;
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 A16, A54, TARSKI:def 2;
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 A79, A22, WSIERP_1:20 ;
:: 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 A80, Th45, A82, RVSUM_1:72; :: thesis: verum
end;
then A83: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A83, A14);
 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