formula_list(usable). % corollary of Schroeder's cycle law

	( all x y z ( (n(x,k(z,r(y))) = Z) -> (n(z,k(x,y)) = Z) )).

end_of_list.