%=======================================================================
%
%       Functions on domain {0..n-1} for which f(0)=0
%       and f(x+1) is never greater than f(x)+1.
%       Is enumerated by EIS A000108 (1,1,2,5,14,42,132,429,...)
%       a.k.a. Catalan numbers.
%       Probably the simplest axiomatization that results
%       a structure enumerated by Catalans.
%       Direct correspondence with Stanley's interpretations
%       (pp), (qq) and (rr), where the last is
%       "noncrossing Murasaki diagrams with n vertical lines".
%
% See http://www-math.mit.edu/~rstan/ec/catalan.ps.gz
% Exercise 19 for those interpretations.
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A000108
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A071157
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A071159
% C. Banderier, A. Denise, P. Flajolet, M. Bousquet-Milou et al.,
% Generating Functions for Generating Trees, Discrete Mathematics 246(1-3), March 2002, pp. 29-55.
% Available at: http://pauillac.inria.fr/algo/banderier/Papers/DiscMath99.ps
% http://www.maths.usyd.edu.au:8000/u/kooc/catalan.html
% http://www.iki.fi/~kartturi/matikka/ModFin/A000108.fnd
% http://www.iki.fi/~kartturi/matikka/ModFin/A000108A.fnd
%
% http://arp.anu.edu.au/~jks/finder.html
%
%==========================================================================

sort {
        int
        cardinality = 1
}


function {
        f:      int -> int.
}


clause {
        f(0) = 0.
        x > 0 -> FALSE=(f(x-1)+1 < f(x)).  % No larger than one-step leaps upward.
}

setting {
        verbosity stats: full
        stack: maximal
}


end