By the * finite determinacy theorem*, we may assume that
,
, is a polynomial.
Since
is faithfully flat and all
data will be defined over
, we may replace
by
and, similarly,
by
and
by
for the computation.
With the additional assumption
, all data will be
defined over
, and we can apply methods of computer algebra.
Using standard basis methods for * local rings*,
one can compute a monomial
-basis
of

The matrix of with respect to is defined by . Since , we obtain for

A * reduced normalform* with respect to a * local monomial
ordering* allows to compute the projection to the first summand in

The basis representation of with respect to defined by can be computed inductively by

Using standard basis methods, one can check if and compute a -basis of with

with respect to is