{{Short description|Term ordering in abstract rewriting}} thumb|Triangle diagram of two terms ''s'' ≤ ''t'' related by the encompassment preorder. In theoretical computer science, in particular in automated theorem proving and term rewriting, the '''containment''',<ref>{{cite journal| author=Gerard Huet| title=A Complete Proof of Correctness of the Knuth–Bendix Completion Algorithm| journal=J. Comput. Syst. Sci.| year=1981| volume=23| number=1| pages=11–21| doi=10.1016/0022-0000(81)90002-7| doi-access=free}}</ref> or '''encompassment''', preorder (≤) on the set of terms, is defined by<ref>{{cite book| author=N. Dershowitz, J.-P. Jouannaud| title=Rewrite Systems| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| editor-link=Jan van Leeuwen| series=Handbook of Theoretical Computer Science}} Here:sect.2.1, p. 250</ref> :''s'' ≤ ''t'' if a subterm of ''t'' is a substitution instance of ''s''. 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,<ref group=note>since both ''f''(''x'') ≤ ''f''(''y'') and ''f''(''y'') ≤ ''f''(''x'') for variable symbols ''x'', ''y'' and a function symbol ''f''</ref> nor total<ref group=note>since neither ''a'' ≤ ''b'' nor ''b'' ≤ ''a'' for distinct constant symbols ''a'', ''b''</ref> * 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''<ref group=note>i.e. irreflexive, transitive, and well-founded binary relation ''R'' such that ''sRt'' implies ''u''[[term (logic)#Operations with terms|[]]''s''σ]<sub>''p''</sub> R ''u''[''t''σ]<sub>''p''</sub> for all terms ''s'', ''t'', ''u'', each path ''p'' of ''u'', and each substitution ''σ''</ref> with (<) is well-founded, where (<) denotes the irreflexive kernel of (≤).<ref>Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy, ''R'' is required to be a "terminating rewrite relation" there.</ref> In particular, (<) itself is well-founded.
==Notes== {{Reflist|group=note}}
==References== {{Reflist}}
Category:Rewriting systems Category:Order theory
{{comp-sci-stub}}