reconsider il = il. (SCM R),0 as Instruction-Location of SCM R ;
set P = (IC (SCM R)),(il. (SCM R),0 ) --> il,(halt (SCM R));
(IC (SCM R)),(il. (SCM R),0 ) --> il,(halt (SCM R)) = (Start-At (il. (SCM R),0 )) +* ((il. (SCM R),0 ) .--> (halt (SCM R))) by FUNCT_4:def 4;
then reconsider P = (IC (SCM R)),(il. (SCM R),0 ) --> il,(halt (SCM R)) as FinPartState of (SCM R) ;
take P ; :: thesis: ( P is autonomic & not P is NAT -defined )
reconsider h = halt (SCM R) as Element of ObjectKind il by AMI_1:def 14;
ObjectKind (IC (SCM R)) = NAT by AMI_1:def 11;
then reconsider l = il as Element of ObjectKind (IC (SCM R)) by AMI_1:def 4;
(IC (SCM R)),il --> l,h is autonomic by AMI_1:67;
hence P is autonomic ; :: thesis: not P is NAT -defined

now

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

end;

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