formula_list(usable). %specialized variant of (viii): ( all x y z w ( (i(x,I) & i(y,I)) -> (k(n(x,y),n(z,w))=n(n(k(x,z),k(y,z)),n(k(x,w),k(y,w)))) )). ( all x y z w (i(n(k(x,z),k(y,w)), k(k(x,r(x)),k(y,w))) )). end_of_list.