Termination conjecture for the SatSAGBI procedure

Let $K$[...]. Given a positively graded subalgebra $S$ and an indeterminate $a_0$, let $\sigma$ be a compatible term ordering, and let Procedure~ be the procedure that computes a $\sigma$-SAGBI basis of the saturation

$$S:a_0^\infty.$$

SatSAGBI termination conjecture. If there is a finite $\sigma$-SAGBI basis of $S:a_0^\infty$, then Procedure~ terminates in a finite number of iterations, hence it is an algorithm. The procedure is proved correct when it terminates; the delicate point is that its intermediate algebras might form a sequence that approaches the saturation without ever reaching it. The paper leaves finite termination under the stated finite-basis hypothesis open.