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))))),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 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))))),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 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 0 -started 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;
X1: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t)) . (intpos pD) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (intpos pD) by SCMPDS_5:40;
X3: (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)) = (Initialize (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)) by SCMPDS_5:40;
X4: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t)) . (intpos pp) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (intpos pp) by SCMPDS_5:40;
X5: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t)) . (intpos sp) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (intpos sp) by SCMPDS_5:40;
A60: 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)))),t))) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),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)))),t))) . (DataLoc (((Initialize (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 (((Initialize (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) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (DataLoc (((Initialize (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;
X6: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t)) . (DataLoc (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (intpos pD)),i)) = (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (DataLoc (((Initialize (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;
DataLoc (((Initialize (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, X1, 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 X1, 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 (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (intpos pD)),i) by X1, 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 (((Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (intpos pD)),i) by X1, 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 (((Initialize (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 X1, ZFMISC_1:33;
A66: (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t)) . (DataLoc (((Initialize (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 (((Initialize (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 (((Initialize (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 (((Initialize (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 (((Initialize (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 (((Initialize (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 (((Initialize (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
.= (Initialize (IExec ((((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))) ';' (AddTo ((intpos sp),cv,(- 1)))),t))) . (DataLoc (((Initialize (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, X1, X6 ;
:: 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
.= (IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),(Initialize (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 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)))),t))) . (DataLoc ((s . (intpos sp)),fr))) by A15, A20, A71, A59, A72, A74, A57, A60, X1, X3, X4, X5
.= (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 SCMPDS_5:40
.= ((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