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
A1: intloc 0 in dom (Initialized I) by SCMFSA6A:45;
A2: I +* (Start-At (0,SCM+FSA)) c= s +* (Initialized I) by Th8, FUNCT_4:26;
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by Th19, FUNCT_4:26;
then A3: ex n being Element of NAT st
( Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),n) & CurInstr ((ProgramPart (s +* (Initialized I))),(Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))) = halt SCM+FSA ) by EXTPRO_1:def 8;
not intloc 0 in NAT

proof

A4: intloc 0 in Int-Locations by SCMFSA_2:9;
assume intloc 0 in NAT ; :: thesis: contradiction
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 ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) . (intloc 0) by FUNCT_4:12
.= (s +* (Initialized I)) . (intloc 0) by A3, A2, Def4
.= (Initialized I) . (intloc 0) by A1, FUNCT_4:14
.= 1 by SCMFSA6A:46 ;
:: thesis: verum