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.