The digested equations (those in items O1, O2 and O3) often contain the necessary conditions of the desired theorem and the main flow of the proof of the converse. If the starting polynomial equations follow as algebraic consequences of the digested equations, then we should exit the above loop. The starting equations, say , follow as algebraic consequences of the digested equations, say , if and only if the Gröbner Basis generated by reduces (in a standard way) the polynomial to 0 for . Checking whether or not this happens is a purely mechanical process. (See §).
When one exits the above loop, one is presented with the question of how to finish of the proof of the theorem. We shall call the steps required to go from a final spreadsheet to the actual theorem the ``end game''. We shall describe some ``end game'' technique in §. We shall illustrate the ``end game'' in § and §. As we shall see, typically the first step is to run NCProcess2 whose output is a very small set of equations.