ترتيب الإحاطة

في علوم الحاسوب النظرية ، وخاصة في إثبات النظريات الآلي وإعادة كتابة المصطلحات ، يتم تعريف الاحتواء ، ^{[ 1 ]} أو الشمول ، الترتيب المسبق (≤) على مجموعة المصطلحات ، بواسطة ^{[ 2 ]}

s  ≤ t إذا كان أحد الحدود الفرعية لـ t هو حالة استبدال لـ s . 

يتم استخدامه على سبيل المثال في خوارزمية إكمال كنوت-بنديكس .

• إن الاحتواء هو ترتيب مسبق ، أي انعكاسي ومتعدي ، ولكنه ليس مضادًا للتناظر ، ^{[ ملاحظة 1 ]} ولا كليًا ^{[ ملاحظة 2 ]}
• العلاقة المكافئة المقابلة ، المعرفة بواسطة s  ~ t إذا كان s ≤ t ≤ s ، هي المساواة modulo إعادة التسمية .     
• s  ≤ t عندما يكون s حدًا فرعيًا من t . 
• s  ≤ t عندما يكون t حالة استبدال لـ s . 
• إن اتحاد أي ترتيب إعادة كتابة سليم R ^{[ ملاحظة 3 ]} مع (<) هو اتحاد سليم ، حيث يرمز (<) إلى النواة غير الانعكاسية لـ (≤). ^{[ 3 ]} وعلى وجه الخصوص، فإن (<) نفسه سليم.