set P = ((IC S),0) --> (0,(halt S));
A: ((IC S),0) --> (0,(halt S)) = (Start-At (0,S)) +* (0 .--> (halt S)) by FUNCT_4:def 4;
then reconsider P = ((IC S),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, A; :: thesis: not P is NAT -defined
dom P = {(IC S),0} by FUNCT_4:65;
then A1: IC S in dom P by TARSKI:def 2;
not dom P c= NAT by A1, COMPOS_1:3;
hence not P is NAT -defined by RELAT_1:def 18; :: thesis: verum