% Source: http://bibiserv.techfak.uni-bielefeld.de/cgi-bin/talp_submit/examples
% from: Thomas Arts, Hans Zantema,
%       Termination of logic programs using semantic unification,
%       In Proceedings of the Fifth International Workshop on
%       Logic Program Synthesis and Transformation, LNCS 1048,
%       pp. 219-233, Springer-Verlag, Berlin, 1996

right(tree(X, XS1, XS2), XS2).

flat(niltree, nil).
flat(tree(X, niltree, XS), cons(X, YS)) :-
        right(tree(X, niltree, XS), ZS),
        flat(ZS, YS).
flat(tree(X, tree(Y, YS1, YS2), XS), ZS) :-
        flat(tree(Y, YS1, tree(X, YS2, XS)), ZS).