formula_list(usable). ( all x y z v ( (i(x,I) & i(z,I)) -> (k(n(x,z),n(y,v))=n(k(x,y),k(z,v))) )). % (xxiii)_1 end_of_list.