X<X -> [].
X=<X.

p(s(X))=X.
s(p(X))=X.

X<s(X).
s(X)<X -> [].

(X<Y)==(s(X)=<Y).

(s(X)<s(Y))==(X<Y).

(s(X)=<s(Y))==(X=<Y).

(X=<Y) == (X<Y or X=Y).

(s(X)<Y)==(X<p(Y)).

(p(X)<Y)==(X<s(Y)).

%(X<Y), (Y=<X) -> [].


%(X=<Y) == ~(Y<X).

precedence([s,p,=<,<]).

option(var_overlaps(off)).