The BartGohbergKaashoekVan 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:
 There are no equations in 1 unknown,
 There are 4 categories
of equations in 2 unknowns
 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
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.