let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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:16;
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[ Element of NAT ] means for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT
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 Element of 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:8;
then n + cv < pp by A4, XXREAL_0:2;
then A13: n + cv < pD by A5, XXREAL_0:2;
A14: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A15: S1[k] ; :: thesis: S1[k + 1]
now
let t be 0 -started State of SCMPDS; :: thesis: for f being FinSequence of NAT
for Q being the Instructions of SCMPDS -valued ManySortedSet 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 = k + 1 & ( for i being Element of 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 the Instructions of SCMPDS -valued ManySortedSet 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 = k + 1 & ( for i being Element of 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 the Instructions of SCMPDS -valued ManySortedSet 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 = k + 1 & ( for i being Element of 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 Element of 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:27;
A23: now
set Dv = DataLoc ((t . (intpos sp)),cv);
let u be 0 -started State of SCMPDS; :: thesis: for U being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 ) )
let U be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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))),U,u)) . y = u . y ) ) )
assume that
A24: for x being Int_position st x in {(intpos sp),(intpos pp)} holds
u . x = t . x and
A25: 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))),U,u)) . y = u . y ) )
set t0 = Initialize u;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u));
A26: DataLoc (((Initialize u) . (intpos sp)),fr) = DataLoc (n,fr) by A16, A25, SCMPDS_5:40
.= intpos (n + fr) by SCMP_GCD:5 ;
then A27: abs (((Initialize u) . (intpos sp)) + fr) = n + fr by ZFMISC_1:33;
then A28: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp) = (Initialize u) . (intpos pp) by A3, A5, A7, A26, SCMPDS_2:61
.= u . (intpos pp) by SCMPDS_5:40 ;
intpos pp in {(intpos sp),(intpos pp)} by TARSKI:def 2;
then A29: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp) = pD by A17, A24, A28;
then ((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0 <> sp by A4, A5, A11, XXREAL_0:2;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0) <> sp by A29, ABSVALUE:def 1;
then A30: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)),0) <> intpos sp by ZFMISC_1:33;
A31: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos sp) = (Initialize u) . (intpos sp) by A1, A7, A26, A27, SCMPDS_2:61
.= u . (intpos sp) by SCMPDS_5:40 ;
thus A32: (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 SCMPDS_5:47
.= u . (intpos sp) by A31, A30, SCMPDS_2:60 ; :: 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))),U,u)) . y = u . y ) )
DataLoc ((t . (intpos sp)),cv) = intpos (n + cv) by A16, SCMP_GCD:5;
then A33: abs ((t . (intpos sp)) + cv) = n + cv by ZFMISC_1:33;
then abs (((Initialize u) . (intpos sp)) + fr) <> abs ((t . (intpos sp)) + cv) by A2, A27;
then A34: DataLoc (((Initialize u) . (intpos sp)),fr) <> DataLoc ((t . (intpos sp)),cv) by ZFMISC_1:33;
A35: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)),0) = intpos (pD + 0) by A29, SCMP_GCD:5;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0) = pD + 0 by ZFMISC_1:33;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)) + 0) <> abs ((t . (intpos sp)) + cv) by A4, A5, A12, A33, XXREAL_0:2;
then A36: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (intpos pp)),0) <> DataLoc ((t . (intpos sp)),cv) by ZFMISC_1:33;
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 SCMPDS_5:47
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))) . (DataLoc ((t . (intpos sp)),cv)) by A36, SCMPDS_2:60
.= (Initialize u) . (DataLoc ((t . (intpos sp)),cv)) by A34, SCMPDS_2:61
.= u . (DataLoc ((t . (intpos sp)),cv)) by SCMPDS_5:40 ; :: 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))),U,u)) . y = u . y ) )
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:34, SCMPDS_6:35; :: 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))),U,u)) . y = u . y
A37: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . (intpos pp) = (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize u))))) . (intpos pp) by SCMPDS_5:47
.= u . (intpos pp) by A3, A6, A28, A35, SCMPDS_2:60 ;
hereby :: thesis: verum
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))),U,u)) . b1 = u . b1 )
assume A38: y in {(intpos sp),(intpos pp)} ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . b1 = u . b1
per cases ( y = intpos sp or y = intpos pp ) by A38, TARSKI:def 2;
suppose y = intpos sp ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . b1 = u . b1
hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . y = u . y by A32; :: thesis: verum
end;
suppose y = intpos pp ; :: thesis: (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . b1 = u . b1
hence (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),U,u)) . y = u . y by A37; :: thesis: verum
end;
end;
end;
end;
A39: DataLoc ((s . (intpos sp)),fr) = intpos (n + fr) by SCMP_GCD:5;
set t0 = Initialize t;
set t1 = Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize 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);
A40: DataLoc (((Initialize t) . (intpos sp)),fr) = DataLoc (n,fr) by A16, SCMPDS_5:40
.= intpos (n + fr) by SCMP_GCD:5 ;
then A41: abs (((Initialize t) . (intpos sp)) + fr) = n + fr by ZFMISC_1:33;
then A42: (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos sp) = (Initialize t) . (intpos sp) by A1, A7, A40, SCMPDS_2:61
.= t . (intpos sp) by SCMPDS_5:40 ;
(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp) = (Initialize t) . (intpos pp) by A3, A5, A7, A40, A41, SCMPDS_2:61
.= t . (intpos pp) by SCMPDS_5:40 ;
then A43: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) = intpos (pD + 0) by A17, SCMP_GCD:5;
then A44: abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0) = pD + 0 by ZFMISC_1:33;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0) <> sp by A4, A5, A11, XXREAL_0:2;
then A45: DataLoc (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)),0) <> intpos sp by ZFMISC_1:33;
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)),(Initialize t))))) . (intpos sp) by SCMPDS_5:47
.= t . (intpos sp) by A42, A45, SCMPDS_2:60 ;
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:5;
then A48: abs (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv) = n + cv by ZFMISC_1:33;
then pD <> abs (((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 ZFMISC_1:33;
A50: f . (0 + 1) = t . (DataLoc ((t . (intpos pD)),0)) by A20, A21
.= (Initialize t) . (DataLoc ((t . (intpos pD)),0)) by SCMPDS_5:40
.= (Initialize t) . (DataLoc (((Initialize t) . (intpos pD)),0)) by SCMPDS_5:40 ;
n + fr <> abs (((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 A39, ZFMISC_1:33;
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)),(Initialize t))))) . (DataLoc ((s . (intpos sp)),fr)) by SCMPDS_5:47
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (DataLoc ((s . (intpos sp)),fr)) by A6, A7, A43, SCMPDS_2:60
.= ((Initialize t) . (DataLoc ((s . (intpos sp)),fr))) + (f . 1) by A40, A41, A50, SCMPDS_2:61
.= (t . (DataLoc ((s . (intpos sp)),fr))) + (f . 1) by SCMPDS_5:40 ;
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:46
.= (f . 1) + (t . (DataLoc ((s . (intpos sp)),fr))) by A51, A52, SCMPDS_2:60 ;
n + cv <> sp by A1, NAT_1:11;
then abs (n + cv) <> sp by ABSVALUE:def 1;
then A54: DataLoc ((t . (intpos sp)),cv) <> intpos sp by A16, ZFMISC_1:33;
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:46
.= (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos pD) by A49, SCMPDS_2:60
.= (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))))) . (intpos pD) by SCMPDS_5:47
.= ((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pD)) + 1 by A43, SCMPDS_2:60
.= ((Initialize t) . (intpos pD)) + 1 by A6, A7, A40, A41, SCMPDS_2:61
.= (t . (intpos pD)) + 1 by SCMPDS_5:40 ;
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:31;
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:3;
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:40;
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:40;
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:40;
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:40;
A63: for k being Element of 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:16;
let i be Element of 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:8;
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:40;
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:5
.= intpos (m + (1 + i)) ;
then A66: abs (((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, ZFMISC_1:33;
then abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp)) + 0) <> abs (((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)),(Initialize 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, ZFMISC_1:33;
m <= m + (1 + i) by NAT_1:11;
then abs (((Initialize t) . (intpos sp)) + fr) <> abs (((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 (((Initialize 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, ZFMISC_1:33;
n + cv < m by A13, A18, XXREAL_0:2;
then abs (((IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),Q,t)) . (intpos pD)) + i) <> abs (((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, ZFMISC_1:33;
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:46
.= (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:60
.= (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize 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:47
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize 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:60
.= (Initialize 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:61
.= 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:40 ;
0 + 1 <= i + 1 by XREAL_1:8;
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, A59, A65 ;
:: thesis: verum
end;
abs (((Initialize t) . (intpos sp)) + fr) <> n + cv by A2, A41;
then A71: DataLoc (((Initialize t) . (intpos sp)),fr) <> intpos (n + cv) by ZFMISC_1:33;
abs (((Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize 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)),(Initialize t))) . (intpos pp)),0) <> intpos (n + cv) by ZFMISC_1:33;
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)),(Initialize t))))) . (intpos (n + cv)) by SCMPDS_5:47
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos (n + cv)) by A72, SCMPDS_2:60
.= (Initialize t) . (intpos (n + cv)) by A71, SCMPDS_2:61
.= t . (intpos (n + cv)) by SCMPDS_5:40
.= k + 1 by A16, A19, A20, SCMP_GCD:5 ;
abs (((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 ZFMISC_1:33;
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:46
.= s . (intpos sp) by A16, A46, A74, SCMPDS_2:60 ;
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:5;
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:46
.= ((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos (n + cv))) + (- 1) by A47, SCMPDS_2:60
.= len (Del (f,1)) by A20, A58, A73 ;
pp <> abs (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)) + cv) by A2, A4, A48, XREAL_1:8;
then A77: intpos pp <> DataLoc (((IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos sp)),cv) by ZFMISC_1:33;
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:46
.= (IExec (((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))),Q,t)) . (intpos pp) by A77, SCMPDS_2:60
.= (Exec ((AddTo ((intpos pp),0,1)),(Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))))) . (intpos pp) by SCMPDS_5:47
.= (Exec ((AddTo ((intpos sp),fr,(intpos pD),0)),(Initialize t))) . (intpos pp) by A3, A6, A43, SCMPDS_2:60
.= (Initialize t) . (intpos pp) by A3, A5, A7, A40, A41, SCMPDS_2:61
.= pD by A17, SCMPDS_5:40 ;
1 <= len f by A20, NAT_1:11;
then A79: 1 in dom f by FINSEQ_3:27;
n + cv <> pp by A2, A4, XREAL_1:8;
then abs (n + cv) <> pp by ABSVALUE:def 1;
then DataLoc ((s . (intpos sp)),cv) <> intpos pp by ZFMISC_1:33;
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,(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, Th68
.= (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 SCMPDS_5:48
.= (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:40
.= ((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:27 ;
:: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
now
let t be 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 Element of NAT st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ) holds
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 Element of NAT st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ) implies for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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 Element of NAT st k < len f holds
f . (k + 1) = t . (DataLoc ((t . (intpos pD)),k)) ; :: thesis: for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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)))
f = <*> NAT by A81;
then Sum f = 0 by RVSUM_1:102;
hence for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT 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, A81, Th66; :: thesis: verum
end;
then A82: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A82, 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