Knuth-Bendixは停止性が保証されないので、その多項式環への具体化とみなせるBuchbergerアルゴリズムも、停止性が保証されないと思いこんでいた。が、
こっちは必ず停止するのか。