⁵Equational unification can be represented in terms of a reachability problem [75] and, therefore, we do not consider completeness results for equational unification here; see [4] for a survey on termination of narrowing and completeness results for equational unification and reachability problems in the free case.