%%% -*- prolog -*-

%%% Peano Arithmetic!

%% term z for zero
%% term s(X) for successor of X

zero(z).
%% pred(X,Y) means "predecessor of X is Y"
pred(s(X),X).

%% | ?- pred(s(s(s(s(s(z))))), F), pred(F, T), pred(T, D), pred(D, O).
%% 
%% D = s(s(z))
%% F = s(s(s(s(z))))
%% O = s(z)
%% T = s(s(s(z)))
%% 
%% yes

%% add(X, Y, Z) means "X plus Y is Z"
add(z, X, X).
add(s(X), Y, s(Z)) :- add(X, Y, Z).

%% sub(X,Y,Z) means "X minus Y is Z"
sub(X, Y, Z) :- add(Y, Z, X).

%% CLOSED WORLD ASSUMPTION in action:
%% | ?- sub(s(s(s(z))), s(s(s(s(z)))), X).
%% no

%% mul(X, Y, Z) means "X times Y is Z"
mul(z, _ ,z).
mul(s(X), Y, Z) :- mul(X, Y, U), add(Y, U, Z). % z = (x+1)*y <- u=x*y, z=u+y

pyth(X, Y, Z) :- mul(X, X, X2), mul(Y, Y, Y2), mul(Z, Z, Z2), add(X2, Y2, Z2).

le(z,_).
le(s(X), s(Y)) :- le(X, Y).

%%% | ?- le(X, s(s(s(s(s(s(s(s(s(s(z))))))))))), le(Y, s(s(s(s(s(s(s(s(s(s(z))))))))))), le(Z, s(s(s(s(s(s(s(s(s(s(z))))))))))), pyth(X,Y,Z).
