%=======================================================================
%
%       
%       Handshaking across a table (everybody shaking), with
%       no crossing handshakes allowed.
%       Is enumerated by 0,1,0,2,0,5,0,14,0,42,0,132,0,429,0,1430,0,4862,0,16796,0,...
%       whose bisection is the famous A000108, Catalan numbers.
%
% Actually, it's more natural to think here Stanley's interpretation (o),
% ways of connecting 2n points in the plane lying on a horizontal line
% by n nonintersecting arcs, each arc connecting two of the points
% and lying above the points, or
% (kk) fixed-point free involutions w of [2n] such that if i < j < k < l
% and w(i) = k, then w(j) != l (in other words, 3412-avoiding fixed-point
% free involutions), which are essentially the same thing.
%
% See http://www-math.mit.edu/~rstan/ec/catalan.ps.gz
% Exercise 19 for the interpretations.
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A000108
% http://www.research.att.com/~njas/sequences/a002694.gif
% http://www.maths.usyd.edu.au:8000/u/kooc/catalan.html
% http://www.iki.fi/~kartturi/matikka/ModFin/A000110A.fnd
%
% http://arp.anu.edu.au/~jks/finder.html
%
% The last axiom says, that
% if((x<y) && (y != f(x)) && (x < f(x)) && (y < f(y)))
% then should hold either that (f(x) < y) or f(y) < f(x).
%
% I.e. the relative orders   x   < f(x)  <   y   < f(y)
%                      and   x   <   y   < f(y)  < f(x)
% are possible,
%               but not:     x   <   y   < f(x)  < f(y)
%
% The semicolon (;) in clauses stands for disjuction, "or".
%
%==========================================================================

sort {
        int
        cardinality = 20
}


function {
        f:      int -> int { bijective }
}


clause {
        f(x) = x -> FALSE.                      % No fixed points.
        f(x) = y -> f(y) = x.                   % Just transpositions, no larger cycles.
        x=y; x>y; y=f(x); x>f(x); y>f(y); f(x)<y; f(y) < f(x).
}

setting {
        verbosity stats: full
        stack: maximal
}


end