Друго доказателство за завършване на унификационния процес след краен брой
стъпки
Нека е дадена една система от уравнения от вида
(1)
T1=U1, T2=U2,
..., Tn=Un,
където T1,T2,...,Tn,U1,U2,...,Un
са термове. Да наречем нейна сложност числото (2l+r)2s, където s е броят
на неизвестните в нея, относно които тя не е решена, l е сборът
на теглата на термовете T1,T2,...,Tn
и r е сборът от теглата на термовете U1,U2,...,Un. Ще можем да бъдем сигурни в завършването на унификационния
процес след краен брой стъпки, ако покажем, че сложността на системата
(1) строго намалява винаги, когато извършим някое от преобразуванията премахване
на тъждество, разпадане, обръщане и заместване. За първите три от тях това
се вижда лесно. За да се убедим, че е така и при четвъртото, първо доказваме,
че при всеки избор на променливата X и на термовете U и V
теглото на терма [U=:X](V) не надминава произведението
от теглата на двата терма U и V (доказателството може да
се извърши чрез индукция относно V, съобразена с дефиницията за
терм). Да предположим сега, че от системата (1) сме получили нова чрез
заместване, основаващо се на наличието в (1) на уравнение X=U,
където X е променлива, U е терм, X не е променлива
на U и X участва в някое друго от уравненията на (1).
Да означим с sў,lў
и rў новите стойности, които получават съответно
s, l и r след споменатото преобразуване на (1). Тъй като теглото
на терма U очевидно е по-малко от сбора 2l+r, лесно се съобразява,
че ще бъде в сила неравенството 2lў+rў<(2l+r)2. Оттук, като вземем
пред вид и неравенството sўЈs-1, получаваме, че