%-----------------BEGIN OF LATEX-FILE--------------------------------
\documentstyle {article}
\setlength{\topmargin}{-1cm}
\setlength{\headheight}{1.5cm}
\setlength{\headsep}{0.3cm}
\setlength{\textheight}{23.5cm}
\setlength{\oddsidemargin}{0.5cm}
\setlength{\evensidemargin}{0.5cm}
\setlength{\textwidth}{15cm}
\pagestyle{myheadings}
\markright{\sc the electronic journal of combinatorics 1
(1994), \# R10\hfill}
\thispagestyle{empty}
\title{Short and Easy Computer Proofs
of the Rogers-Ramanujan Identities
and of Identities of Similar Type}
\author{Peter Paule\thanks{Supported in part by
grant P7220 of the Austrian FWF} \\
Research Institute for Symbolic Computation \\
Johannes Kepler University Linz \\
A--4040 Linz, Austria \\
{\tt Peter.Paule@risc.uni-linz.ac.at}}
\date{Submitted: July 15, 1994; Accepted: July 26, 1994.}
\begin{document}
\maketitle
%\def\qchoose#1 #2{\bigl[ {#1 \atop #2} \bigr]}
\def\defeq{\mathrel{:=}} % "defined as equal to"
\newtheorem{th}{Theorem}
%\begin{description}
\begin{abstract}
%\noindent
New short and easy computer proofs of finite versions
of the Rogers-Ramanujan identities and of similar type
are given. These include a very short proof of the first
Rogers-Ramanujan identity that was missed by computers,
and a new proof of the
well-known quintuple product identity by
creative telescoping.
\end{abstract}
\medskip
{\bf AMS Subject Classification.} 05A19; secondary 11B65, 05A17
\section{Introduction}
The celebrated Rogers-Ramanujan identities stated as
series-product identities are
\begin{eqnarray}
\label{rr}
1+\sum_{k=1}^\infty {q^{k^2+a k}\over
(1-q)(1-q^2)\cdots (1-q^k)}=
\prod_{j=0}^\infty {1\over (1-q^{5j+a+1})(1-q^{5j-a+4})}
\end{eqnarray}
where $a=0$ or $a=1$, see e.g. Andrews \cite{top} which
also contains a brief historical account.
It is well-known that number theoretic identities
like these, or of similar type, can be deduced as
limiting cases of $q$-hypergeometric finite-sum
identities.
Due to recent algorithmic breakthroughs, see for instance
Zeilberger \cite{holo}, or,
Wilf and Zeilberger \cite{wz}, {\it proving} these
finite versions becomes more and more routine
work that can be left to the computer.
For instance,
the computers Ekhad and Tre \cite{ekhad} delivered
a purely verification proof of the
following finite version, which
was stated first in this form by Andrews \cite{siam prob},
see also Bressoud \cite{siam sol}.
\begin{eqnarray}
\label{watson-andrews}
\sum_k {q^{k^2} \over (q;q)_k (q;q)_{n-k}}=
\sum_k {(-1)^k q^{(5k^2-k)/2} \over
(q;q)_{n-k} (q;q)_{n+k}},
\end{eqnarray}
where $(a;q)_n=(1-a)(1-a q)\cdots (1-a q^{n-1})$
for $n\geq 1$, $(a;q)_0=1$, and $1/(q;q)_n=0$ for
$n<0$. In the limit $n\rightarrow \infty$ one gets
identity (\ref{rr}) with $a=0$, after applying
Jacobi's triple product identity, see section 5.1.
It is evident that the hard part of deducing,
for instance,
the Rogers-Ra\-ma\-nu\-jan identities as a limiting
case of a finite version
consists in {\it finding} such a representation.
On the other hand, it is to expect that
automated {\it proving} will enlarge the
heuristic toolbox in a significant way.
Nevertheless, in this
paper we do not intend to enter the recent
discussion on the r\^{o}le of computer proofs,
which was stimulated by Zeilberger \cite{saviour},
see also Andrews' rebuttal \cite{rebuttal}.
The objective of this paper is to show that for
classical Rogers-Ramanujan type identities,
computers are able to produce "nice" proofs, i.e.
not kind of Byzantine computer output a human
usually is unwilling, or even unable, to verify.
In the particular situations of this article it turns
out that even the computer-constructed proof certificates
are amenable to human verification.
%More precisely, these are proofs,
%or $q$WZ-certificates (see section 2),
%that are not only simple in logical structure,
%but also easy to check for a human with respect
%to the computational steps needed for verification.
%The logical simplicity amounts to the fact that
%ODER: "easy to check"
%but also of {\it human size}. By "human size"
%we mean that all computational steps needed
%to verify the computer proof can be carried out
%by hand without too much pain in a reasonable
%amount of time.
The paper is organized as follows. In section 2
we are going to specify our use of the notion
"computer proof". A computer proof of
a $q$-hypergeometric identity will be understood
as a proof by $q$WZ-certification, based on
the method of creative telescoping.
In section 3 we present a new "very short"
$q$WZ-certification proof of (\ref{watson-andrews})
that was missed by the computers
Ekhad and Tre \cite{ekhad}.
In section 4 we provide the $q$WZ-certificate
of another finite Rogers-Ra\-ma\-nu\-jan version
due to Andrews \cite{finite} and which originates
in the work of Schur \cite{schur}, who
independently discovered (\ref{rr}).
As briefly indicated in section 4,
this finite version plays an outstanding r\^ole
for certain applications in physics.
Besides the versions given in Andrews \cite{triple},
all known finite Rogers-Ramanujan type identities deliver
the product-side only after applying expansion formulas
like the triple or the quintuple product identities.
In section 5, for sake of completeness,
$q$WZ-certificates
of corresponding finite versions are presented.
%as well as of Rogers-Ramanujan type
%identities due to Goellnitz-Gordon and
%Rogers-Selberg.
In section 6 we briefly comment on the newly developed
computer program we used to find the proof certificates
in this paper.
\section{$q$WZ-certification}
Analogous to the algorithm presented by Zeilberger \cite{fast},
the computer program we used takes terminating $q$-hypergeometric
sums as input. Its output is a linear recurrence that is satisfied
by the input sum, together with a rational function serving as
a proof certificate. As made explicit in this section, verifying
the recurrence is equivalent to checking a rational function
identity.
Let $f:=(f_{n,k})$ be
a double-indexed sequence with values in a
suitable (e.g. computable) ground-field $F$ containing
the rational number field and $q$. In the following
we consider $q$ as an indeterminate, which could be
specialized to a nonzero complex number
(with $|q|<1$ for limit considerations).
We shall consider
only sequences where $n$ runs through the nonnegative
integers, whereas the second parameter
$k$ might run through all integers.
The sequence $f$ is called $q$-hypergeometric in both
parameters if both quotients
\[
{f_{n,k}\over f_{n-1,k}} \hbox{\ \ and\ \ }
{f_{n,k}\over f_{n,k-1}}
\]
are rational functions in $q^n$ and $q^k$ over $F$
for all $n$ and $k$ where the quotients are
well-defined.
For instance, if $[l]\defeq (1-q^l)/(1-q)$ for integer $l$,
and
\[
{n\brack k}\defeq\cases{\displaystyle
{\prod_{l=1}^k {[n-l+1]\over [l]}}
&, if $0\le k\le n$\cr
0 &, otherwise\cr}
\]
are the Gaussian polynomials, then
\[
{n+1\brack k+1}/{n\brack k+1}={1-q^{n+1}\over 1-q^{n-k}}
\hbox{\ \ and\ \ }
{n+1\brack k+1}/{n+1\brack k}={1-q^{n-k+1}\over 1-q^{k+1}}.
\]
For $q=1$ (resp. $q\rightarrow 1$) the Gaussian
polynomial ${n\brack k}$ turns into ${n\choose k}$, the ordinary
binomial coefficient.
We say the sequence $f$ has finite support with respect
to $k$, if the following is true for each $n$ fixed:
$f_{n,k}\neq 0$ for all $k$ from a finite integer interval $I_n$,
and $f_{n,k}=0$ for all $k$ outside $I_n$. A simple example
for such a sequence is provided by
$f_{n,k}:={n\brack k}$ where $I_n=\{0,1,\ldots,n\}$.
Given a sequence $(f_{n,k})$ being $q$-hypergeometric
in both parameters and having finite support with
respect to $k$.
For nonnegative integer $n$
define $S_n:=\sum_k f_{n,k}$, a finite sum due to
finite support property.
We use the convention that the summation
parameter $k$ runs through all the integers, in case the
summation range is not specified explicitly.
Alternatively, the sequence $S:=(S_n)$ can be represented
in terms of a recursion of some order $d$. For instance,
as the unique solution of the recurrence
\begin{eqnarray}
\label{rec}
c_0(n) S_n + c_1(n) S_{n-1} + \cdots + c_d(n) S_{n-d} = 0
\end{eqnarray}
for $n\geq d$, with certain coefficients $c_i(n)$,
$c_0(n)\neq 0$, and with respect to the
initial values $S_0, S_1, \ldots, S_{d-1}$.
Equivalently,
the annihilating operator
\begin{eqnarray}
%\label{}
A_S(N):= \sum_{l=0}^d c_l(n) N^{-l},
\end{eqnarray}
where $N$ denotes the shift-operator
with respect to $n$,
together with the $d$ initial values represent $S$
in a unique way.
%{\it Remark:} If the coefficients $c_l(n)$ are polynomials
%in $n$, Stanley \cite{stan} calls $(S_n)$ P-recursive.
Let $f$ and $S$ be as above, then the $q$WZ-certificate of the
annihilating operator is by definition a
rational function $cert_S(n,k)$,
rational in $q^n$ and $q^k$,
such that
\begin{eqnarray}
\label{telescop}
A_S(N) f_{n,k} = g_{n,k}-g_{n,k-1}
\end{eqnarray}
where
\begin{eqnarray}
%\label{}
g_{n,k}:= cert_S(n,k)\ f_{n,k}.
\end{eqnarray}
We shall use this type of certification
following Wilf's and Zeilberger's paradigm of "creative
telescoping", see e.g \cite{creative}, \cite{qwz}
or \cite{wz}. Namely,
given $S$ in sum representation as above,
the $q$WZ-certificate contains all information
necessary
to prove that $S$ satisfies the homogeneous
recursion described by the operator $A_S(N)$.
This is true, because summing (\ref{telescop})
over sufficiently many $k$, i.e. over an integer
interval containing the finite support such that
the bounds evaluate to zero,
immediately implies (\ref{rec}).
Thus what is left is to verify (\ref{telescop}).
But this is equivalent to checking a {\it rational
function identity}, i.e.
\begin{eqnarray}
\label{ratid}
r(n,k)=cert_S(n,k)-cert_S(n,k-1){f_{n,k-1}\over f_{n,k}}
\end{eqnarray}
where $r(n,k)$, rational in $q^n$ and $q^k$,
comes from
\[
A_S(N) f_{n,k}=r(n,k)\ f_{n,k}.
\]
%Here one uses that $f_{n,k}$ is $q$-hypergeometric
%in $n$.
The actual computation of $r(n,k)$ is straightforward
from rewriting the $N^{-l}$ actions as rational function
multiples of $f_{n,k}$, i.e.
\[
N^{-1} f_{n,k} = {f_{n-1,k} \over f_{n,k}} f_{n,k},
\hbox{\ \ }
N^{-2} f_{n,k} = {f_{n-2,k} \over f_{n-1,k}}
{f_{n-1,k} \over f_{n,k}} f_{n,k},
\hbox{\ a.s.o. }
\]
\section{A Computer Proof that was Missed by Computers}
Ekhad and Tre \cite{ekhad} gave a $q$WZ-certification
proof of (\ref{watson-andrews})
by showing that both sides
are solutions of a certain {\it fifth} order linear
recurrence equation. More precisely, they showed
that the left hand side is annihilated by a recurrence
operator of order two,
whereas the right hand side by a fifth order multiple
of that operator. What Ekhad and Tre missed
observing is that {\it both} sides
of a slight variation of the original form
of identity (\ref{watson-andrews})
satisfy indeed the same recurrence of order {\it two}.
This variation makes use of the summand's symmetry.
It consists in introducing an extra factor
$1+q^k$ in the summand of the right hand side,
which,
because of symmetry in $k$ and $-k$,
amounts to the same as multiplying the sum by 2.
This is made more transparent if we look at the
decomposition of the summand $f(k)$ into its even and
its odd part, in the usual way,
\[
f(k)=f_e(k)+f_o(k)={f(k)+f(-k)\over 2} + {f(k)-f(-k)\over 2}.
\]
Summing over all integers the sum of the odd parts obviously
vanishes and it is true that
\[
\sum_k f(k) = \sum_k f_e(k) = \sum_k {f(k)+f(-k)\over 2}.
\]
\begin{th}
For nonnegative integers $n$:
\begin{eqnarray}
\label{pp-watson}
\sum_k {2 q^{k^2} \over (q;q)_k (q;q)_{n-k}}=
\sum_k {(-1)^k (1+q^k) q^{(5k^2-k)/2} \over
(q;q)_{n-k} (q;q)_{n+k}}.
\end{eqnarray}
In addition, both sides are annihilated
by
\begin{eqnarray}
\label{pp-watson op}
A(N):= (1-q^n) N^0-(1+q-q^n +q^{2n-1})N^{-1}+q N^{-2}.
\end{eqnarray}
\end{th}
{\it Proof:} Denote the left hand side of (\ref{pp-watson})
by $L(n)$, the right hand side by $R(n)$.
Since the initial values coincide,
\begin{eqnarray}
L(0)=R(0)=2 \hbox{\ \ and \ \ }
L(1)=R(1)=2 {1+q\over 1-q},
\end{eqnarray}
it suffices to prove that both sides are annihilated by
$A(N)$.
But this follows, as explained in section 2,
from the corresponding $q$WZ-cer\-ti\-fi\-ca\-tes:
\begin{eqnarray}
cert_L (n,k) = -q^{2n-1} (1-q^{n-k})
%{ (1-q^{n-k})\over (1-q^n) }
\end{eqnarray}
and
\begin{eqnarray}
cert_R (n,k) = {q^{2n+3k}\over 1+q^k} (1-q^{n-k}).
%{ (1-q^{n-k})\over (1-q^n) }.
\end{eqnarray}
{\it Remark:} We want to point out that all computational
steps needed to verify the proof are indeed of "human" size, i.e.
they can be carried out
by hand without too much pain in a reasonable
amount of time.
(The verification of this statement is left to the reader.)
\vskip 0.3cm
From a $q$-hypergeometric
point of view (\ref{watson-andrews}) is a
terminating special instance of Watson's $q$-analogue
of Whipple's theorem, see e.g. Gasper and Rahman
\cite{GR}, (III.18).
The successful variation, i.e. the
idea of introducing the extra factor $1+q^k$,
stems from the (human) author's study,
in interaction with the computer,
of various
terminating cases of Watson's $q$-analogue.
The introduction of the extra factor $1+q^k$ or,
more generally, summing the even part
turns out to be crucial for boiling down $q$WZ-certificates
of many more finite identities of similar type.
More precisely, in these instances the telescoping
equation (\ref{telescop}) finds a solution for an
annihilating operator of smaller degree than for
the original summand.
For example:
\begin{itemize}
\item Without introducing the extra symmetry factor $1+q^{-k}$,
the right hand side of (1.1) in Bressoud \cite{bress},
another finite version of (\ref{rr}, $a=0$),
has minimal recursion order 5, instead of 2,
with respect to $q$WZ-certification. Analogous observations
hold for all other finite versions
of Rogers-Ramanujan type identities
presented in \cite{bress}.
\item Without introducing the extra symmetry factor $1+q^{2k}$,
the left hand side of (55) in Paule \cite{paule},
a finite version of a Goellnitz-Gordon identity,
has minimal recursion order 4, instead of 2,
with respect to $q$WZ-certification.
\item Without introducing the extra symmetry factor $1+q^k$,
the left hand side of (48) in Paule \cite{paule},
a finite version of a Rogers-Selberg identity,
has minimal recursion order 7 (!), instead of 3,
with respect to $q$WZ-certification.
\end{itemize}
\section{The Andrews-Schur Identity}
As observed by Andrews \cite{finite},
the following {\it polynomial} identity for $a=0$
and $a=1$ immediately implies (\ref{rr})
by taking $n \rightarrow \infty$ and using
Jacobi's triple product identity (see the next section).
\begin{eqnarray}
\label{andrews-schur}
\lefteqn{\sum_{k=0}^n q^{k^2+a k}
{2n-k+a\brack k} = }\\
& &\sum_{k=-\infty}^\infty q^{10k^2+(4a-1)k}
{2n+2a+2\brack n-5k}
{[10k+2a+2]\over [2n+2a+2]}.\nonumber
\end{eqnarray}
(This corresponds to $\alpha = 0$ and $n\rightarrow 2n-1$, or,
$\alpha = -1$ and $n\rightarrow 2n$ in the theorem
of \cite{finite}, cf. also (3.10) and (3.12) in
Andrews \cite{triple}.)
As pointed out by Andrews \cite{finite}, this finite
version of (\ref{rr}) has its origin in the
work of Schur \cite{schur}. The importance of (\ref{andrews-schur})
comes from the fact that it describes $q\rightarrow q^{-1}$
duality of regimes of R.J. Baxter's solution to the hard
hexagon model of statistical mechanics, see e.g.
Andrews \cite{hh} or \cite{q-series}.
With respect to creative telescoping
it turns out that the following reciprocal
variant of (\ref{andrews-schur}) finds nicer
$q$WZ-certificates than the identity in
its original form.
\begin{th}
For $a=0$ or $a=1$:
\begin{eqnarray}
\label{a-s-finite}
\sum_{k=-\lfloor a/2 \rfloor}^n q^{k^2+2ak} {n+k+a\brack n-k}=
\sum_{k=-\lfloor (n+2a+2)/5 \rfloor}^{\lfloor n/5 \rfloor}
q^{15k^2 + (6a+1)k} {2n+2a+2 \brack n-5k}
{[10k+2a+2]\over [2n+2a+2]}.
\end{eqnarray}
\end{th}
{\it Proof:} Denote the left hand side of (\ref{a-s-finite})
by $L^{(a)}(n)$, the right hand side by $R^{(a)}(n)$.
In view of
\begin{eqnarray}
\label{initial}
L^{(a)}(0)=R^{(a)}(0)=1 \hbox{\ \ and \ \ }
L^{(a)}(1)=R^{(a)}(1)=[a+1]+q^{2a+1}
\end{eqnarray}
it suffices to prove that both sides are annihilated by
\begin{eqnarray}
\label{annihil}
A^{(a)}(N):= N^0-(1+q+q^{2n+2a-1})N^{-1}+qN^{-2}.
\end{eqnarray}
But this follows, as explained in section 2,
from the corresponding $q$WZ-cer\-ti\-fi\-ca\-tes:
\begin{eqnarray}
\label{L-cert}
cert_{L^{(a)}}(n,k) = -q^{2n+2a-1} {[n-k]\over [n+k+a]}
\end{eqnarray}
and
\begin{eqnarray}
\label{R-cert}
\lefteqn{cert_{R^{(a)}}(n,k) = -q^{2n+20k+6(a+1)} }\\
& & {[n-5k-4][n-5k-3][n-5k-2][n-5k-1][n-5k]\over
[10k+2a+2][2n+2a-2][2n+2a-1][2n+2a][2n+2a+1]}
\nonumber.
\end{eqnarray}
{\it Remark:}
%We want to point out that all computational
%steps needed to verify the proof are of human size, i.e.
%can be carried out by hand without too much pain. (The
%verification of this statement is left to the reader.)
(i) It is interesting to note that both sides of (\ref{a-s-finite})
are annihilated by the same operator (\ref{annihil})
{\it for all} nonnegative integers $a$. But only for the specific choices
$a=0$ or $a=1$ the initial values of the sums match.
(ii) For combinatorial interpretations of the finite sums
arising in (\ref{andrews-schur}) and (\ref{a-s-finite}) see,
for instance, Agarwal and Andrews \cite{hook}.
\vskip 0.3cm
%The duality of (\ref{andrews-schur}) and (\ref{a-s-finite})
%is made explicit as follows.
Identity (\ref{a-s-finite}) is the reciprocal dual of
(\ref{andrews-schur}).
This can be seen, for instance, as follows.
On the left hand side of (\ref{andrews-schur})
reverse the order of summation, i.e. $k\rightarrow n-k$.
The rest follows immediately by $q\rightarrow q^{-1}$
using the well-known fact that Gaussian
polynomials are reciprocal, i.e.
\[
{n\brack m}_{q\rightarrow q^{-1}} =
q^{m(m-n)} {n\brack m}.
\]
In concluding this section we note that,
in contrast to other finite versions of (\ref{rr}),
the Andrews-Schur identity finds a nontrivial
specialization for $q=1$.
Namely, for
$q=1$ both identities (\ref{andrews-schur}) and (\ref{a-s-finite})
turn into the binomial identity ($a=0$ or $a=1$)
\begin{eqnarray}
\label{q=1}
\sum_{k=-\lfloor a/2 \rfloor}^n {n+k+a\choose n-k} =
\sum_{k=-\lfloor (n+2a+2)/5 \rfloor}^{\lfloor n/5 \rfloor}
{2n+2a+2 \choose n-5k} {5k+a+1 \over n+a+1}.
\end{eqnarray}
For $a=0$ (resp. $a=1$) this corresponds to two different
binomial sum representations of the even (resp. odd)
Fibonacci numbers. That can be seen, for instance,
directly from the defining recursion (\ref{annihil}) for
$q=1$, and the first two initial values. For integer $a>1$
identity (\ref{q=1}) results in nice Fibonacci relations
which group together mod 5. More precisely, let $l(n,a)$
(resp. $r(n,a)$)
denote the left (resp. right) side of (\ref{q=1}) and let
$(F(k))_{k\geq 0}$ be the Fibonacci sequence with $F(0)=F(1)=1$.
Then for all nonnegative integers $a,m,n$ we have $l(n,a)=F(2n+a)$
and $r(n,5m)=F(10m+2n)$, $r(n,5m+1)=F(10m+2n+1)$,
$r(n,5m+2)=-F(10m+2n+3)$, $r(n,5m+3)=-F(10m+2n+6)$, and
$r(n,5m+4)=0$.
\section{Triple and Quintuple Product Expansions}
Besides those ones given in Andrews \cite{triple},
all known finite Rogers-Ramanujan type identities deliver
the product-side only after applying expansion formulas
like the triple or the quintuple product identities.
For sake of completeness, we present
$q$WZ-certificates of corresponding finite versions.
Version (\ref{quintuple-finite}) for the
quintuple product identity
seems to be stated the first time
in this form.
\subsection{Jacobi's Triple Product Identity}
It is well-known, see e.g. Andrews \cite{top}, that
Jacobi's triple product identity
\begin{eqnarray}
\label{jacobi}
\sum_{k=-\infty}^\infty q^{k\choose 2} x^k =
\prod_{j=1}^\infty (1-q^j)(1+x^{-1} q^j)(1+x q^{j-1})
\end{eqnarray}
can be deduced, for instance, as a limiting case
$n\rightarrow \infty$ of the following finite variant
of the $q$-binomial theorem.
\begin{th}
For nonnegative integers $n$ and $x\neq 0$:
\begin{eqnarray}
\label{jacobi-finite}
\sum_k {2n \brack n+k} q^{k\choose 2} x^k =
(-x^{-1} q;q)_n (-x;q)_n.
\end{eqnarray}
In addition, both sides are annihilated by
\begin{eqnarray}
\label{jacobi op}
A(N)=N^0-(1+x^{-1} q^n)(1+x q^{n-1})N^{-1}.
\end{eqnarray}
\end{th}
{\it Proof:} Denote the sum by $L(n)$.
It suffices to prove that both
sides of (\ref{jacobi-finite}) evaluate to 1 for
$n=0$, and are annihilated by $A(N)$.
The nontrivial part follows, as explained in section 2,
from the corresponding $q$WZ-certificate:
\begin{eqnarray}
\label{jacobi cert}
cert_L (n,k)=q^{n-1}
{[n-k](q^{k+1}[n-k-1]-x[n+k])\over
[2n-1][2n]}.
\end{eqnarray}
{\it Application:}
It is easy to see that in the limit $n\rightarrow \infty$
the left hand side of (\ref{andrews-schur}) tends to
the left hand side of (\ref{rr}), whereas the right hand
side tends to
\begin{eqnarray}
%\label{}
{1\over (q;q)_\infty}
\sum_{k=-\infty}^\infty q^{10k^2 +(4a-1)k} (1-q^{10k+2a+2}),
\end{eqnarray}
where $(a;q)_\infty= \prod_{j=0}^\infty (1-a q^j)$.
This can be rewritten as
\begin{eqnarray}
%\label{}
{1\over (q;q)_\infty}
\sum_{k=-\infty}^\infty (-1)^k q^{(5 k^2 +(4a-1)k)/2},
\end{eqnarray}
which turns into the product side of (\ref{rr})
after applying (\ref{jacobi}) with
$q\rightarrow q^5$ and $x\rightarrow -q^{2a+2}$.
\subsection{The Quintuple Product Identity}
A standard form of the quintuple identity reads as
($z\neq 0$):
\begin{eqnarray}
\label{quintuple}
\lefteqn{ \sum_{k=-\infty}^\infty (-1)^k q^{(3k^2-k)/2} z^{3k} (1+z q^k)=} \\
& &\prod_{j=1}^\infty (1-q^j)(1+z^{-1} q^j)(1+z q^{j-1})
(1+z^{-2} q^{2j-1})(1+z^2 q^{2j-1}), \nonumber
\end{eqnarray}
see, for instance, Gasper and Rahman \cite{GR} (Ex. 5.6, together
with the references).
Again we prove (\ref{quintuple}) as a limiting case.
\begin{th}
For nonnegative integers $n$ and $w\neq 0$:
\begin{eqnarray}
\label{quintuple-finite}
\sum_k (-1)^k q^{(3k^2+k)/2} w^{3k} {2n\brack n+k}
{1-w^2 q^{2k+1}\over (w^{-2};q)_{n-k} (w^2 q^2;q)_{n+k}} =\\
{1-w^2 q\over (w^{-1};q)_n (w q;q)_n}. \nonumber
\end{eqnarray}
In addition, both sides are annihilated by
\begin{eqnarray}
\label{quintuple op}
A(N)=N^0-(1-w^{-1} q^{n-1})^{-1} (1-w q^n)^{-1} N^{-1}.
\end{eqnarray}
\end{th}
{\it Proof:} Denote the sum by $L(n)$, which is defined
over a $q$-hypergeometric summand sequence having finite
support with respect to $k$.
It suffices to prove that both
sides of (\ref{quintuple-finite}) evaluate to
$1-w^2 q$ for
$n=0$, and are annihilated by $A(N)$.
The nontrivial part follows, as explained in section 2,
from the corresponding $q$WZ-certificate:
%-------volker new begin----------------------------------
\begin{minipage}{12cm}
\begin{eqnarray*}
\label{quintuple cert 2nd}
cert_L (n,k)&=& w q^{n+2k}
{(1-w^{-2} q^{n-k-1})(1-w q^{k+1})\over
{(1-w^{-1} q^{n-1})(1-w^2 q^{2k+1})(1-w q^n)}} \times\\
&& {[n-k] ([n-k-1] -w q^n [2n-1] +w^2 q [n+k])\over
[2n] [2n-1]}.
\end{eqnarray*}
\end{minipage}
\hfill
\parbox{1cm}
{\begin{eqnarray}
\end{eqnarray}}
%-------volker new end----------------------------------
%\parbox{10cm}
%{\begin{eqnarray*}
%\label{quintuple cert}
%cert_L (n,k)=&& w q^{n+2k}
% {(1-w^{-2} q^{n-k-1})(1-w q^{k+1})\over
% {(1-w^{-1} q^{n-1})(1-w^2 q^{2k+1})(1-w q^n)}} \times\\
% && {[n-k] ([n-k-1] -w q^n [2n-1] +w^2 q [n+k])\over
%[2n] [2n-1]}.
%\end{eqnarray*}}
%\hfill
%\parbox{1cm}
%{\begin{eqnarray}
%\end{eqnarray}}
For $n\rightarrow \infty$ in (\ref{quintuple-finite})
we get the identity, first stated by G.N. Watson,
\begin{eqnarray}
\label{quintuple-watson}
\sum_k (-1)^k q^{(3k^2+k)/2} w^{3k} (1-w^2 q^{2k+1})=
{(q;q)_\infty (w^{-2};q)_\infty (w^2 q;q)_\infty \over
(w^{-1};q)_\infty (w q;q)_\infty},
\end{eqnarray}
which is easily seen to
be equivalent to (\ref{quintuple}).
{\it Remark:} Identity (\ref{quintuple-finite}) is a
a terminating version of a very-well-poised
$_6 \psi_6$ identity due to W.N. Bailey. We derived
it following Andrews' proof of (\ref{quintuple}) given
in \cite{appl}.
{\it Application:} Taking the limit $n\rightarrow \infty$
in (\ref{quintuple}) and
applying the quintuple product identity
to the right hand side series
\begin{eqnarray}
{1\over (q;q)_\infty}
\sum_{k=-\infty}^\infty q^{15 k^2 +(6a+1)k} (1-q^{10k+2a+2}),
\end{eqnarray}
the reciprocal Andrews-Schur identity (\ref{a-s-finite})
becomes ($a=0$ or $a=1$)
\begin{eqnarray}
\label{rogers}
\sum_{k=0}^\infty {q^{k^2 +2a k}\over (q;q)_{2k+a}} =
\prod_{j=0}^\infty {1\over (1-q^{2j+1})
(1-q^{20j+4a+4})(1-q^{20j-4a+16})}.
\end{eqnarray}
These are identities due to L.J. Rogers, see e.g.
Agarwal and Andrews \cite{hook}.
\section{Conclusion}
All $q$WZ-certificates presented in this paper
have been found by a computer program
which is
a $q$-analogue of Zeilberger's "fast" algorithm
for proving terminating hypergeometric identities,
see Zeilberger \cite{fast}. The program is written
in Mathematica by Riese \cite{riese}. The algorithmic
backbone of the program is a $q$-analogue
of Gosper's algorithm \cite{gosper}, see also
Graham, Knuth and Patashnik \cite{gkp},
based
on recent work of the author \cite{gff}.
After completion
the program will be available upon request.
Riese's package is not the first implementation of a $q$-analogue
of Zeilberger's "fast" algorithm. There are Maple programs written
by Zeilberger, cf. \cite{ekhad}, and
Koornwinder \cite{koorn}. In \cite{koorn}, one can also find
a rigorous description of the algorithmic background of
Koornwinder's implementation.
We want to conclude with a short example concerning
the performance of Riese's program.
With respect to Watson's $q$-analogue
of Whipple's theorem, see e.g. Gasper and Rahman
\cite{GR} (III.18), Ekhad and Tre \cite{ekhad}
remarked that their memories did not suffice for
coming up with a $q$WZ-certification proof.
With Riese's program one needs approximately
10 minutes on an Apollo 4500 workstation
for obtaining the certificates (of order 2)
of both sides. The $q$WZ-certificates presented
in this paper are obtained in about 60 seconds or less.
A more detailed discussion of algorithmic background,
performance, and examples will be given in paper
by the author and Riese \cite{pp-riese}.
\bigskip
\noindent
{\bf Acknowledgment}: The author thanks Volker Strehl,
Herb Wilf and Doron Zeilberger for valuable suggestions
and comments.
%-------------------------------------------------
\begin{thebibliography}{80}
\bibitem{hook} A.K. Agarwal and G.E. Andrews, {\em Hook
differences and lattice paths}, J. Stat. Planning and
Inference, {\bf 14} (1986), 5--14.
\bibitem{finite} G.E. Andrews, {\em A polynomial identity
which implies the Rogers-Ramanujan Identities}, Scripta. Math.,
28 (1970), 297--305.
\bibitem{siam prob} G.E. Andrews, {\em Problem 74-12}, SIAM Rev.,
{\bf 16} (1974), 390.
\bibitem{appl} G.E. Andrews, {\em Applications of basic
hypergeometric functions}, SIAM Rev., {\bf 16} (1974), 441-484.
\bibitem{hh} G.E. Andrews, {\em The hard-hexagon model and
Rogers-Ramanujan type identities}, Proc. Natl. Acad. Sci. USA,
{\bf 78} (1981), 5290--5292.
\bibitem{top} G.E. Andrews, {\em The Theory of Partitions},
Encyclopedia of Mathematics and its Applications Vol.2,
G.-C. Rota ed., Addison-Wesley, Reading, 1976 (Reissued:
Cambridge University Press, London and New York, 1985).
\bibitem{q-series} G.E. Andrews, {\em q-Series: Their
Development and Application in Analysis, Number Theory,
Combinatorics, Physics, and Computer Algebra}, CBMS
Regional Conference Series, No. 66, American. Math. Soc.,
Providence, 1986.
\bibitem{triple} G.E. Andrews, {\em The Rogers-Ramanujan
identities without Jacobi's triple product}, Rocky Mountain J.
Math., {\bf 17} (1987), 659--672.
\bibitem{rebuttal} G.E. Andrews, {\em The death of proof?
Semi-rigorous mathematics? You've got to be kidding!},
Math. Intelligencer, to appear.
\bibitem{siam sol} D.M. Bressoud, {\em Solution of Problem 74-12},
SIAM Rev., {\bf 23} (1981), 101--104.
\bibitem{bress} D.M. Bressoud, {\em Some identities for
terminating $q$-series}, Math. Proc. Camb. Phil. Soc.,
{\bf 89} (1981), 211--223.
\bibitem{ekhad} S.B. Ekhad and S. Tre, {\em A purely
verification proof of the first Rogers-Ramanujan identity},
J. Comb. Th. (A), {\bf 54} (1990), 309--311.
\bibitem{GR} G. Gasper and M. Rahman, {\em Basic
Hypergeometric Series}, Encyclopedia of Mathematics
and its Applications Vol.35,
G.-C. Rota ed.,
Cambridge University Press, London and New York, 1990.
\bibitem{gosper} R.W. Gosper, {\em Decision procedures for indefinite
hypergeometric summation}, Proc. Natl. Acad. Sci. USA.,
{\bf 75}, 40--42.
\bibitem{gkp} R. Graham, D. Knuth and O. Patashnik, {\em
Concrete Mathematics, A Foundation for Computer Science}.
Addison-Wesley, 1989.
\bibitem{koorn} T.H. Koornwinder, {\em On Zeilberger's Algorithm
and its $q$-analogue}, J. of Comput. and Appl. Math.,
{\bf 48} (1993), 91--111.
\bibitem{paule} P. Paule, {\em On identities of the
Rogers-Ramanujan type}, J. Math. Anal. Appl.,
{\bf 107} (1985), 255--284.
\bibitem{gff} P. Paule, {\em Greatest-Factorial Factorization
and Symbolic Summation I}, RISC-Linz Report Series No. 93-02
(submitted to J. Symb. Computation).
\bibitem{pp-riese} P. Paule and A. Riese, {\em A Mathematica
version of Zeilberger's Algorithm for proving
terminating $q$-hypergeometric series identities},
in preparation.
\bibitem{riese} A. Riese, {\em A Mathematica $q$-analogue
of Zeilberger's algorithm for proving $q$-hypergeometric
identities}, diploma thesis, in preparation.
\bibitem{schur} I. Schur, {\em Ein Beitrag zur additiven
Zahlentheorie und zur Theorie der Kettenbr\"uche}, S.-B.
Preuss. Akad. Wiss. Phys.-Math.Kl. (1917) 302--321.
(Reprinted: Gesammelte Abhandlungen, Vol.2, Springer,
Berlin (1973), 117--136.
%\bibitem{stan} R. Stanley, {\em Differentiably finite power
%series}, Europ. J. Comb., {\bf 1} (1980), 175--188.
\bibitem{qwz} H.S. Wilf and D. Zeilberger, {\em Rational function
certification of mul\-ti\-sum$/$integral$/$`q'identities}, Bull. Amer.
Math. Soc. (N.S.), {\bf 27} (1992), 148--153.
\bibitem{wz} H.S. Wilf and D. Zeilberger, {\em An algorithmic proof
theory for hypergeometric (ordinary and "q") multisum/integral
identities}, Invent. Math., {\bf 108} (1992), 575--633.
\bibitem{holo} D. Zeilberger,
{\em A holonomic systems approach to special
function identities}, J.\ Comp.\ Appl.\ Math.,
{\bf 32} (1990), 321--368.
\bibitem{fast} D. Zeilberger, {\em A fast algorithm for proving
terminating hypergeometric identities}, Discr. Math.,
{\bf 80} (1990), 207--211.
\bibitem{creative} D. Zeilberger, {\em The method of creative
telescoping}, J. Symb. Computation, {\bf 11} (1991), 195--204.
\bibitem{saviour} D. Zeilberger, {\em Theorems for a price:
tomorrow's semi-rigorous mathematical culture}, Notices of the
A.M.S., {\bf 40} (1993), 978--981.
\end{thebibliography}
\end{document}
%-----------------END OF LATEX-FILE--------------------------------