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