formula_list(usable).

(	all x ( k(I,x) = x) ).	% (ix)_2

(	all x ( i(x,k(x,U)))).	% (ix)_3	

(	all x ( i(x,k(U,x)))).	% (ix)_4

(	all x ( i(d(Z,x),x))).	% (ix)_5

(	all x ( i(d(x,Z),x))).	% (ix)_6

              ( k(U,U) = U).	% (ix)_7 == (ii)_0
 
              ( d(Z,Z) = Z).	% (ix)_8

end_of_list.