formula_list(usable).

( all x y z v ( (i(x,I) & i(z,I)) -> (k(n(y,v),n(x,z))=n(k(y,x),k(v,z))) )). % (xxiii)_2

end_of_list.