reconsider il = 2 as Instruction-Location of SCMPDS by AMI_1:def 4;
set P = (IC SCMPDS ),il --> il,(halt SCMPDS );
(IC SCMPDS ),il --> il,(halt SCMPDS ) = (Start-At il) +* (il .--> (halt SCMPDS )) by FUNCT_4:def 4;
then reconsider P = (IC SCMPDS ),il --> il,(halt SCMPDS ) as FinPartState of ;
take P ; :: thesis: ( P is autonomic & not P is NAT -defined )
( ObjectKind il = the Instructions of SCMPDS & ObjectKind (IC SCMPDS ) = 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

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

end;

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