formula_list(usable). % preparation for Schroeder's cycle law

	( all x y z ( u(k(r(x),c(u(c(z),k(x,y)))),c(y)) = c(y) )).

	( all x ( k(x,I) = x )). 	% BVI

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

end_of_list.