num(z).
num(s(X)) :- num(X).

dec(s(X), X).
inc(X, s(X)).

add(X, z, X).
add(X, s(Y), s(Z)) :- add(X, Y, Z).

sub(X, Y, Z) :- add(Z, Y, X).    

mul(X, z, z).
mul(X, s(Y), Z) :- mul(X, Y, A), add(X, A, Z).

one(s(z)).
two(s(s(z))).
three(s(s(s(z)))).
four(s(s(s(s(z))))).
five(s(s(s(s(s(z)))))).
six(s(s(s(s(s(s(z))))))).
seven(s(s(s(s(s(s(s(z)))))))).
eight(s(s(s(s(s(s(s(s(z))))))))).
nine(s(s(s(s(s(s(s(s(s(z)))))))))).
ten(s(s(s(s(s(s(s(s(s(s(z))))))))))).
eleven(s(s(s(s(s(s(s(s(s(s(s(z)))))))))))).
twelve(s(s(s(s(s(s(s(s(s(s(s(s(z))))))))))))).
thirteen(s(s(s(s(s(s(s(s(s(s(s(s(s(z)))))))))))))).
fourteen(s(s(s(s(s(s(s(s(s(s(s(s(s(s(z))))))))))))))).
fifteen(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(z)))))))))))))))).

val(z, 0).
val(s(X), Y) :- val(X, Z), Y is Z + 1.

% val works perfectly for decoding peano numbers, i.e.
%   val(s(s(s(z))), X) produces X=3 and then stops without
%   getting into a loop searching for alternative answers.
% it also works perfectly as a filter, i.e.
%   val(s(s(s(s(z)))), 3) produces false and stops
%   val(s(s(s(z))), 3) produces true and stops
% it works perfectly as a generator, meaning that val(A, B)
%   produces A=z, B=0; A=s(z), B=1; and so on for all pairs.
% val only works partially as an encoder:
%   val(X, 4) correctly produces X=s(s(s(s(z)))) but if
%   backtracking occurs, it will get into an infinite loop
%   searching for another solution.