formula_list(usable).

( all x y ( d(x,r(y)) = U <-> u(d(Z,x),y) = U )).       % (xix)_1

( all x y ( d(x,r(y)) = U <-> u(d(Z,x),d(Z,y)) = U ) ). % (xix)_2

end_of_list.