В результате к самым верхним вершинам дерева редукций могут быть приписаны секвенции единственного вида .
Пусть v – одна из таких вершин.
а) если секвенция, приписанная v, содержит одинаковую переменную и слева и справа, то v больше не раскрывается и помечается значком «+».
б) иначе если в секвенции, приписанной v, k=0, то v больше не раскрывается и помечается значком «-».
в) иначе если секвенция, приписанная v, уже приписана некоторой вершине w, располагающейся в дереве редукций ниже v, то v больше не раскрывается и помечается значком <-, w>.
г) иначе к вершине v применяется редукция 2 рода следующего вида:
… …. …
и т.д.
Ясно, что алгоритм построения дерева редукций закончит работу за конечное число шагов.