formula_list(usable).

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

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

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

end_of_list.