let s be 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 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 ; 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 ; ( 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))
; (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 = Initialize s;
set s1 = Exec ((((intpos sp),fr) := 0),(Initialize 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 (((Initialize s) . (intpos sp)),fr) =
DataLoc (n,fr)
by SCMPDS_5:40
.=
intpos (n + fr)
by SCMP_GCD:5
;
then A10:
abs (((Initialize s) . (intpos sp)) + fr) = n + fr
by ZFMISC_1:33;
then
abs (((Initialize s) . (intpos sp)) + fr) <> sp
by A1, NAT_1:12;
then A11:
DataLoc (((Initialize s) . (intpos sp)),fr) <> intpos sp
by ZFMISC_1:33;
A12:
DataLoc (((Initialize 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),(Initialize s))))) . (intpos pD)
by SCMPDS_5:47
.=
(Exec ((((intpos sp),fr) := 0),(Initialize s))) . (intpos pD)
by A8, SCMPDS_2:57
.=
(Initialize 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),(Initialize s))))) . (intpos sp)
by SCMPDS_5:47
.=
(Exec ((((intpos sp),fr) := 0),(Initialize s))) . (intpos sp)
by A14, SCMPDS_2:57
.=
(Initialize 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),(Initialize s))))) . (intpos (n + fr))
by SCMPDS_5:47
.=
(Exec ((((intpos sp),fr) := 0),(Initialize 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 ;
( k < len f implies (Initialize (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
;
(Initialize (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 (((Initialize s) . (intpos sp)) + fr) <> m + k
by A5, A10, A18, XXREAL_0:2;
then A22:
DataLoc (
((Initialize s) . (intpos sp)),
fr)
<> intpos (m + k)
by ZFMISC_1:33;
thus (Initialize (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)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos pD)),k))
by SCMPDS_5:40
.=
(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),(Initialize s))))) . (intpos (m + k))
by SCMPDS_5:47
.=
(Exec ((((intpos sp),fr) := 0),(Initialize s))) . (intpos (m + k))
by A21, SCMPDS_2:57
.=
(Initialize 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
;
verum end;
abs (((Initialize s) . (intpos sp)) + fr) <> n + cv
by A2, A10;
then A23:
DataLoc (((Initialize 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;
X1:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos pp) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))) . (intpos pp)
by SCMPDS_5:40;
X2:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos sp) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))) . (intpos sp)
by SCMPDS_5:40;
X3:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos pD) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))) . (intpos pD)
by SCMPDS_5:40;
A27: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos pp) =
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),(Initialize s))))) . (intpos pp)
by SCMPDS_5:47
.=
pD
by SCMPDS_2:57
;
then
for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))
by A1, A2, A3, A4, A5, A16, A13, Th72, X1, X2, X3;
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 SCMPDS_6:140;
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),(Initialize s))))) . (intpos (n + cv))
by SCMPDS_5:47
.=
(Exec ((((intpos sp),fr) := 0),(Initialize s))) . (intpos (n + cv))
by A24, SCMPDS_2:57
.=
(Initialize s) . (intpos (n + cv))
by A23, SCMPDS_2:58
.=
s . (intpos (n + cv))
by SCMPDS_5:40
.=
len f
by A6, SCMP_GCD:5
;
X4:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos sp)),fr)) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos sp)),fr))
by SCMPDS_5:40;
X5:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos sp)),cv)) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos sp)),cv))
by SCMPDS_5:40;
for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))
by A1, A2, A3, A4, A5, A16, A27, A13, Th72, X1, X2, X3;
then
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 SCMPDS_6:139;
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
.=
(IExec ((for-down ((intpos sp),cv,1,((AddTo ((intpos sp),fr,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1))))),(Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s))))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),s)) . (intpos sp)),fr))
by SCMPDS_5:48
.=
Sum f
by A1, A2, A3, A4, A5, A16, A27, A13, A17, A29, A19, Th73, X1, X2, X3, X4, X5
;
verum