p(X,Y,X,Y).
p(X,Y,Y,X).
p(X,Y,Z,X,A,B) :- p(Y,Z,A,B).
p(X,Y,Z,A,X,B) :- p(Y,Z,A,B).
p(X,Y,Z,A,B,X) :- p(Y,Z,A,B).
p(X,Y,Z,U,X,A,B,C) :- p(Y,Z,U,A,B,C).
p(X,Y,Z,U,A,X,B,C) :- p(Y,Z,U,A,B,C).
p(X,Y,Z,U,A,B,X,C) :- p(Y,Z,U,A,B,C).
p(X,Y,Z,U,A,B,C,X) :- p(Y,Z,U,A,B,C).

minus(z,_,z).
minus(X,z,X).
minus(s(X),s(Y),Z)   :- minus(X,Y,Z).

nat(z).
nat(s(X)) :- nat(X).
p(X) :- nat(X).
p(X) :- p(s(X)), eq(X,s(X)).
eq(X,X).

half(X,Y) :- double(Y,X). 
half(X,Y) :- p(X,Z), double(Y,Z). 
p(s(X),X).

double(z,z).
double(s(X),s(s(Y))) :- double(X,Y).

append(n,YS,YS).
append(c(X,XS),YS,c(X,ZS)) :- append(XS,YS,ZS).

perm(n,n).
perm(XS,c(Y,YS)) :- delet(Y,XS,ZS), perm(ZS,YS).

delet(X,c(X,XS),XS).
delet(X,c(Y,YS),c(Y,ZS)) :- delet(X,YS,ZS).
and(true, true, true ).
and(true, false,false).
and(false,true, false).
and(false,false,false).
