³Equational unification can be represented in terms of a reachability problem [66] (see Section 12.6.1) and, therefore, we do not consider completeness results for equational unification here; see [5] for a recent survey on termination of narrowing and completeness results for equational unification and reachability problems in the free case.