reconsider il = 2 as Element of NAT ;
set P = (IC SCMPDS ),2 --> 2,(halt SCMPDS );
(IC SCMPDS ),2 --> 2,(halt SCMPDS ) = (Start-At il,SCMPDS ) +* (il .--> (halt SCMPDS )) by FUNCT_4:def 4;
then reconsider P = (IC SCMPDS ),2 --> 2,(halt SCMPDS ) as FinPartState of SCMPDS ;
take P ; :: thesis: ( P is autonomic & not P is NAT -defined )
thus P is autonomic by AMI_1:67; :: thesis: not P is NAT -defined
dom P = {(IC SCMPDS ),2} by FUNCT_4:65;
then A1: IC SCMPDS in dom P by TARSKI:def 2;
not dom P c= NAT by A1, AMI_1:48;
hence not P is NAT -defined by RELAT_1:def 18; :: thesis: verum