formula_list(usable).

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

( 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.