let s be State of ; for b being Int-Location
for I being Program of st I is_closed_on Initialize s & I is_halting_on Initialize s & not b in UsedIntLoc I holds
(IExec I,s) . b = (Initialize s) . b
let b be Int-Location ; for I being Program of st I is_closed_on Initialize s & I is_halting_on Initialize s & not b in UsedIntLoc I holds
(IExec I,s) . b = (Initialize s) . b
let I be Program of ; ( I is_closed_on Initialize s & I is_halting_on Initialize s & not b in UsedIntLoc I implies (IExec I,s) . b = (Initialize s) . b )
set a = b;
assume that
A1:
I is_closed_on Initialize s
and
A2:
I is_halting_on Initialize s
and
A3:
not b in UsedIntLoc I
; (IExec I,s) . b = (Initialize s) . b
set Is = Initialize s;
set sI = s +* (Initialized I);
A4:
( I +* (Start-At (insloc 0 )) c= Initialized I & Initialized I c= s +* (Initialized I) )
by FUNCT_4:26, SCMFSA8C:19;
A5:
ProgramPart ((Initialize s) +* (I +* (Start-At (insloc 0 )))) halts_on (Initialize s) +* (I +* (Start-At (insloc 0 )))
by A2, SCMFSA7B:def 8;
NAT misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A6:
dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations
by SCMFSA8A:3;
A7:
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 )))
by SCMFSA8A:13;
then
for m being Element of NAT st m < LifeSpan (s +* (Initialized I)) holds
IC (Computation (s +* (Initialized I)),m) in dom I
by A1, SCMFSA7B:def 7;
then A8:
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . b = (s +* (Initialized I)) . b
by A3, A4, SF_MASTR:69, XBOOLE_1:1;
DataPart (s +* (Initialized I)) = DataPart (Initialize s)
by SCMFSA8B:5;
then A9:
(s +* (Initialized I)) . b = (Initialize s) . b
by SCMFSA6A:38;
DataPart (IExec I,s) =
DataPart ((Result (s +* (Initialized I))) +* (s | NAT ))
by SCMFSA6B:def 1
.=
DataPart (Result (s +* (Initialized I)))
by A6, FUNCT_4:94, SCMFSA_2:127
.=
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))
by A7, A5, AMI_1:122
;
hence
(IExec I,s) . b = (Initialize s) . b
by A8, A9, SCMFSA6A:38; verum