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.