%=======================================================================
%
%	Partially ordered sets ("posets") with n labeled elements,
%       with all elements having a common meet.
%
%       Is enumerated by EIS A001035 (1,1,3,19,219,4231,130023,...),
%
%       Here we fix the element 0 as a "root" where
%       "all the little posets" eventually meet,
%       so we get the same sequence as with A001035.fnd,
%       but shifted once right.
%
% See also:
%
% http://www.research.att.com/cgi-bin/access.cgi/as/njas/sequences/eisA.cgi?Anum=A001035
% http://mathworld.wolfram.com/PartialOrder.html
% http://www.iki.fi/~kartturi/matikka/ModFin/A006059.fnd
%
% http://arp.anu.edu.au/~jks/finder.html
%
%=======================================================================

sort {
        ELEM
        cardinality = 4
}


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 -> e(f(x),x).                         % Every element, except the root (0) must have
        f(x) = x -> FALSE.                      % _another_ element "less" than it.
}

setting {
        verbosity stats: full
        stack: maximal
}


end