Най-напред ще се убедим, че ако една нетъждествена система от уравнения между термове не е в решен вид и не е явно нерешима, то към нея е приложимо поне едно преобразуване от изброените четири вида. И наистина, нека една система от уравнения между термове не е в решен вид и не е явно нерешима. Ще разгледаме два случая: а) лявата страна на всяко от уравненията в системата е някоя променлива; б) в системата има уравнение, на което лявата страна не е променлива. В случая а) ще разгледаме два подслучая: а1) лявата страна на някое от уравненията е променлива на дясната му страна; а2) лявата страна на никое от уравненията не е променлива на дясната му страна. В подслучая а1), като използваме, че системата не съдържа явно нерешимо уравнение, заключаваме, че системата съдържа уравнение, на което лявата и дясната страна са една и съща променлива  –  следователно в този подслучай може да се извърши премахване на тъждество. В подслучая а2), като използваме, че системата не е в решен вид, заключаваме, че лявата страна на някое от уравненията съвпада с лявата страна на друго от тях или е променлива на дясната му страна  –  следователно в този подслучай може да се извърши заместване. Да предположим сега, че е налице случаят б) и да разгледаме уравнение от системата, на което лявата страна не е променлива. Ако дясната страна на това уравнение е променлива, то ще може да се извърши обръщане. Остава да разгледаме възможността и дясната страна на това уравнение да не е променлива. Понеже системата не съдържа явно нерешимо уравнение, двете страни на разглежданото уравнение трябва да бъдат еднотипни. Едната възможност за това е двете страни да представляват една и съща константа  –  тогава ще може да се извърши премахване на тъждество. Другата възможност е уравнението да има вида

    Забележка 1. В горните разсъждения използвахме възможността за премахване само на специален вид тъждества – на такива, на които двете страни представляват една и съща променлива или една и съща константа. Значи разсъжденията биха били валидни и ако в описанието на преобразуването премахване на тъждество бяхме се ограничили само с такъв вид тъждества.

    След разсъжденията, които извършихме преди малко, вече се вижда следната евентуална възможност да се докаже, че отговорът на въпроса за резултатност на метода е положителен: да се покаже, че ако тръгнем от коя да е система от уравнения между термове и последователно получаваме нови системи от този вид чрез извършване на някои от четирите изброени видове преобразувания, то след известен брой такива преходи ще достигнем до система, за която не е възможно никое преобразуване от въпросните четири вида (според доказаното тази система непременно ще е в решен вид или ще съдържа явно нерешимо уравнение). Сега ще се възползваме от тази възможност.

    За една нетъждествена система от уравнения между термове ще казваме, че е решена относно дадена променлива ξ, ako ξ е лява страна на някое уравнение от системата и нито е променлива на дясната му страна, нито участва в някое друго от уравненията на системата. Лесно се проверява, че ако в системата има уравнение от въпросния вид, това уравнение се запазва или преминава в уравнение от същия вид при всяко от четирите разглеждани преобразувания. Следователно ако системата е решена относно дадена променлива и извършим някое от четирите преобразувания, новополучената система също ще е решена относно тази променлива. Освен това при всяко от четирите преобразувания множеството на променливите на новополучената система се съдържа в множеството на променливите на онази, от която е получена. Значи същото ще важи и за множеството на променливите, относно които системата не е решена. Това показва, че при никое от четирите вида преобразувания не може да нарастне броят на променливите, относно които системата не е решена. От друга страна при заместване този брой намалява строго, защото лявата страна ξ на използваното за заместването уравнение  ξ = θ при това преобразуване отпада от множеството на променливите, относно които системата не е решена. Ясно е при това положение, че когато тръгнем от една нетъждествена система от уравнения между термове и последователно извършваме преобразувания от четирите вида, не е възможно заместване да се извърши повече пъти, отколкото са променливите в първоначалната система. Остава да се убедим, че за всяка нетъждествена система от уравнения между термове има горна граница и за това колко пъти последователно могат да се извършват преобразувания от останалите три вида, без да се извършва заместване (ако покажем, че е така, става ясна невъзможността процесът на прилагане на преобразувания измежду разглежданите четири да продължи безкрайно  –  в противен случай след последното прилагане на заместване би трябвало да следват безбройно много прилагания на преобразувания измежду останалите три).

    Ще дефинираме за всеки терм положително цяло число, което ще наричаме негово тегло. Дефиницията е индуктивна: считаме, че променливите имат тегло 1, константите имат тегло 2, а теглото на терм от вида ω(α₁,…,α_m) при обичайните предположения за m, ω, α₁, …, α_m е увеличеният с 1 сбор от теглата на термовете α₁, …, α_m. Ясно е при тази дефиниция, че терм, който не е променлива, непременно има тегло, по-голямо от 1. Като използваме дефиницията и това следствие от нея, лесно виждаме, че ако подложим една система от уравнения между термове на някое преобразуване от първите три вида (без заместване), то сборът от теглата на левите страни на системата се намалява поне с 1. Това показва, че ако тръгнем от коя да е система от уравнения между термове, не е възможно последователно да извършваме преобразувания само от първите три вида повече пъти отколкото е сборът на теглата на левите страни на системата, от която сме тръгнали.

    Забележка 2. При заместване сборът на теглата на левите страни може не само да не намалее, а даже да нарастне (да речем в системата  X = a ,  X = b  теглата на левите части на уравненията имат сбор 2, а за системата  X = a ,  a = b , получена от нея чрез заместване, този сбор е 3). Това е причината, поради която в направените разсъждения си служим и с още един показател – броят нa променливите на системата, относно които тя не е решена.

    Забележка 3. Когато една система от уравнения между термове няма решение, това нерядко може да се види по описания начин без да има нужда да се извършват преобразувания от четирите вида до получаване на система, към която повече не са приложими такива преобразувания. Например от системата

    Установената тук резултатност на метода (заедно с обстоятелството, че при всяко от четирите преобразувания множеството на променливите на новополучената система се съдържа в множеството на променливите на онази, от която е получена) и онова, което знаем за системите в решен вид, позволяват да се направи следното заключение: ако една система от уравнения между термове има решение, то тя има идемпотентно най-общо решение, действащо в множеството на нейните променливи. Строго казано, ние доказахме това твърдение само за нетъждествени системи, но непосредствено се вижда неговата вярност и за тъждествените  –  при тях такова най-общо решение е тъждествената субституция.

Последно изменение: 28.06.2008 г.