have the following theoretical algorithm, alluded to in Theorem \[thm:GGB\]. We do not claim that it terminates, but if it does, then it returns a finite equivariant Gröbner basis by Theorem \[thm:Buchberger\].

 

Input

:   a finite subset $B$ of $K[X]$.

Output (assuming termination)

:   a finite equivariant Gröbner basis of the ideal generated by $GB$.

Procedure

:    

    1.  $P:=B \times B$;

    2.  while $P \neq \emptyset$ do

        1.  choose $(b_0,b_1) \in P$ and set $P:=P \setminus
                    \{(b_0,b_1)\}$;

        2.  compute a finite complete set ${\mathcal{S}}$ of equivariant $S$-polynomials for $(b_0,b_1)$;

        3.  while ${\mathcal{S}}\neq \emptyset$ do

            1.  choose $f \in {\mathcal{S}}$ and set ${\mathcal{S}}:={\mathcal{S}}\setminus \{f\}$;

            2.  compute a $G$-remainder $r$ of $f$ modulo $B$;

            3.  if $r \neq 0$ then set $B:=B \cup \{r\}$ and $P:=P \cup (B \times r)$;

    3.  return $B$.

Note the order in which $B$ and $P$ are updated: one needs to add $(r,r)$ to $P$, as well. The proof of correctness of this algorithm is straightforward and omitted.

If the partial order $\preceq$ on ${\mathrm{Mon}}$ defined in the introduction does not admit infinite antichains, then the equivariant Buchberger algorithm always terminates. Indeed, suppose that the algorithm would not terminate, and let $r_1,r_2,r_3,\ldots$ be the sequence of remainders 