
704 van Emden and Szeredi
Let us combine this definition with that of merge. As the first step, we obtain
from the above implication the instance:
conj (m (Α. Χ, Β. Υ, A. Z) ,T2,T3,S)
if merge(m(Α.X,B.Y,A.Z)),times2(T2),times3(T3),
split(S)
We use the definition of merge to obtain by resolution ("unfolding" or
"partial application"):
conj (m(A.X,B. Υ,Α.Ζ) , T2,T3,S)
if lt(A,B) , merge (m(X,B. Υ, Z) ) , times2 (T2) ,times3(T3),
split(S)
When we now use the only if part of the definition of conj on the right-hand
side,
we obtain (by "folding"):
conj (m(A.X,B. Υ,Α.Ζ) ,T2,T3,S)
if lt(A,B) ,conj (m(X,B. Y,Z) ,T2,T3,S)
In a similar way, each of th ...