# The Bart-Gohberg-Kaashoek-Van Dooren Theorem: Step 1

## Solution via a prestrategy

We now apply a prestrategy to see how one might discover the theorem. 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. This is done in the Mathematica input file FACStep1.m. The spreadsheet created by NCProcess1 is a list of equations whose solution set is the same as the solution set for the FAC equations. The 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
3. There is one category of equations in 4 unknowns.
The equations to take note of appear below.

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

m n 1 - m n

First notice that the first equation is not written as a rule since it has a collected form. This collect form can be used to assist a person in finding decompositions. A user must observe that this equation becomes an equation in the unknown quantity m n when multiplied on the right by n. This motivates the creation of a new variable P
 P = m n
The user may notice (if the user does not notice it at this point, it will become very obvious with an additional run of NCProcess1) at this point that the second equation above is an equation in only one unknown quantity m n once the above assignment has been made and P is considered known. These observations lead us to ``select'' the equations m n - P and m n - 1 + m n. Since we selected an equation in m n and an equation in m n, it is reasonable to select the the equations n m - 1, and n m - 1 because they have exactly the same unknowns.

Once we have decided on which equations to select, we are ready for step 2.