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

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

exp(X,0,s(0)).
exp(X,s(Y),Z):-exp(X,Y,V),fois(X,V,Z).

eval(0,0).
eval(s(X),s(Y)):-eval(X,Y).
eval(a(X,Y),Z):-eval(X,Xe),eval(Y,Ye),plus(Xe,Ye,Z).
eval(m(X,Y),Z):-eval(X,Xe),eval(Y,Ye),fois(Xe,Ye,Z).
eval(e(X,Y),Z):-eval(X,Xe),eval(Y,Ye),exp(Xe,Ye,Z).

div(X,Y,0,X):-plus(s(Z),X,Y).
div(X,Y,s(Q),R):-plus(Z,Y,X),div(Z,Y,Q,R).

npremier(X):-plus(s(s(Y)),s(Z),X),div(X,s(s(Y)),Q,0).

ndiv(X,Y):-div(X,Y,Q,s(R)).
nndiv(X,0).
nndiv(X,s(0)).
nndiv(X,s(s(Y))):-ndiv(X,s(s(Y))),nndiv(X,s(Y)).
est_premier(s(X)):-nndiv(s(X),X).

fib(0,0).
fib(s(0),s(0)).
fib(s(s(X)),Y):-fib(s(X),Xsf),fib(X,Xf),plus(Xsf,Xf,Y).

fnn(atom(X),atom(X)).
fnn(et(X,Y),et(Xe,Ye)):-fnn(X,Xe),fnn(Y,Ye).
fnn(ou(X,Y),ou(Xe,Ye)):-fnn(X,Xe),fnn(Y,Ye).
fnn(imp(X,Y),ou(Xe,Ye)):-fnn(neg(X),Xe),fnn(Y,Ye).
fnn(neg(et(X,Y)),ou(Xe,Ye)):-fnn(neg(X),Xe),fnn(neg(Y),Ye).
fnn(neg(ou(X,Y)),et(Xe,Ye)):-fnn(neg(X),Xe),fnn(neg(Y),Ye).
fnn(neg(imp(X,Y)),et(Xe,Ye)):-fnn(X,Xe),fnn(neg(Y),Ye).
fnn(neg(neg(X)),Xe):-fnn(X,Xe).
fnn(neg(atom(X)),neg(atom(X))).

distrib(atom(X),atom(X)).
distrib(neg(atom(X)),neg(atom(X))).
distrib(et(X,Y),et(Xe,Ye)):-distrib(X,Xe),distrib(Y,Ye).
distrib(ou(X,Y),D):-distrib(Y,et(A,B)),distrib(et(ou(X,A),ou(X,B)),D).
distrib(ou(X,Y),D):-distrib(X,et(A,B)),distrib(et(ou(A,Y),ou(B,Y)),D).
distrib(ou(X,Y),D):-distrib(X,ou(A,B)),distrib(ou(A,ou(B,Y)),D).
distrib(ou(atom(Z),Y),ou(atom(Z),ou(A,B))):-distrib(Y,ou(A,B)).
distrib(ou(neg(atom(Z)),Y),ou(neg(atom(Z)),ou(A,B))):-distrib(Y,ou(A,B)).
distrib(ou(atom(Z),atom(Y)),ou(atom(Z),atom(Y))).
distrib(ou(atom(Z),neg(atom(Y))),ou(atom(Z),neg(atom(Y)))).
distrib(ou(neg(atom(Z)),atom(Y)),ou(neg(atom(Z)),atom(Y))).
distrib(ou(neg(atom(Z)),neg(atom(Y))),ou(neg(atom(Z)),neg(atom(Y)))).

fnc(X,Y):-fnn(X,Z),distrib(Z,Y).
	

pol(atom(X),R,cons(atom(X),R)).
pol(top,R,cons(tops,R)).
pol(bot,R,cons(bots,R)).
pol(et(X,Y),R,cons(ets,P)):-pol(Y,R,Q),pol(X,Q,P).
pol(ou(X,Y),R,cons(ous,P)):-pol(Y,R,Q),pol(X,Q,P).
pol(imp(X,Y),R,cons(imps,P)):-pol(Y,R,Q),pol(X,Q,P).
pol(neg(X),R,cons(negs,P)):-pol(X,R,P).