Процедура исключения по алгоритму Бухбергера и базисам Грёбнера может завершиться неполным исключением и не дать многочлена от одной переменной. Почему в данном случае она завершается многочленом

- это может стать предметом отдельного рассмотрения, которое может быть не очень простым.
Она больше ничем не может закончиться. В худшем случае вы получите не один многочлен от одной переменной, а несколько; ну тогда возьмите их НОД. Лемма Сарда гарантирует, что никакого вырождения не будет.
-- Чт, 09 июн 2016 09:16:50 -- не процедура, а формула. И никакого отдельного рассмотрения не требуется.
Вы просто взяли наивную процедуру последовательного исключения одной переменной за другой и обозначили её шаги буквами

. Если вы думаете, что раньше никто до этого не додумывался, то вынужден вас разочаровать; проблема именно с лишними корнями, которые делают результат абсолютно бесполезным.