Theorem § follows from the stronger theorem:

**Theorem 1.3***
The key formulas in Theorems *1, 3, 4* can be derived with a *1*-strategy.
*

As an example of how Theorem above
is stronger than Theorem
§,
we mention
that in defining an idealized strategy, we have often said that
*there exist*
polynomials in the ideal or the user selects certain
polynomials from *the ideal*.
In practice, our implemented operations for automatically
reducing the size of generating sets for polynomial ideals
remove many redundant polynomial equations,
and the user can select from this reduced generating set.
For an example, see
§.
The user has little work to do in making a selection.
In the same spirit as
Theorem 1.3,
the theorem of item 2 of
§
can be derived using a symmetrized 2-strategy.

Note in practice a user can get great benefit from our strategy software when he thinks up a clever (unmotivated) unknown, but we are unable to formalize or analyze this type of intervention, so it plays no role in this paper.

Wed Jul 3 10:27:42 PDT 1996