set P = (IC SCM+FSA ),(insloc 0 ) --> (insloc 0 ),(halt SCM+FSA );
(IC SCM+FSA ),(insloc 0 ) --> (insloc 0 ),(halt SCM+FSA ) = (Start-At (insloc 0 )) +* ((insloc 0 ) .--> (halt SCM+FSA )) by FUNCT_4:def 4;
then reconsider P = (IC SCM+FSA ),(insloc 0 ) --> (insloc 0 ),(halt SCM+FSA ) as FinPartState of ;
take P ; :: thesis: ( P is autonomic & not P is NAT -defined )
( ObjectKind (insloc 0 ) = the Instructions of SCM+FSA & ObjectKind (IC SCM+FSA ) = NAT ) by AMI_1:def 11, AMI_1:def 14;
hence P is autonomic by AMI_1:67; :: thesis: not P is NAT -defined

now

assume A1: dom P c= NAT ; :: thesis: contradiction
A2: dom P = {(IC SCM+FSA ),(insloc 0 )} by FUNCT_4:65;
then IC SCM+FSA in dom P by TARSKI:def 2;
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by A1, AMI_1:def 4;
l in dom P by A2, TARSKI:def 2;
hence contradiction by AMI_1:48; :: thesis: verum

end;

hence not P is NAT -defined by RELAT_1:def 18; :: thesis: verum