%=======================================================================
%
%       Unlabeled rooted plane binary trees counted by their leaves.
%       Is enumerated by EIS A000108 (1,1,2,5,14,42,132,429,...)
%       a.k.a. Catalan numbers.
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A000108
% http://www.iki.fi/~kartturi/matikka/ModFin/A001147.fnd
%
% http://arp.anu.edu.au/~jks/finder.html
%
% See the following two papers by Peter J. Cameron:
%
% Orbits of permutation groups on unordered sets, IV: homogeneity and transitivity,
% J. London Math. Soc. (2) 27 (1983), 238-247.
%
% Some treelike objects, Quart. J. Math. Oxford (2) 38 (1987), 155-183.
%
% On pages 240 & 241 of the former paper, we have five axioms:
%
% A1. If x|yz holds, then x, y, z are distinct.
% A2. If x|yz holds, then x|zy holds.
% A3. If x|yz and x|yw hold, then x|zw holds. (z and w distinct!)
% A4. for any distinct x, y, z, exactly one of x|yz, y|zx, z|xy holds.
% A5. for no four points a,b,c,d it is true that a|bc, b|cd, c|da, d|ab hold.
%
% We add a sixth axiom, to impose a circular order on the leaves:
%
% A6. If x|yz holds, then either x = min(x,y,z) or x = max(x,y,z).
%
% with the nice result that we get rooted binary plane trees!
% (See the page 160 of the latter paper).
%
%=======================================================================

sort {
        LEAF
        cardinality = 4
}


function {
        b:        LEAF,LEAF,LEAF -> int.  % b(x,y,z)=1 means that leaf x bifurcates before y and z.
}


clause {
%% Make b actually a boolean function (obtaining only values 0 or 1):
        b(x,y,z) > 1 -> FALSE.
%% Axiom A1:
        b(x,x,y) = 0.
        b(x,y,y) = 0.
        b(x,y,x) = 0.
%% Axiom A2:
        b(x,y,z) -> b(x,z,y).           % The second and third arg commute.
%% Axiom A3:
        z=w; 0=b(x,y,z); 0=b(x,y,w); b(x,z,w).
%% Axiom A4:
        x = y; y = z; x = z; (b(x,y,z) + b(y,z,x) + b(z,x,y) = 1).
%% Axiom A5:
        0=b(x,y,z); 0=b(y,z,w); 0=b(z,w,x); 0=b(w,x,y).
%% Axiom A6:
        x < y; x > z; b(x,y,z)=0.
        x < z; x > y; b(x,y,z)=0.
}

setting {
        verbosity stats: full
        stack: maximal
        ugly
}


end