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