formula_list(usable).

( all x y z ( i(k(r(x),x),I) -> i(n(k(x,y),k(x,z)), k(x,n(y,z))) )).

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

end_of_list.