%==========================================================================
%
%       Number of labeled trees on n nodes:  n^(n-2).
%       Is enumerated by EIS A000272 (1,1,3,16,125,1296,16807,262144,...)
%       Number of spanning trees in complete graph K_n on n labeled nodes.
%       Number of transitive subtree acyclic digraphs on n-1 vertices.
%       Moral transitive directed acyclic graphs?
%
%       Here we fix the element 0 as a "root" to which
%       "all the small trees of the forest" are connected,
%       so we get the same sequence as with A000272.fnd,
%       but shifted once right.
%
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A000272
% http://mathworld.wolfram.com/PartialOrder.html
% http://www.iki.fi/~kartturi/matikka/ModFin/A000169.fnd
% http://www.iki.fi/~kartturi/matikka/ModFin/A000272.fnd
% http://www.iki.fi/~kartturi/matikka/ModFin/A000272Rv2.fnd
% http://www.iki.fi/~kartturi/matikka/ModFin/A001035R.fnd
%
% http://arp.anu.edu.au/~jks/finder.html
%
% Note: The penultimate axiom specifies that if a vertex has two distinct
%       nodes below it ("<"), then they should be comparable by themselves.
%       I.e. the Hasse-diagram of these posets cannot branch downward.
%
% One should probably read also this:
% R. Castelo and A. Siebes, A characterization of moral transitive directed acyclic graph
% Markov models as trees and its properties, Technical Report CS-2000-44,
% Faculty of Computer Science, University of Utrecht.
% ftp://ftp.cs.uu.nl/pub/RUU/CS/techreps/CS-2000/2000-44.ps.gz
%
%==========================================================================

sort {
        ELEM
        cardinality = 1
}


function {
        e:      ELEM,ELEM -> bool.
        f:      ELEM -> ELEM { cut }
}


clause {
        e(x,x) -> FALSE.                        % Irreflexive.
        e(x,y) -> FALSE = e(y,x).               % Asymmetric.
        FALSE = e(x,y); FALSE = e(y,z); e(x,z). % Transitive.
        FALSE = e(x,z); FALSE = e(y,z); x=y; e(x,y); e(y,x). % IF (x<z)&(y<z)&(x!=y) THEN x<y OR y<x.
        x -> e(f(x),x).                         % Every element, except the root (0) must have another element "less" than it.
}

setting {
        verbosity stats: full
        stack: maximal
}


end