let s be State of ; :: thesis: for I being Program of st I is_halting_on Initialize s holds
( ( for a being read-write Int-Location holds (IExec I,s) . a = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . f ) )
set A = NAT ;
let I be Program of ; :: thesis: ( I is_halting_on Initialize s implies ( ( for a being read-write Int-Location holds (IExec I,s) . a = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . f ) ) )
set s0 = Initialize s;
set s1 = (Initialize s) +* (I +* (Start-At (insloc 0 )));
assume I is_halting_on Initialize s ; :: thesis: ( ( for a being read-write Int-Location holds (IExec I,s) . a = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . f ) )
then A1: ProgramPart ((Initialize s) +* (I +* (Start-At (insloc 0 )))) halts_on (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA7B:def 8;

hereby :: thesis: for f being FinSeq-Location holds (IExec I,s) . f = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . f

let a be read-write Int-Location ; :: thesis: (IExec I,s) . a = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . a

now

assume A2: a in NAT ; :: thesis: contradiction
then reconsider a = a as Instruction-Location of SCM+FSA by AMI_1:def 4;
a in NAT by A2;
hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

then not a in (dom s) /\ NAT by XBOOLE_0:def 4;
then A3: not a in dom (s | NAT ) by RELAT_1:90;
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
hence (IExec I,s) . a = ((Result ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) +* (s | NAT )) . a by SCMFSA6B:def 1
.= (Result ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) . a by A3, FUNCT_4:12
.= (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . a by A1, AMI_1:122 ;
:: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec I,s) . f = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . f

now

assume A4: f in NAT ; :: thesis: contradiction
then reconsider f = f as Instruction-Location of SCM+FSA by AMI_1:def 4;
f in NAT by A4;
hence contradiction by SCMFSA_2:85; :: thesis: verum

end;

then not f in (dom s) /\ NAT by XBOOLE_0:def 4;
then A5: not f in dom (s | NAT ) by RELAT_1:90;
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At (insloc 0 ))) by SCMFSA8A:13;
hence (IExec I,s) . f = ((Result ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) +* (s | NAT )) . f by SCMFSA6B:def 1
.= (Result ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) . f by A5, FUNCT_4:12
.= (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . f by A1, AMI_1:122 ;
:: thesis: verum