Encompassment ordering (original) (raw)

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 s ≤ t if a subterm of t is a substitution instance of s. It is used e.g. in the Knuth–Bendix completion algorithm.