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

% Defining mod(X,Y,Z)
% “Z is the remainder from dividing X by Y”

% Specification: 
% ∃Q s.t. X = Y ∗ Q + Z   ∧   Z < Y

% We can simply write the specification:
mod(X,Y,Z) :- 
    less(Z, Y), 
    times(Y,_Q,W), 
    plus(W,Z,X).

% Try:
% ?- op(100,fy,s).
% (defines s as a prefix operator to save us 
%  writing parenthesis)
% ?- mod(s s s s s s s s s s s s s 0, s s s 0, Z).
% ?- mod(s s s s s s s s s s s s s 0, Y, s 0).

% Another possible definition:
mod2(X,Y,X) :- 
    less(X, Y).
mod2(X,Y,Z) :- 
    plus(X1,Y,X), 
    mod2(X1,Y,Z).

% ?- mod2(s s s s s s s s s s s s s 0, s s s 0, Z).
% ?- mod2(s s s s s s s s s s s s s 0, Y, s 0).

% This second is more efficient than the first one
% for several query modes.

% Other predicates:

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

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

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

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