let s be State of SCM+FSA ; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec I,s) . (intloc 0 ) = 1
let I be InitHalting keepInt0_1 Program of SCM+FSA ; :: thesis: (IExec I,s) . (intloc 0 ) = 1
not intloc 0 in NAT

proof

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

end;

then A2: not intloc 0 in dom (s | NAT ) by RELAT_1:86;
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by Th5, FUNCT_4:26;
then A3: ( Initialized I c= s +* (Initialized I) & 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 AMI_1:def 22, FUNCT_4:26;
thus (IExec I,s) . (intloc 0 ) = ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT )) . (intloc 0 ) by SCMFSA6B:def 1
.= (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) . (intloc 0 ) by A2, FUNCT_4:12
.= 1 by A3, Def3 ; :: thesis: verum