formula_list(usable).

% the arbitrary selection operation a ("arb") is used here
%	to state well-foundedness of the membership relation e
%	(for definiteness, a(0)=0)


all y x ( e(y,a(x)) -> -( e(y,x) ) ).
a(0) = 0.

end_of_list.