let s be State of SCM+FSA ; :: thesis: for I being parahalting keeping_0 Program of SCM+FSA holds (IExec I,s) . (intloc 0 ) = 1
let I be parahalting keeping_0 Program of SCM+FSA ; :: thesis: (IExec I,s) . (intloc 0 ) = 1
s +* (Initialized I) is halting by Th19, FUNCT_4:26;
then consider n being Element of NAT such that
A1: ( Result (s +* (Initialized I)) = Computation (s +* (Initialized I)),n & CurInstr (Result (s +* (Initialized I))) = halt SCM+FSA ) by AMI_1:def 22;
A2: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
A3: I +* (Start-At (insloc 0 )) c= s +* (Initialized I) by Th8, FUNCT_4:26;
not intloc 0 in NAT

proof

assume A4: intloc 0 in NAT ; :: thesis: contradiction
intloc 0 in Int-Locations by SCMFSA_2:9;
hence contradiction by A4, SCMFSA_2:13, XBOOLE_0:3; :: thesis: verum

end;

then not intloc 0 in dom (s | NAT ) by RELAT_1:86;
hence (IExec I,s) . (intloc 0 ) = (Result (s +* (Initialized I))) . (intloc 0 ) by FUNCT_4:12
.= (s +* (Initialized I)) . (intloc 0 ) by A1, A3, Def4
.= (Initialized I) . (intloc 0 ) by A2, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: verum