% reflexivity
eq(X,X).

% X*e = X
eq(X*e,W) == eq(X,W) <- eq(E,E)	if [X*e>=W].

% X*i(X) = e
eq(X*IX,W) == eq(e,W) <- eq(i(X),IX)		if [X*IX>=W,i(X)>=IX].

% X*(Y*Z) = (X*Y)*Z
eq(V*Z,W) == eq(X*U,W) <- eq(Y*Z,U), eq(X*Y,V)	if [V*Z>=W,Y*Z>=U,X*Y>=V].

% goal <- e*x = x
% goal [] <- eq(E*X,x), eq(e,E), eq(x,X) if [e>=E,x>=X].

% goal <- e*e = e
% goal [] <- eq(E*E,e), eq(e,E) if [e>=E].

% goal <- i(x)*x = e
goal [] <- eq(IX*X,e), eq(i(X),IX), eq(x,X) if [i(X)>=IX,x>=X].



option(horn(off)).