ocean_level(rising).
temperature(extreme).
global_warming(conspiracy) :- 
  ocean_level(stable), 
  temperature(normal).
global_warming(real) :- 
  ocean_level(rising), 
  temperature(extreme).

nat(z).
nat(s(N)) :- nat(N).

plus(z, N, N).
plus(s(M), N, s(P)) :- 
  plus(M, N, P).

mult(z, N, z).
mult(s(M), N, P) :- 
  plus(Q, N, P), 
  mult(M, N, Q).

mem(X, [X | _]).
mem(X, [Y | Ys]) :- 
  X \= Y,
  mem(X, Ys).

listsum([], z).
listsum([X | Xs], N) :-
  nat(X),
  listsum(Xs, M),
  plus(X, M, N).

eval(app(E1,E2), F) :-
  eval(E1,E1prime), 
  eval(app(E1prime,E2), F).
eval(app(lam(X,E),E2),F) :- 
  subst(E2,X,E,F).

subst(E,X,v(X),E).
subst(E,X,v(Y),v(Y)) :- 
  X \= Y.
subst(E,X,app(E1,E2),app(E1prime,E2prime)) :-
  subst(E,X,E1,E1prime), 
  subst(E,X,E2,E2prime).
subst(E,X,lam(X,F),lam(X,F)).
subst(E,X,lam(Y,F),lam(Y,Fprime)) :- 
  X \= Y, 
  subst(E,X,F,Fprime).