formula_list(usable).

% symmetric difference s

all x v z ( s(s(x,v),z) = s(x,s(v,z)) ).
all v z ( s(v,s(z,v)) = z ).
all z v ( s(z,z) = s(v,v) ).

% intersection n

all x v z ( n(n(x,v),z) = n(x,n(v,z)) ).
all v z x ( n(s(v,z),x) = s(n(x,z),n(x,v)) ).
all x ( n(x,x) = x ).

% inclusion i

all x v ( i(x,v) <-> ( n(x,v) = x ) ).

% dyadic union u

all x v ( u(x,v) = s(s(x,v),n(x,v)) ).

end_of_list.