Definition of S-polynomial.
Easy theorem: for the reduction algorithm to suffice for determining ideal membership, it had better reduce the S-polynomials to zero, making it a Gröbner basis.
Buchberger's algorithm: when it doesn't, just throw them in as new generators, and repeat until done. The result is a Gröbner basis.
Theorems to be proven: the converse of that easy theorem (Buchberger's criterion), and the fact that Buchberger's algorithm terminates.
