#inMishna5


steps := [[1,1],[0,-1],[-1,0]]: # must have length 3.
offset := 3:
closedform := 2*27^(n-1)*pochhammer(4/3,n-1)*pochhammer(5/3,n-1)/pochhammer(5/2,n-1)/pochhammer(3,n-1):
obviousrec := f[i,j,n]=f[i+steps[1,1],j+steps[1,2],n-1]+f[i+steps[2,1],j+steps[2,2],n-1]+
              f[i+steps[3,1],j+steps[3,2],n-1]:
operator := Sn - (Si^steps[1,1]*Sj^steps[1,2]+Si^steps[2,1]*Sj^steps[2,2]+Si^steps[3,1]*Sj^steps[3,2]):
gu := 1458*(1 + n)*(2 + n)*(159 + 136*i - 68*j + 80*n + 9*n^2)*f[i, j, n] + 
 9*(-44478 - 181221*i + 130420*i^2 + 230800*i^3 + 67888*i^4 - 105576*j + 
   130316*i*j - 660372*i^2*j - 371924*i^3*j + 146560*j^2 + 443604*i*j^2 + 
   707820*i^2*j^2 - 76568*j^3 - 540608*i*j^3 + 139120*j^4 - 41001*n - 
   381864*i*n + 191808*i^2*n + 142848*i^3*n - 25878*j*n - 99288*i*j*n - 
   482904*i^2*j*n + 122400*j^2*n + 460440*i*j^2*n - 132048*j^3*n - 
   13788*n^2 - 116667*i*n^2 + 71940*i^2*n^2 - 16164*j*n^2 - 100668*i*j*n^2 + 
   50988*j^2*n^2 - 2013*n^3 - 4896*i*n^3 - 6120*j*n^3 - 108*n^4)*
  f[i, j, 3 + n] - (-21060 - 969246*i + 480993*i^2 + 244165*i^3 + 21886*i^4 + 
   59382*j - 418482*i*j - 802518*i^2*j - 118028*i^3*j + 275232*j^2 + 
   734634*i*j^2 + 218100*i^2*j^2 - 207332*j^3 - 156416*i*j^3 + 34480*j^4 - 
   15948*n - 407910*i*n + 219325*i^2*n + 47480*i^3*n - 41586*j*n - 
   259606*i*j*n - 160152*i^2*j*n + 143470*j^2*n + 151848*i*j^2*n - 
   42928*j^3*n - 4167*n^2 - 50857*i*n^2 + 23980*i^2*n^2 - 20824*j*n^2 - 
   33556*i*j*n^2 + 16996*j^2*n^2 - 457*n^3 - 1632*i*n^3 - 2040*j*n^3 - 
   18*n^4)*f[i, j, 6 + n] + 54*(29349*i + 159690*i^2 - 200400*i^3 + 204*i^4 + 
   149382*j - 451641*i*j + 701100*i^2*j - 714*i^3*j + 222159*j^2 - 
   701676*i*j^2 + 306*i^2*j^2 + 207660*j^3 + 816*i*j^3 - 408*j^4 + 
   202284*i*n - 137462*i^2*n - 67480*i^3*n + 5901*j*n + 137675*i*j*n + 
   235536*i^2*j*n - 26777*j^2*n - 236136*i*j^2*n + 69968*j^3*n + 
   63827*i*n^2 - 64040*i^2*n^2 - 5893*j*n^2 + 96992*i*j*n^2 - 34052*j^2*n^2 - 
   204*i*n^3 + 3060*j*n^3)*f[i, 1 + j, 2 + n] + 
 (-3466116*i + 2445516*i^2 + 914918*i^3 + 7696*i^4 + 689364*j - 2822667*i*j - 
   3123939*i^2*j - 26936*i^3*j + 758460*j^2 + 3158151*i*j^2 + 11544*i^2*j^2 - 
   927346*j^3 + 30784*i*j^3 - 15392*j^4 - 1379574*i*n + 1222792*i^2*n + 
   135368*i^3*n + 149691*j*n - 1729387*i*j*n - 469848*i^2*j*n + 
   568135*j^2*n + 466152*i*j^2*n - 135856*j^3*n - 124594*i*n^2 + 
   128080*i^2*n^2 - 34114*j*n^2 - 193984*i*j*n^2 + 68104*j^2*n^2 + 
   408*i*n^3 - 6120*j*n^3)*f[i, 1 + j, 5 + n] - 
 324*(2 + n)*(52536*i - 50202*i^2 + 204*i^3 - 33009*j + 73800*i*j - 
   306*i^2*j - 25524*j^2 - 306*i*j^2 + 204*j^3 + 18124*i*n - 16768*i^2*n - 
   11411*j*n + 25195*i*j*n - 8797*j^2*n)*f[i, 2 + j, 1 + n] + 
 3*(2717076*i - 2631694*i^2 + 7288*i^4 - 1709010*j + 3883759*i*j + 
   7288*i^3*j - 1342069*j^2 - 5466*i^2*j^2 - 3644*i*j^3 + 1822*j^4 + 
   896840*i*n - 840272*i^2*n - 563062*j*n + 1256708*i*j*n - 436808*j^2*n + 
   72496*i*n^2 - 67072*i^2*n^2 - 45644*j*n^2 + 100780*i*j*n^2 - 
   35188*j^2*n^2)*f[i, 2 + j, 4 + n] + 49572*(2*i - j)*(2 + i + j)*(1 + n)*
  (2 + n)*f[i, 3 + j, n] - 54*(2*i - j)*(2 + i + j)*(4 + n)*(211 + 34*n)*
  f[i, 3 + j, 3 + n] + 162*(63579*i + 15192*i^2 + 408*i^3 - 21018*j - 
   28254*i*j - 1326*i^2*j + 3372*j^2 + 1020*i*j^2 + 45380*i*n + 7988*i^2*n - 
   10290*j*n - 15062*i*j*n + 1124*j^2*n + 10465*i*n^2 + 884*i^2*n^2 - 
   800*j*n^2 - 1768*i*j*n^2 + 884*i*n^3)*f[1 + i, j, 2 + n] - 
 6*(254940*i + 57967*i^2 + 187*i^3 - 56385*j - 119975*i*j + 26784*j^2 - 
   1632*i*j^2 + 1768*j^3 + 113065*i*n + 14678*i^2*n - 14103*j*n - 
   29768*i*j*n + 3776*j^2*n + 17095*i*n^2 + 884*i^2*n^2 - 800*j*n^2 - 
   1768*i*j*n^2 + 884*i*n^3)*f[1 + i, j, 5 + n] + 
 972*j*(2 + n)*(384 + 179*n)*f[1 + i, 1 + j, 1 + n] - 
 9*j*(23381 + 8248*n + 716*n^2)*f[1 + i, 1 + j, 4 + n] - 
 148716*j*(1 + n)*(2 + n)*f[1 + i, 2 + j, n] + 
 162*j*(4 + n)*(211 + 34*n)*f[1 + i, 2 + j, 3 + n] + 
 5832*(2 + n)*(104*i - 68*j + 63*i*n - 68*j*n)*f[2 + i, j, 1 + n] - 
 54*(7377*i - 6752*j + 2760*i*n - 2776*j*n + 252*i*n^2 - 272*j*n^2)*
  f[2 + i, j, 4 + n] - 99144*(i - 2*j)*(1 + n)*(2 + n)*f[3 + i, j, n] + 
 108*(i - 2*j)*(4 + n)*(211 + 34*n)*f[3 + i, j, 3 + n]:



# no further changes needed below.

print(`Lattice Walks in the Quarter-Plane`):
print():
print(`By Shalosh B. Ekhad (c/o D. Zeilberger), and Manuel Kauers' computer`):
print():
print(`Theorem`): 
print(`Let f[i,j,n] be the number of walks from the origin,`):
print(`to the point (i,j), with exactly n steps, staying in the`):
print(`first quarter-plane i>=0, j>=0, using the steps`):
print({op(steps)}):
print(`Then `):
print(f[0,0,offset*n]= closedform ):

print():

print(`Proof: By using the obvious recurrence `):
print(obviousrec):
print(`For n>=1, i>=0, j>=0 `):
print(`subject to the initial conditions `):
print(`f[0,0,0]=1, f[i,j,0]=0 if`, (i,j)<>(0,0) ):
print(`and boundary conditions: `):
print(f[-1,j,n]=0, f[i,-1,n]=0 ):
print(`the computer first generates lots of data`):
print(`and then using the quasi-holonomic ANSATZ `):
print(`as described in Manuel Kauers and Doron Zeilberger's `):
print(`seminal paper : The quasi-holonomic ansatz and restricted `):
print(`lattice paths `):
print(`finds the following partial recurrence equation `):

print(gu=0):

Gu:=gu:
for i0 from 0 to 20 do
for j0 from 0 to 20 do
for n0 from 0 to 20 do
 Gu:=subs(f[i+i0,j+j0,n+n0]=Si^i0*Sj^j0*Sn^n0,Gu):
od:
od:
od:

print(`Let Si, Sj, Sn be the fundamental shift operators in the`):
print(` i, j, and n , directions, respectively `):
print(`The above lemma means that f[i,j,n] is annihilated by the operator`):
lprint(Gu);

print(`The proof that this opeator indeed annihilates f[i,j,n] `):
print(`is routine.`):
print(`Indeed, f[i,j,n] is annihilated by the operator `):
print(operator):
print():

print(`taking successive commatators we eventually get the 0 operator  `):
print(`and all we have to do is check that the inital conditions `):
print(` for the intermediate operators also hold, that is a (fast!)`):
print(`routine verification . `):

printf("Plugging-in i=0,j=0,n->%g n, we get that f[0,0,%g n] satisfies\n", offset, offset):

gu00:=subs({i=0,j=0,n=offset*n},gu):

print(gu00=0):

printf("But the very same recurrence is also satisfied by h(%g n):=\n", offset):

print(closedform):

print(`since plugging this last expression indeed gives`):
mu00:=subs({f[0,0,offset*n]=closedform, 
            f[0,0,offset*n+offset]=subs(n=n+1,closedform),
            f[0,0,offset*n+2*offset]=subs(n=n+2,closedform),
            f[0,0,offset*n+3*offset]=subs(n=n+3,closedform),
            f[0,0,offset*n+4*offset]=subs(n=n+4,closedform)},gu00):

mu00:=normal(simplify(mu00/closedform)):
print(mu00):

print(`Since the theorem is true for n=0,1,2,3 (check!) `):
print(`It is true in general. QED `):