Summary of a Prestrategy

We have just given the basic ideas. As a prestrategy proceeds, more and more equations are digested by the user and more and more unknowns become knowns. Thus we ultimately have two classes of knowns: original knowns ${\cal K}_0$ and user designated knowns ${\cal K}_U$. Often a theorem can be produced directly from the output by taking as hypotheses the existence of knowns ${\cal K}_U \cup {\cal K}_0$ which are solutions to the equations involving only knowns.

Assume that we have found these solutions. To prove the theorem, that is to construct solutions to the original equations, we must solve the remaining equations. Fortunately, the digested equations often are in a block triangular form which is amenable to backsolving. This is one of the benefits of ``digesting" the equations.

An example, makes all of this more clear.