remove(A,Setu)=Setu  <- empty(Setu).

set_of_fours(Sete) -> empty(Sete),exists(X,member(X,Sete)).

member(A,remove(A,Setu)) -> [].

member(B,Setu) and ~(A=B) -> member(B,remove(A,Setu)). 

member(B,remove(A,Setu))=> member(B,Setu).

exists(X,member(X,Setu))=>member(choose(Setu),Setu).

all(Setu,all(Setv,all(X,member(X,Setu)<=>member(X,Setv))=>choose(Setu)=choose(Setv))).

four_tuple(X)<=>exists(Y,exists(Z,exists(A,exists(B,X=(Y,Z,A,B))))).

set_of_fours(Sete)<=>all(X,member(X,Sete)=>four_tuple(X)).

f((X,Y,Z,U))=Z.

is_set(nil).

is_set(cons(X,Y))<- is_set(Y) and ~member(X,Y).



member(_,nil) -> [].
member(U,cons(V,G)) <=>  U=V or  member(U,G).

nonempty(Setv)<=>exists(X,member(X,Setv)).

empty(Setv)<=>(~(nonempty(Setv))).


/*lemma1==exists(Sete,nonempty(Sete)).*/

sum(Sete)=0<-empty(Sete) and is_set(Sete).

sum(Sete)=sum(remove(choose(Sete),Sete))+choose(Sete)<-is_set(Sete).

/*
~all(Sete,sum(Sete)=0).

lemma1.

lemma1==exists(Sete,~nonempty(Sete)).*/


X+0=X.

X+Y=X<=>Y=0.

X+Y=Y<=>X=0.


%%~exists(X,set_of_fours(X) and is_set(X) and  exists(Y,member(Y,X))).

lemmax==exists(X,nonempty(X) and set_of_fours(X) and  is_set(X)).

%%exists(X,nonempty(X) and set_of_fours(X)).

%%exists(X,nonempty(X) and is_set(X)).
%%~exists(X,nonempty(X)).

lemmax.





%%~exists(Sete,is_set(Sete) and exists(X,member(X,Sete) and ~(f(X)=0))).

%%all(Sete,set_of_fours(Sete)=>all(X,member(X,Sete)=>f(X)=0)).

~ exists(X,~(X=0)).




%%all(Sete,is_set(Sete)=>sum(Sete)=0).




precedence([sum,f,set_or_fours,remove,empty,four_tuple,choose,member]).