let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being 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 Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
let s be 0 -started State of SCMPDS; for sp, cv, result, pp, pD being 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 Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,result,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),result)) = Sum f
let sp, cv, fr, pp, pD be 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 Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) holds
(IExec ((sum (sp,cv,fr,pp,pD)),P,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 Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k)) ) implies (IExec ((sum (sp,cv,fr,pp,pD)),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 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 Nat st k < len f holds
f . (k + 1) = s . (DataLoc ((s . (intpos pD)),k))
; (IExec ((sum (sp,cv,fr,pp,pD)),P,s)) . (DataLoc ((s . (intpos sp)),fr)) = Sum f
reconsider n = s . (intpos sp) as Element of NAT by A1, INT_1:3;
A8:
intpos pD <> intpos pp
by A4, XTUPLE_0:1;
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)),P,s);
set P2 = P;
set s0 = s;
set s1 = Exec ((((intpos sp),fr) := 0),s);
set a = DataLoc ((s . (intpos sp)),fr);
set a1 = DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr);
A9:
DataLoc ((s . (intpos sp)),fr) = intpos (n + fr)
by SCMP_GCD:1;
then A10:
|.((s . (intpos sp)) + fr).| = n + fr
by XTUPLE_0:1;
then
|.((s . (intpos sp)) + fr).| <> sp
by A1, NAT_1:12;
then A11:
DataLoc ((s . (intpos sp)),fr) <> intpos sp
by XTUPLE_0:1;
A12:
DataLoc ((s . (intpos sp)),fr) <> intpos pD
by A3, A4, A9, XTUPLE_0:1;
A13: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD) =
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos pD)
by SCMPDS_5:42
.=
(Exec ((((intpos sp),fr) := 0),s)) . (intpos pD)
by A8, SCMPDS_2:45
.=
s . (intpos pD)
by A12, SCMPDS_2:46
;
n <= n + fr
by NAT_1:12;
then
sp <> pp
by A1, A3, XXREAL_0:2;
then A14:
intpos sp <> intpos pp
by XTUPLE_0:1;
A15:
intpos (n + fr) <> intpos pp
by A3, XTUPLE_0:1;
A16: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp) =
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos sp)
by SCMPDS_5:42
.=
(Exec ((((intpos sp),fr) := 0),s)) . (intpos sp)
by A14, SCMPDS_2:45
.=
n
by A11, SCMPDS_2:46
;
then A17: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr)) =
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos (n + fr))
by SCMP_GCD:1
.=
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos (n + fr))
by SCMPDS_5:42
.=
(Exec ((((intpos sp),fr) := 0),s)) . (intpos (n + fr))
by A15, SCMPDS_2:45
.=
0
by A9, SCMPDS_2:46
;
A18:
n + fr < pD
by A3, A4, XXREAL_0:2;
A19:
now for k being Nat st k < len f holds
(Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) = f . (k + 1)reconsider m =
s . (intpos pD) as
Element of
NAT by A5, INT_1:3;
let k be
Nat;
( k < len f implies (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) = f . (k + 1) )assume A20:
k < len f
;
(Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,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 XTUPLE_0:1;
m <= m + k
by NAT_1:11;
then
|.((s . (intpos sp)) + fr).| <> m + k
by A5, A10, A18, XXREAL_0:2;
then A22:
DataLoc (
(s . (intpos sp)),
fr)
<> intpos (m + k)
by XTUPLE_0:1;
thus (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k)) =
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD)),k))
by SCMPDS_5:15
.=
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos (m + k))
by A13, SCMP_GCD:1
.=
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos (m + k))
by SCMPDS_5:42
.=
(Exec ((((intpos sp),fr) := 0),s)) . (intpos (m + k))
by A21, SCMPDS_2:45
.=
s . (intpos (m + k))
by A22, SCMPDS_2:46
.=
s . (DataLoc ((s . (intpos pD)),k))
by SCMP_GCD:1
.=
f . (k + 1)
by A7, A20
;
verum end;
|.((s . (intpos sp)) + fr).| <> n + cv
by A2, A10;
then A23:
DataLoc ((s . (intpos sp)),fr) <> intpos (n + cv)
by XTUPLE_0:1;
n + cv <> pp
by A2, A3, XREAL_1:6;
then A24:
intpos (n + cv) <> intpos pp
by XTUPLE_0:1;
A25:
(((intpos sp),fr) := 0) ';' ((intpos pp) := pD) is_halting_on s,P
by SCMPDS_6:21;
A26:
(((intpos sp),fr) := 0) ';' ((intpos pp) := pD) is_closed_on s,P
by SCMPDS_6:20;
A27:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pp) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (intpos pp)
by SCMPDS_5:15;
A28:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (intpos sp)
by SCMPDS_5:15;
A29:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pD) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (intpos pD)
by SCMPDS_5:15;
A30: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos pp) =
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos pp)
by SCMPDS_5:42
.=
pD
by SCMPDS_2:45
;
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)),P,s)),P
by A1, A2, A3, A4, A5, A16, A13, Th51, A27, A28, A29;
then A31:
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)),P,s),P
by SCMPDS_6:126;
A32: (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),cv)) =
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos (n + cv))
by A16, SCMP_GCD:1
.=
(Exec (((intpos pp) := pD),(Exec ((((intpos sp),fr) := 0),s)))) . (intpos (n + cv))
by SCMPDS_5:42
.=
(Exec ((((intpos sp),fr) := 0),s)) . (intpos (n + cv))
by A24, SCMPDS_2:45
.=
s . (intpos (n + cv))
by A23, SCMPDS_2:46
.=
len f
by A6, SCMP_GCD:1
;
A33:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr)) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr))
by SCMPDS_5:15;
A34:
(IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),cv)) = (Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),cv))
by SCMPDS_5:15;
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)),P,s)),P
by A1, A2, A3, A4, A5, A16, A30, A13, Th51, A27, A28, A29;
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)),P,s),P
by SCMPDS_6:125;
hence (IExec ((sum (sp,cv,fr,pp,pD)),P,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))))),P,(Initialize (IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s))))) . (DataLoc (((IExec (((((intpos sp),fr) := 0) ';' ((intpos pp) := pD)),P,s)) . (intpos sp)),fr))
by A16, A26, A25, A31, Th28
.=
Sum f
by A1, A2, A3, A4, A5, A16, A30, A13, A17, A32, A19, Th52, A27, A28, A29, A33, A34
;
verum