:- module(_,_,[sr/bfall]).

% Simplest recursive type: nat/1

nat(0).
nat(s(X)) :- nat(X).

% Recursive programming: arithmetic with nats

less_or_equal(0,X) :- nat(X).
less_or_equal(s(X),s(Y)) :- less_or_equal(X,Y).

%% Multiple uses: 
% ?- less_or_equal(s(0),s(s(0))).
% ?- less_or_equal(X,0).
% 
% Multiple solutions:
% ?- less_or_equal(X,s(0)).
% ?- less_or_equal(s(s(0)),Y).

plus(0,Y,Y) :- nat(Y).
plus(s(X),Y,s(Z)) :- plus(X,Y,Z).

% Multiple uses: 
% ?- plus(s(s(0)),s(0),Z).
% ?- plus(s(s(0)),Y,s(0)).
% ?- plus(s(0),Y,s(s(s(0)))).
%
% Multiple solutions: 
% ?- plus(X,Y,s(s(s(0)))).

% Alternative definition:
plus_alt(X,0,X) :- nat(X).
plus_alt(X,s(Y),s(Z)) :- plus_alt(X,Y,Z).

% The meaning of plus is the same, even if both 
% defintiions are combined (not recommended!)

% Try to define: times(X,Y,Z) (Z = X*Y), exp(N,X,Y)
% (Y = X^N ), factorial(N,F) (F = N!), 
% minimum(N1,N2,Min), ...