%
% multiplication on integers
%

use(int).

X+0=X.
0+X=X.
X+s(Y)=s(X+Y).
% s(X)+Y=s(X+Y). % leads to non-termination


% unary minus
% due to a limitation in the concept
% of precedences we cannot use "-" for both
% the unary and binary "minus"

--0=0.
--s(X)=p(--X).

X-Y = X+ (--Y).


1=s(0).

X*1=X.
1*X=X.
X*0=0.
0*X=0.

X*s(Y)=X+X*Y.