.
Also, more and more unknowns
become knowns.
Thus
we ultimately have two classes of knowns:
original knowns 
and user designated knowns 
.
Often
prominent in the statement of a theorem
is the subset 
of consisting of
equations involving only knowns
.
Indeed many classical theorems (at least the ones we present here) have the form:
the equations in C have a solution if and only if the equations in
Now the ``only if'' part of this is clear from the derivation using a strategy,
but proving the ``if'' part is a less precise process.
Proving the ''if'' part is the business of what we call
the ``end game'',
which is the act of using the last spreadsheet generated
during a prestrategy to write down a theorem and its proof.
Clearly one of the first steps is to
translate the equations on the spreadsheet into palatable language.
For example, if one obtains the equation 
and
and 
, then one would say that P
is a projection. A slightly more complicated example would be
if 
where
, 
, 
and Y are invertible and
and was self-adjoint. If
and X were in 
, then one could say
that 
would have to be both symmetric
and invertible.
When one performs the
approach of the above paragraph to obtain the ``if''
part of the theorem,
one tries
to record enough necessary
conditions so that the conditions are also sufficient.
Once
such conditions (in the form of polynomial equations)
are selected from the
spreadsheet
,
then one assumes that each of these equations hold
for certain unspecified values of the knowns (those
variables in )
and tries to find values for the remaining variables such that
each of the equations on the final spreadsheet holds.
If one can find values for these remaining variables, then,
since each of the equations of the final spreadsheet
holds, each of the equations on the initial spreadsheet holds
and one has proven the desired ``if'' part of the theorem.
Fortunately,
the spreadsheet often has
a block triangular form which is amenable to backsolving.
One of the benefits of putting the equations
in categories is that this reveals this triangular structure (see
§).
These ``end game'' techniques are demonstrated in § and §.