We solve a system in 3 variables and 3 unknowns
Its triangular decomposition consists of only one regular chain
The polynomial in x is not normalized
Indeed its initial is not a constant in R
We compute the inverse of the initial of px w.r.t. rc Note that the Inverse will not fail if its first argument is not invertible w.r.t. its second one; computations will split if a zero-divisor is met. This explains the non-trivial signature of the Inverse function
We get the inverse the initial of px w.r.t. rc
We multiply px by the inverse of its initial and reduce the product w.r.t rc. The returned polynomial is now normalized w.r.t. rc. Note that only the polynomials of rc in y and z are used during this reduction process.