% term ::= atom | functor | variable | integers | ...
% atom ::= anything that starts with a lowercase letter
% socrates, happy
% sadlkFL
% variable ::= anything that start with uppercase letter
% X , X1 , Foo
% functor ::= atom applied to arguments:
% happy(socrates), likes(X, socrates)

rainy.
cold.

snowy :-                        % ←
    rainy ,
    cold.

% snowy :-
%     ','(rainy, cold).

human(socrates).
human(aristotle).
human(avicenna).

% human(X) :-
%     X = socrates ;   X = aristotle ;   X = avicenna.

mortal(X) :-
    human(X).

mentor(socrates, plato).
mentor(socrates, plotinus).
mentor(plato, aristotle).
mentor(aristotle, alexander-the-great).

influenced(X, Y) :-
    mentor(X, Y).

influenced(X, Y) :-
    influenced(X, Z),
    mentor(Z, Y).


% 1.2.1
% o ≡ 0
% s(o) ≡ 1
% s(s(o)) ≡ 2

% uadd : ℕ × ℕ → ℕ
% uadd ⊆ ℕ × ℕ × ℕ
% uadd(X, Y, Z) holds iff X + Y = Z

uadd(o, N, N).
uadd(s(N), M, s(X)) :-
    uadd(N, M, X).

uint(o, 0).
uint(s(N), X1) :-
    uint(N, X),
    X1 is X + 1.

umult(o, X, o).
umult(s(N), M, X) :-
    umult(N, M , Y),
    uadd(M, Y , X).

% 1.2.2
ufib(o, o).
ufib(s(o), s(o)).
ufib(s(s(X)), Y) :-
    ufib(s(X), Y1),
    ufib(X, Y2),
    uadd(Y1, Y2, Y).

% lists
% []
% [H | T]
% [1, 2, 3]

% 1.1.1
append([], Y , Y).
append([H | T], Y, [H | Z]) :-
    append(T, Y, Z).

% reverse([], []).
% reverse([H | T], Y) :-
%     reverse(T, T1),
%     append(T1, [H], Y).

reverseAcc([], Acc, Acc).
reverseAcc([H | T], Acc, X) :-
    reverseAcc(T, [H | Acc], X).
reverse(X, Y) :-
    reverseAcc(X, [], Y).

% 1.1.2
delete(_, [],[]).
delete(X, [X | T], T1) :-
    delete(X, T, T1).
delete(X, [H | T], [H | T1]) :-
    dif(X, H),
    delete(X, T, T1).

removeDuplicates([], []).
removeDuplicates([H | T], [H | T2]) :-
    delete(H, T, T1),
    removeDuplicates(T1, T2).