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

hereby :: thesis: verum

let a be 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 a in NAT ; :: thesis: contradiction
then reconsider a = a as Instruction-Location of SCM+FSA by AMI_1:def 4;
a = a ;
hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

then not a in (dom s) /\ NAT by XBOOLE_0:def 4;
then A2: ( a in dom (Result ((Initialize s) +* (I +* (Start-At (insloc 0 ))))) & not a in dom (s | NAT ) ) by RELAT_1:90, SCMFSA_2:66;
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 A2, 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;