%==========================================================================
%
%       Number of labeled rooted trees with n nodes: n^(n-1), with
%       no node having (upward) branching degree greater than 2.
%       Is enumerated by EIS A0????? (1,2,9,60,480,4320,....) Not in EIS.
%       (Except that with these axiomatizations we don't get a solution for
%        cardinality = 1).
%
% Notes:
%
%  The fourth 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.
%
%  The fifth axiom specifies that no vertex can have three vertices
%  "larger than it", which themselves would be incomparable.
%  I.e. the maximum branching degree of the tree is 2.
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A000169
% http://www.iki.fi/~kartturi/matikka/ModFin/A000169.fnd
%
% http://arp.anu.edu.au/~jks/finder.html
%
%==========================================================================

sort {
        ELEM
        cardinality = 6
}


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


clause {
        e(x,x).                                 % Reflexive.
        FALSE = e(x,y); FALSE = e(y,x); x=y.    % Antisymmetric.
        FALSE = e(x,y); FALSE = e(y,z); e(x,z). % Transitive.
        x=z; y=z; x=y; FALSE = e(x,z); FALSE = e(y,z); e(x,y); e(y,x). % IF (x<z)&(y<z)&(x!=y) THEN x<y OR y<x.
        FALSE=e(w,x); FALSE=e(w,y); FALSE=e(w,z); e(x,y); e(x,z); e(y,z); e(y,x); e(z,x); e(z,y).
        x=y; e(f(x),x); e(f(y),y).              % If x and y are distinct, then at least other has a predecessor,
        f(x) = x -> FALSE.                      % which is _true_ predecessor.
}

setting {
        verbosity stats: full
        stack: maximal
}


end