Proving a certain binomial identity with three parameters I would like to prove the following identity:
$$\sum_{m\geq 0} (-1)^{i-m}{m+k \choose m} {i-1 \choose m-1}{m+k+1 \choose j}  = \sum_{m\geq 0} {m+k \choose k}{k+1 \choose i-m}{k+1 \choose j-m}$$
for fixed $i,j \geq 1$, $k\geq 0$.  If it helps, I have a combinatorial interpretation of the RHS:  it counts the number of arrangements of $i$ $a$'s, $j$ $b$'s, and $k$ $c$'s so that the substrings "aa", "bb" cannot occur (there is no restriction on the c's.)  This I can show, although I have not found a direct combinatorial proof.  If it's helpful I can give my proof for the right-hand side; I derived it from the so-called Carlitz-Scoville-Vaughan theorem which I found out about recently on Math Overflow.
It is related to this question; I have a proof for it, contingent on proving this binomial identity.  I "stumbled" across this through some very optimistic guessing, but I'm not sure how to prove it.  I thought of using WZ theory, but as far as I know that only applies to identities with one parameter, not more general ones - but I'd be very happy if an algorithmic verification was possible.
Other possibilities:  Interpret the left-hand side as an inclusion-exclusion argument, or a determinantal formula.  Or, find a recurrence that both sides satisfy.
 A: Multiply both sides by $x^iy^jz^k$ and sum over all indices.
First, let's look at the left side:
$$
\begin{align}
&\sum_{m,i,j,k}(-1)^{i-m}\binom{m+k}{m}\binom{i-1}{m-1}\binom{m+k+1}{j}x^iy^jz^k\\
&=\sum_{m,i,j,k}\binom{m+k}{k}\binom{-m}{i-m}\binom{m+k+1}{j}x^iy^jz^k\\
&=\sum_{m,j,k}\binom{m+k}{k}\binom{m+k+1}{j}\left(\frac{x}{1+x}\right)^my^jz^k\\
&=\sum_{m,k}\binom{m+k}{k}\left(\frac{x}{1+x}\right)^m(1+y)^{m+k+1}z^k\\
&=\sum_{m,k}(-1)^k\binom{-m-1}{k}\left(\frac{x}{1+x}\right)^m(1+y)^{m+k+1}z^k\\
&=\sum_{m}\left(\frac{x}{1+x}\right)^m(1+y)^{m+1}(1-(1+y)z)^{-m-1}\\
&=\frac{1+y}{1-(1+y)z}\frac{1}{1-\frac{x}{1+x}\frac{1+y}{1-(1+y)z}}\\
&=\frac{(1+x)(1+y)}{(1+x)+(1+y)-(1+x)(1+y)(1+z)}\tag{1}
\end{align}
$$
Next, let's look at the right side:
$$
\begin{align}
&\sum_{m,i,j,k}\binom{m+k}{k}\binom{k+1}{i-m}\binom{k+1}{j-m}x^iy^jz^k\\
&=\sum_{m,j,k}\binom{m+k}{k}\binom{k+1}{j-m}x^m(1+x)^{k+1}y^jz^k\\
&=\sum_{m,k}\binom{m+k}{k}x^m(1+x)^{k+1}y^m(1+y)^{k+1}z^k\\
&=(1+x)(1+y)\sum_{m,k}(-1)^k\binom{-m-1}{k}(xy)^m((1+x)(1+y)z)^k\\
&=(1+x)(1+y)\sum_{m}\frac{(xy)^m}{(1-(1+x)(1+y)z)^{m+1}}\\
&=\frac{(1+x)(1+y)}{1-(1+x)(1+y)z}\frac{1}{1-\frac{xy}{1-(1+x)(1+y)z}}\\
&=\frac{(1+x)(1+y)}{(1+x)+(1+y)-(1+x)(1+y)(1+z)}\tag{2}
\end{align}
$$
Comparing $(1)$ and $(2)$ shows that the left and right hand sides are equal.
A: You can apply the Zeilberger algorithm to this problem. The existence of several variables is not a problem, except that you have a choice in selecting the one you want to use. (This is because the quotient of your binomial coeffients will be automatically fully factorized and the additional variables will occur as constant terms in these linear factors.)
Say, you choose $j$ as the variable in the Zeilberger algorithm.
Then, you find a recurrence relation of degree 2 for the left sum and a recurrence relation of degree 3 for the right sum.
From these two recurrences, you can build up one recurrence for the difference (for example, gfun's rec+rec command if you use maple) and then just check that sufficiently initial conditions give zero.
The other variables will occur in the coefficients of your recurrence, but this does not pose a problem.
Another approach is to convert both sums to hypergeometric functions that happen to be ${}_3F_2$s and then search for the right transformation formula among the many known ones.
If you tell me what programs you use, I can give you more advice, but note that your notation of the sums is already problematic, because your right-hand expression is not necessarily zero for positive $m$, but presumably you want it to be.
