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
A1: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
s +* (Initialized I) is halting by Th5, FUNCT_4:26;
then consider n being Element of NAT such that
A2: ( Result (s +* (Initialized I)) = Computation (s +* (Initialized I)),n & CurInstr (Result (s +* (Initialized I))) = halt SCM+FSA ) by AMI_1:def 22;
not intloc 0 in NAT

proof

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

end;

then A4: not intloc 0 in dom (s | NAT ) by RELAT_1:86;
thus (IExec I,s) . (intloc 0 ) = ((Result (s +* (Initialized I))) +* (s | NAT )) . (intloc 0 ) by SCMFSA6B:def 1
.= (Result (s +* (Initialized I))) . (intloc 0 ) by A4, FUNCT_4:12
.= 1 by A1, A2, Def3 ; :: thesis: verum