% Peano represention: o (zero), s (successor)
% s(s(s(o))) represents "three"

isPeano(o).
isPeano(s(N)) :- isPeano(N).

% add(X,Y,Z) <=> Z is the sum of X and Y
add(o,Y,Y).
add(s(X),Y,s(Z)) :- add(X,Y,Z).

% sub(X,Y,Z) <=> Z is the difference of X and Y (<=> add(Y,Z,X))
sub(X,Y,Z) :- add(Y,Z,X).

% mult(X,Y,Z) <=> Z is the product of X and Y
mult(o,_,o).
mult(s(X),Y,Z) :- mult(X,Y,XY), add(XY,Y,Z).

% less-or-equal relation
leq(o,_).
leq(s(X),s(Y)) :- leq(X,Y).
