(Univariate) Ore polynomial rings have a Euclidean algorithm. This is implemented in the following routines: skew_pdiv, skew_prem, skew_gcdex, and skew_elim. An extension to the multivariate case is available through Groebner bases computations (see Groebner and in particular Groebner[Basis] and Groebner[Reduce]).

Here we show how the package can be used to derive a proof of the Reed-Dawson identity:

is

for even  and  for odd .

Let us introduce an algebra of linear recurrence operators in  and .  and  denote the shift operators in  and , respectively.

We compute first-order recurrences satisfied by the summand (which we denote by ).

We eliminate  between these operators by computing their greatest common right divisor.

The factor  corresponds to taking a finite difference. Definite summation for  over all integers yields a telescoping series that collapses to 0. We therefore get:

Therefore, the sum  satisfies

Now, the announced result follows from the initial conditions:

For ,

so that  for odd .

For ,

so that  is given by

which is .

Here we derive contiguity relations for the Gauss hypergeometric function.  This function is known to Maple as:

It is  for

When considering the summand, we introduce the following algebra:

The bivariate sequence  vanishes at both of the following operators:

(General algorithms exist to find such operators.)

From the previous first-order recurrences, we derive relations on  in the mixed differential difference algebra.

The equations are obtained by multiplication of the recurrences by , followed by summation over all non-negative . Formally, this corresponds to changing  into  and  into .

Therefore, we set

The linear differential operator  is called a step-up operator. It relates the forward shift of  to derivatives of  by the following equation.

The elimination of  between this step-up operator and the differential equation yields a contiguity relation for --a purely recurrence equation. It is obtained by the extended skew gcd algorithm:

In other words, the Gauss hypergeometric function satisfies the following equation:

More interestingly, the extended Euclidean algorithm yields a step-down operator for  - a relation between an inverse shift of  and its derivatives. This is obtained by computing an inverse of  modulo .

From this result, we have  and .  In particular,

is the step-down operator: