formula_list(usable).

(	all x ( n(k(n(I,x),U), k(n(I,c(x)),U)) = Z )).	% (xxiva)

(	all x ( u(k(n(I,x),U), k(n(I,c(x)),U)) = U )).	% (xxivb)

end_of_list.