English: Lattice of generalizations of the term (a*b)*c, with a, b, c constants and x, y, z variables. Multiplication operators "*" are omitted in the picture. All involved terms are linear, i.e. don't contain multiple occurrences of the same variable. To the right of each term, the set of its paths leading to a function (or constant) symbol is shown in blue; the path numbering scheme is shown in the upper left corner for the term (a*b)*c. Join and meet in this lattice, i.e. anti-unification and unification of terms, corresponds to intersection and union of their path sets, respectively. Since this correspondance is a lattice isomorphism, the shown lattice is distributive. Similarly, every sublattice of the subsumption lattice of linear terms that doesn't contain Ω is distributive. See en:Subsumption lattice for a nondistributive sublattice of linear terms including Ω.