Encompassment ordering

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.