let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s & not f in UsedInt*Loc I holds
(IExec I,s) . f = (Initialize s) . f
let f be FinSeq-Location ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s & not f in UsedInt*Loc I holds
(IExec I,s) . f = (Initialize s) . f
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on Initialize s & I is_halting_on Initialize s & not f in UsedInt*Loc I implies (IExec I,s) . f = (Initialize s) . f )
set a = f;
assume that
A1: I is_closed_on Initialize s and
A2: I is_halting_on Initialize s and
A3: not f in UsedInt*Loc I ; :: thesis: (IExec I,s) . f = (Initialize s) . f
set Is = Initialize s;
set sI = s +* (Initialized I);
A4: ( I +* (Start-At 0 ,SCM+FSA ) c= Initialized I & Initialized I c= s +* (Initialized I) ) by FUNCT_4:26, SCMFSA8C:19;
A5: ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) 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 0 ,SCM+FSA )) by SCMFSA8A:13;
then for m being Element of NAT st m < LifeSpan (s +* (Initialized I)) holds
IC (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m) in dom I by A1, SCMFSA7B:def 7;
then A8: (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . f = (s +* (Initialized I)) . f by A3, A4, SF_MASTR:71, XBOOLE_1:1;
DataPart (s +* (Initialized I)) = DataPart (Initialize s) by SCMFSA8B:5;
then A9: (s +* (Initialized I)) . f = (Initialize s) . f 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 (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) by A7, A5, AMI_1:122 ;
hence (IExec I,s) . f = (Initialize s) . f by A8, A9, SCMFSA6A:38; :: thesis: verum