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 sp)) + result < pp & pp < pD & pD < s . (intpos pD) & 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 (sum sp,cv,result,pp,pD),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 sp)) + fr < pp & pp < pD & pD < s . (intpos pD) & 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 (sum sp,cv,fr,pp,pD),s) . (DataLoc (s . (intpos sp)),fr) = Sum f
let f be FinSequence of NAT ; :: thesis: ( s . (intpos sp) > sp & cv < fr & (s . (intpos sp)) + fr < pp & pp < pD & pD < s . (intpos pD) & 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 (sum sp,cv,fr,pp,pD),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 sp)) + fr < pp
and
A4:
pp < pD
and
A5:
pD < s . (intpos pD)
and
A6:
len f = s . (DataLoc (s . (intpos sp)),cv)
and
A7:
for k being Element of NAT st k < len f holds
f . (k + 1) = s . (DataLoc (s . (intpos pD)),k)
; :: thesis: (IExec (sum sp,cv,fr,pp,pD),s) . (DataLoc (s . (intpos sp)),fr) = Sum f
reconsider n = s . (intpos sp) as Element of NAT by A1, INT_1:16;
A8:
intpos pD <> intpos pp
by A4, ZFMISC_1:33;
set i0 = (intpos sp),fr := 0 ;
set i1 = (intpos pp) := pD;
set Hi = ((intpos sp),fr := 0 ) ';' ((intpos pp) := pD);
set i2 = AddTo (intpos sp),fr,(intpos pD),0 ;
set i3 = AddTo (intpos pp),0 ,1;
set FD = for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1));
set s2 = IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s;
set s0 = Initialized s;
set s1 = Exec ((intpos sp),fr := 0 ),(Initialized s);
set a = DataLoc (s . (intpos sp)),fr;
set a1 = DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos sp)),fr;
A9: DataLoc ((Initialized s) . (intpos sp)),fr =
DataLoc n,fr
by SCMPDS_5:40
.=
intpos (n + fr)
by SCMP_GCD:5
;
then A10:
abs (((Initialized s) . (intpos sp)) + fr) = n + fr
by ZFMISC_1:33;
then
abs (((Initialized s) . (intpos sp)) + fr) <> sp
by A1, NAT_1:12;
then A11:
DataLoc ((Initialized s) . (intpos sp)),fr <> intpos sp
by ZFMISC_1:33;
A12:
DataLoc ((Initialized s) . (intpos sp)),fr <> intpos pD
by A3, A4, A9, ZFMISC_1:33;
A13: (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos pD) =
(Exec ((intpos pp) := pD),(Exec ((intpos sp),fr := 0 ),(Initialized s))) . (intpos pD)
by SCMPDS_5:47
.=
(Exec ((intpos sp),fr := 0 ),(Initialized s)) . (intpos pD)
by A8, SCMPDS_2:57
.=
(Initialized s) . (intpos pD)
by A12, SCMPDS_2:58
.=
s . (intpos pD)
by SCMPDS_5:40
;
n <= n + fr
by NAT_1:12;
then
sp <> pp
by A1, A3, XXREAL_0:2;
then A14:
intpos sp <> intpos pp
by ZFMISC_1:33;
A15:
intpos (n + fr) <> intpos pp
by A3, ZFMISC_1:33;
A16: (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos sp) =
(Exec ((intpos pp) := pD),(Exec ((intpos sp),fr := 0 ),(Initialized s))) . (intpos sp)
by SCMPDS_5:47
.=
(Exec ((intpos sp),fr := 0 ),(Initialized s)) . (intpos sp)
by A14, SCMPDS_2:57
.=
(Initialized s) . (intpos sp)
by A11, SCMPDS_2:58
.=
n
by SCMPDS_5:40
;
then A17: (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos sp)),fr) =
(IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos (n + fr))
by SCMP_GCD:5
.=
(Exec ((intpos pp) := pD),(Exec ((intpos sp),fr := 0 ),(Initialized s))) . (intpos (n + fr))
by SCMPDS_5:47
.=
(Exec ((intpos sp),fr := 0 ),(Initialized s)) . (intpos (n + fr))
by A15, SCMPDS_2:57
.=
0
by A9, SCMPDS_2:58
;
A18:
n + fr < pD
by A3, A4, XXREAL_0:2;
A19:
now reconsider m =
s . (intpos pD) as
Element of
NAT by A5, INT_1:16;
let k be
Element of
NAT ;
:: thesis: ( k < len f implies (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos pD)),k) = f . (k + 1) )assume A20:
k < len f
;
:: thesis: (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos pD)),k) = f . (k + 1)
pp < m
by A4, A5, XXREAL_0:2;
then
m + k <> pp
by NAT_1:11;
then A21:
intpos (m + k) <> intpos pp
by ZFMISC_1:33;
m <= m + k
by NAT_1:11;
then
abs (((Initialized s) . (intpos sp)) + fr) <> m + k
by A5, A10, A18, XXREAL_0:2;
then A22:
DataLoc ((Initialized s) . (intpos sp)),
fr <> intpos (m + k)
by ZFMISC_1:33;
thus (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos pD)),k) =
(IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos (m + k))
by A13, SCMP_GCD:5
.=
(Exec ((intpos pp) := pD),(Exec ((intpos sp),fr := 0 ),(Initialized s))) . (intpos (m + k))
by SCMPDS_5:47
.=
(Exec ((intpos sp),fr := 0 ),(Initialized s)) . (intpos (m + k))
by A21, SCMPDS_2:57
.=
(Initialized s) . (intpos (m + k))
by A22, SCMPDS_2:58
.=
s . (intpos (m + k))
by SCMPDS_5:40
.=
s . (DataLoc (s . (intpos pD)),k)
by SCMP_GCD:5
.=
f . (k + 1)
by A7, A20
;
:: thesis: verum end;
abs (((Initialized s) . (intpos sp)) + fr) <> n + cv
by A2, A10;
then A23:
DataLoc ((Initialized s) . (intpos sp)),fr <> intpos (n + cv)
by ZFMISC_1:33;
n + cv <> pp
by A2, A3, XREAL_1:8;
then A24:
intpos (n + cv) <> intpos pp
by ZFMISC_1:33;
A25:
((intpos sp),fr := 0 ) ';' ((intpos pp) := pD) is_halting_on s
by SCMPDS_6:35;
A26:
((intpos sp),fr := 0 ) ';' ((intpos pp) := pD) is_closed_on s
by SCMPDS_6:34;
A27: (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos pp) =
(Exec ((intpos pp) := pD),(Exec ((intpos sp),fr := 0 ),(Initialized s))) . (intpos pp)
by SCMPDS_5:47
.=
pD
by SCMPDS_2:57
;
then A28:
for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) is_halting_on IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s
by A1, A2, A3, A4, A5, A16, A13, Th72;
A29: (IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos sp)),cv) =
(IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos (n + cv))
by A16, SCMP_GCD:5
.=
(Exec ((intpos pp) := pD),(Exec ((intpos sp),fr := 0 ),(Initialized s))) . (intpos (n + cv))
by SCMPDS_5:47
.=
(Exec ((intpos sp),fr := 0 ),(Initialized s)) . (intpos (n + cv))
by A24, SCMPDS_2:57
.=
(Initialized s) . (intpos (n + cv))
by A23, SCMPDS_2:58
.=
s . (intpos (n + cv))
by SCMPDS_5:40
.=
len f
by A6, SCMP_GCD:5
;
for-down (intpos sp),cv,1,((AddTo (intpos sp),fr,(intpos pD),0 ) ';' (AddTo (intpos pp),0 ,1)) is_closed_on IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s
by A1, A2, A3, A4, A5, A16, A27, A13, Th72;
hence (IExec (sum sp,cv,fr,pp,pD),s) . (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 (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s)) . (DataLoc ((IExec (((intpos sp),fr := 0 ) ';' ((intpos pp) := pD)),s) . (intpos sp)),fr)
by A16, A26, A25, A28, Th49
.=
Sum f
by A1, A2, A3, A4, A5, A16, A27, A13, A17, A29, A19, Th73
;
:: thesis: verum