Encompassment ordering

In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment, or encompassment, preorder (≤) on the set of terms, is defined by

It is used e.g. in the Knuth–Bendix completion algorithm.

Properties

• Encompassment is a preorder, i.e. reflexive and transitive, but not anti-symmetric, nor total
• The corresponding equivalence relation, defined by s ~ t if s Ã¢Â‰Â¤ t Ã¢Â‰Â¤ s, is equality modulo renaming.
• s Ã¢Â‰Â¤ t whenever s is a subterm of t.
• s Ã¢Â‰Â¤ t whenever t is a substitution instance of s.
• The union of any well-founded rewrite order R with (<) is well-founded, where (<) denotes the irreflexive kernel of (≤). In particular, (<) itself is well-founded.

Notes

References