formula_list(usable).

( all x y z ( i(k(r(x),x),I) -> ( k(n(k(z,r(x)),y),x)=n(z,k(y,x)) ) )). % (xxviii)_2

end_of_list.