%=======================================================================
%
%       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.
%
%       Do it hard way: Compare to:
%       http://www.iki.fi/~kartturi/matikka/ModFin/A000272R.fnd
%
%       Again, 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.
%
% Note that we use the "Skolem-function" g in two distinct ways:
% g(x,x) gives for non-root vertices a preceding vertex v < x,
% and g(x,y) gives a vertex v between x and y: x < v < y.
% if x and y are distinct, and themselves comparable x < y.
%
% This because having multiple "cut"-functions here would
% probably mess up the number of solutions FINDER will give.
%
% But we have to make g partial, because with irreflexive
% comparison rules, there might not always be such intermediate
% vertex. So in the fourth clause, we have to use
% the dummy typeless "exists" (EST, which previously was known as E!).
% Compare to the elegance of
% http://www.iki.fi/~kartturi/matikka/ModFin/A000272.fnd
%
% 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://arp.anu.edu.au/~jks/finder.html
%
%=======================================================================

sort {
        ELEM
        cardinality = 6
}


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


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.
        x=y; FALSE = e(x,z); FALSE = e(y,z); EST(g(x,z)); EST(g(y,z)). % IF (x!=y)&(x<z)&(y<z) THEN exists either v: x<v<z or w: y<w<z.
        x -> e(g(x,x),x).                       % For non-root vertices, return a preceding vertex...
        x -> EST(g(x,x)).                       % which must exist!
        FALSE = e(x,y); e(x,g(x,y)).            % IF (x<y), THEN g(x,y) "gives" a vertex v FOR which v > x.
        FALSE = e(x,y); e(g(x,y),y).            %            AND v < y.  (i.e. x < v < y).
}

setting {
        verbosity stats: full
        stack: maximal
}


end