/*
This is the group example with an explicit definition
of equality. ``Only'' 2.5 times slower than the formulation
with the built-in equality.

In general it is nevertheless recommended to use the built-in
equality ``='' as some of the simplification techniques are more
powerful and/or faster in that case.
*/



predicates([eq]).

% definition of equality
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y), eq(Y,Z) -> eq(X,Z).
eq(X,Y) -> eq(i(X),i(Y)).

eq(X,Y) -> eq(X+Z,Y+Z).
eq(X,Y) -> eq(Z+X,Z+Y).



% group axioms
eq(e+X1,X1).
eq(i(X)+X,e).
eq(X1+X2+X3,X1+(X2+X3)).


precedence( [eq,i,+,e] ).