Solution via a prestrategy

We now apply a prestrategy to see how one might discover the theorem of §subsection:problem.

We run NCProcess1 for 2 iterations where the input is the equations (FAC), together with the declaration of A, B, C as knowns and the remaining variables as unknowns. The file created by NCProcess1 is a list of equations whose solution set is the same as the solution set for the FAC equations. The output is the spreadsheet appearing below. (We added the <=== appearing below after the spreadsheet was created.) The below can be read as an equal sign.

THE ORDER IS NOW THE FOLLOWING:
A < B < C « m « m « n « n « a « b « c « e « f « g

	YOUR SESSION HAS DIGESTED
	THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR:
{a, b, c, e, f, g}
The corresponding rules are the following:

a n A m

b n B

c C m

e n A m

f n B

g C m

	USER CREATIONS APPEAR BELOW

	SOME RELATIONS WHICH APPEAR BELOW
		MAY BE UNDIGESTED

THE FOLLOWING VARIABLES HAVE NOT BEEN SOLVED FOR:
{n, n, m, m}
The expressions with unknown variables {n, m}
and knowns {A, B, C}

n m 1

(1 - m n) A m - (1 - m n) B C m = 0         <===

The expressions with unknown variables {n, m}
and knowns {A}

n m 0

n A m 0

The expressions with unknown variables {n, m}
and knowns {A, B, C}

n m 0

n B C m n A m

The expressions with unknown variables {n, m}
and knowns {}

n m 1

The expressions with unknown variables {n, n, m, m}
and knowns {}

m n 1 - m n                                                 <===

The above ``spreadsheet'' indicates that the unknowns a, b, c, e, f and g are solved for and states their values. The following are facts about the output: (1) there are no equations in 1 unknown, (2) there are 4 categories of equations in 2 unknowns and (3) there is one category of equations in 4 unknowns. A user must observe that the first equation which we marked with <=== becomes an equation in the unknown quantity when multiplied on the right by . This motivates the creation of a new variable P defined by setting

The user may notice at this point that the second equation marked with <=== is an equation in only one unknown quantity once the above assignment has been made and is considered known. These observations lead us to ``select'' (see footnote corresponding to O2 in §) the equations and . Since we selected an equation in and an equation in , it is reasonable to select the the equations , and because they have exactly the same unknowns.

Run NCProcess1 again with § added and declared known as well as A,B and C declared known. The output is:

THE ORDER IS NOW THE FOLLOWING:
A < B < C « m « m « n « n « a « b « c « e « f « g

	YOUR SESSION HAS DIGESTED
	THE FOLLOWING RELATIONS

THE FOLLOWING VARIABLES HAVE BEEN SOLVED FOR:
{a, b, c, e, f, g}
The corresponding rules are the following:

a n A m

b n B

c C m

e n A m

f n B

g C m

The expressions with unknown variables {}
and knowns {A, B, C, P}

P P P

-P A (1 - P)

A P - P A -(1 - P) B C P

	USER CREATIONS APPEAR BELOW

m n P

n m 1

n m 1

m n 1 - m n

	SOME RELATIONS WHICH APPEAR BELOW
		MAY BE UNDIGESTED

THE FOLLOWING VARIABLES HAVE NOT BEEN SOLVED FOR:
{A, B, C, m, m, n, n, P}
The expressions with unknown variables {n, m}
and knowns {P}

m n P

n m 1

The expressions with unknown variables {n, m}
and knowns {P}

m n 1 - P

n m 1

Note that the equations in the above display which are in the undigested section (i.e., below the lowest line of thick black lines) are repeats of those which are in the digested section (i.e., above the lowest line of thick black lines). The symbol indicates that the polynomial equation also appears as a user select on the spreadsheet. We relist these particular equations simply as a convenience. We will see how this helps us in §. Since all equations are digested, we have finished using NCProcess1 (see S3 in §). As we shall see, this output spreadsheet leads directly to the theorem about factoring systems.