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 AMI_1:def 22;
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