let s be 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))),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))),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))),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))),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 t being 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))),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 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 = 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))),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 = 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))),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))),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 State 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) . (intpos sp) = u . (intpos sp) & (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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 & (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_halting_on 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) . 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) . (intpos sp) = u . (intpos sp) & (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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 & (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_halting_on 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) . 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) . (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) . (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 & (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_halting_on 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) . 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) . (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 & (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_halting_on 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) . y = u . y ) )
thus ( (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_closed_on u & (AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1) is_halting_on 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) . y = u . y
A37: (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 ),(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) . 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) . 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) . b1 = u . b1
hence (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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) . b1 = u . b1
hence (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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))),t;
set g = Del f,1;
set It = IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t;
A41: DataLoc ((Initialize t) . (intpos sp)),fr = DataLoc n,fr by A16, SCMPDS_5:40
.= intpos (n + fr) by SCMP_GCD:5 ;
then A42: abs (((Initialize t) . (intpos sp)) + fr) = n + fr by ZFMISC_1:33;
then A43: (Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos sp) = (Initialize t) . (intpos sp) by A1, A7, A41, 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, A41, A42, SCMPDS_2:61
.= t . (intpos pp) by SCMPDS_5:40 ;
then A44: DataLoc ((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)),0 = intpos (pD + 0 ) by A17, SCMP_GCD:5;
then A45: 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 A46: DataLoc ((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)),0 <> intpos sp by ZFMISC_1:33;
A47: (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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 A43, A46, SCMPDS_2:60 ;
then A48: DataLoc ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)),cv = intpos (n + cv) by A16, SCMP_GCD:5;
then A49: abs (((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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)),t) . (intpos sp)) + cv) by A4, A5, A12, XXREAL_0:2;
then A50: intpos pD <> DataLoc ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)),cv by ZFMISC_1:33;
A51: 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)),t) . (intpos sp)) + cv) by A2, A49;
then A52: DataLoc (s . (intpos sp)),fr <> DataLoc ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)),cv by A39, ZFMISC_1:33;
A53: (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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, A44, SCMPDS_2:60
.= ((Initialize t) . (DataLoc (s . (intpos sp)),fr)) + (f . 1) by A41, A42, A51, SCMPDS_2:61
.= (t . (DataLoc (s . (intpos sp)),fr)) + (f . 1) by SCMPDS_5:40 ;
A54: (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),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)),t)) . (DataLoc (s . (intpos sp)),fr) by SCMPDS_5:46
.= (f . 1) + (t . (DataLoc (s . (intpos sp)),fr)) by A52, A53, SCMPDS_2:60 ;
n + cv <> sp by A1, NAT_1:11;
then abs (n + cv) <> sp by ABSVALUE:def 1;
then A55: DataLoc (t . (intpos sp)),cv <> intpos sp by A16, ZFMISC_1:33;
A56: (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD) = (Exec (AddTo (intpos sp),cv,(- 1)),(IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t)) . (intpos pD) by SCMPDS_5:46
.= (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos pD) by A50, 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 A44, SCMPDS_2:60
.= ((Initialize t) . (intpos pD)) + 1 by A6, A7, A41, A42, 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))),t) . (intpos pD) by XREAL_1:31;
then A57: pD < (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),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 A58: 1 in dom f by A20, FINSEQ_1:def 3;
then A59: (len (Del f,1)) + 1 = len f by WSIERP_1:def 1;
A60: now
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) = (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) )
set SD = DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i;
assume i < len (Del f,1) ; :: thesis: (Del f,1) . (i + 1) = (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i)
then A61: i + 1 < (len (Del f,1)) + 1 by XREAL_1:8;
DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i = intpos ((m + 1) + i) by A56, SCMP_GCD:5
.= intpos (m + (1 + i)) ;
then A62: abs (((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)) + i) = m + (1 + i) by 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))),t) . (intpos pD)) + i) by A18, A45, NAT_1:11;
then A63: DataLoc ((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)),0 <> DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i by 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))),t) . (intpos pD)) + i) by A10, A18, A42, A62, XXREAL_0:2;
then A64: DataLoc ((Initialize t) . (intpos sp)),fr <> DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i by 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))),t) . (intpos pD)) + i) <> abs (((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)) + cv) by A49, A62, NAT_1:11;
then A65: DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i <> DataLoc ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)),cv by ZFMISC_1:33;
A66: (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) = (Exec (AddTo (intpos sp),cv,(- 1)),(IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t)) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) by SCMPDS_5:46
.= (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) by A65, SCMPDS_2:60
.= (Exec (AddTo (intpos pp),0 ,1),(Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t))) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) by SCMPDS_5:47
.= (Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) by A63, SCMPDS_2:60
.= (Initialize t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) by A64, SCMPDS_2:61
.= t . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),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 A58, WSIERP_1:def 1
.= t . (DataLoc (t . (intpos pD)),(i + 1)) by A21, A59, A61
.= (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pD)),i) by A62, A66 ;
:: thesis: verum
end;
abs (((Initialize t) . (intpos sp)) + fr) <> n + cv by A2, A42;
then A67: 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, A45, XXREAL_0:2;
then A68: DataLoc ((Exec (AddTo (intpos sp),fr,(intpos pD),0 ),(Initialize t)) . (intpos pp)),0 <> intpos (n + cv) by ZFMISC_1:33;
A69: (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),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 A68, SCMPDS_2:60
.= (Initialize t) . (intpos (n + cv)) by A67, 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)),t) . (intpos sp)) + cv) <> sp by A1, A49, NAT_1:11;
then A70: DataLoc ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)),cv <> intpos sp by ZFMISC_1:33;
A71: (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos sp) = (Exec (AddTo (intpos sp),cv,(- 1)),(IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t)) . (intpos sp) by SCMPDS_5:46
.= s . (intpos sp) by A16, A47, A70, SCMPDS_2:60 ;
then DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos sp)),cv = intpos (n + cv) by SCMP_GCD:5;
then A72: (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (DataLoc ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos sp)),cv) = (Exec (AddTo (intpos sp),cv,(- 1)),(IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t)) . (intpos (n + cv)) by SCMPDS_5:46
.= ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos (n + cv))) + (- 1) by A48, SCMPDS_2:60
.= len (Del f,1) by A20, A59, A69 ;
pp <> abs (((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)) + cv) by A2, A4, A49, XREAL_1:8;
then A73: intpos pp <> DataLoc ((IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos sp)),cv by ZFMISC_1:33;
A74: (IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (intpos pp) = (Exec (AddTo (intpos sp),cv,(- 1)),(IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t)) . (intpos pp) by SCMPDS_5:46
.= (IExec ((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)),t) . (intpos pp) by A73, 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, A44, SCMPDS_2:60
.= (Initialize t) . (intpos pp) by A3, A5, A7, A41, A42, SCMPDS_2:61
.= pD by A17, SCMPDS_5:40 ;
1 <= len f by A20, NAT_1:11;
then A75: 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, A55, TARSKI:def 2;
hence (IExec (for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1))),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))),(IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t)) . (DataLoc (s . (intpos sp)),fr) by A19, A20, A55, A23, Th68
.= (Sum (Del f,1)) + ((IExec (((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) ';' (AddTo (intpos sp),cv,(- 1))),t) . (DataLoc (s . (intpos sp)),fr)) by A15, A20, A71, A59, A72, A74, A57, A60
.= ((Sum (Del f,1)) + (f . 1)) + (t . (DataLoc (s . (intpos sp)),fr)) by A54
.= (Sum f) + (t . (DataLoc (s . (intpos sp)),fr)) by A75, 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
(IExec (for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1))),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 (IExec (for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1))),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
A76: len f = t . (DataLoc (t . (intpos sp)),cv) and
A77: 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: (IExec (for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1))),t) . (DataLoc (s . (intpos sp)),fr) = (Sum f) + (t . (DataLoc (s . (intpos sp)),fr))
f = <*> NAT by A77;
then Sum f = 0 by RVSUM_1:102;
hence (IExec (for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1))),t) . (DataLoc (s . (intpos sp)),fr) = (Sum f) + (t . (DataLoc (s . (intpos sp)),fr)) by A76, A77, Th66; :: thesis: verum
end;
then A78: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A78, A14);
 hence (IExec (for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1))),s) . (DataLoc (s . (intpos sp)),fr) = (Sum f) + 0 by A3, A6, A7, A8, A9
.= Sum f ;
:: thesis: verum