We saw that this factorization problem could be solved with a 2-prestrategy. It was not a 1-prestrategy because there was at least at one point in the session where the user had to make a decision about an equation in two unknowns. On the other hand, the assignment § was a motivated unknown. We will see in § that this is a 1-strategy. For example, the equation
(3.5)
(1 -
m
n)
A
m
-
(1 -
m
n)
B
C
m
= 0
in the two unknowns
m
and
n
can be transformed
into an equation in the one unknown
m
n
by multiplying
by
n
on the right:
(3.6)
(1 -
m
n)
A
m
n
-
(1 -
m
n)
B
C
m
n
= 0
If we do not restrict ourselves to the original variables but allow constructions of new variables (according to certain very rigid rules), then the factorization problem is solvable using a generalization of a 1-prestrategy, called a 1-strategy. Section § will describe 1-strategies.
The brevity of this presentation in a journal suppresses some of the advantages and some of the difficulties. For example, one might not instantly have all of the insight which leads to the second spreadsheet. In practice, a session in which someone ``discovers'' this theorem might use many spreadsheets. All that matters is that one makes a little bit of progress with each step. Also, since this paper discusses mathematics and does not explain how to use the code, it is not easy to see that there is very little which needs to be typed and that the computer computations are fast. For example, when performing the computations in §, one does not type in the 5 equations of (§). One instead, types in the 2 × 2 block matrix and tells the computer that it is an isometry and that U is unitary.