formula_list(usable).

(	all x y z ( k(x,k(y,z)) = k(k(x,y),z) )).	% (iv)_1 == BIV

(	all x y z ( d(x,d(y,z)) = d(d(x,y),z) )).	% (iv)_2

end_of_list.