print(`A One-Line, Purely Empirical (Yet Rigorous!) Proof of Krewaras' `): print(` Latice Walks in the Quarter-Plane Celebrated Theorem`): print(): print(`By Shalosh B. Ekhad (c/o D. Zeilberger), and Manuel Kauers' computer`): print(): print(`Theorem(Kreweras)`): 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 (-1,0),(0,-1)`): print(` and (1,1) [i.e. South, West, and North-East ] `): print(`Then `): print(f[0,0,3*n]= 4^n *(3*n)!/(n+1)!/(2*n+1)! ): print(): print(`Proof: By using the obvious recurrence `): print(f[i,j,n]=f[i+1,j,n-1]+f[i,j+1,n-1]+f[i-1,j-1,n-1] ): 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 `): gu:= -11664*(55335911400 + 6899315729597022*i + 143693631158720*i^2 - 17358455208640*i^3 + 3429073388160*i^4 - 13890238435916844*j - 568343523412640*i*j + 103388714943360*i^2*j - 27432587105280*i^3*j + 561888083129600*j^2 - 205253397269760*i*j^2 + 82297761315840*i^2*j^2 + 135819576435200*j^3 - 109730348421120*i*j^3 + 54865174210560*j^4 + 110845835100*n + 12655932970789527*i*n + 71103437692800*i^2*n + 13503205284800*i^3*n - 25472999121480174*j*n - 277215592692480*i*j*n - 81781248017280*i^2*j*n + 269994654821760*j^2*n + 165086528651520*i*j^2*n - 111073707512320*j^3*n + 72563129100*n^2 + 6750536833164462*i*n^2 + 6278494461760*i^2*n^2 - 13584321033035484*j*n^2 - 24346820990560*i*j*n^2 + 23581323402880*j^2*n^2 + 18619316100*n^3 + 1045355692794357*i*n^3 - 2104432549116954*j*n^3 + 1566110700*n^4)*f[i, j, n] - 54*(-10319625439200 - 25631768921833334454*i - 13808667046076481950*i^2 + 40892540852271474*i^3 + 152429864558251266*i^4 + 56503567200559815948*j + 63593364639896830760*i*j + 2684352335186707236*i^2*j - 636188978589535728*i^3*j - 68132112312700650200*j^2 - 9130403228609127672*i*j^2 + 645351581606763024*i^2*j^2 + 7200545654043486288*j^3 + 177191608554652608*i*j^3 - 285155694478990944*j^4 - 9512904416400*n - 25874988361443058643*i*n - 6394487064162705504*i^2*n + 204423092398178540*i^3*n + 57926086236902626486*j*n + 31180491642896261496*i*j*n + 78246660707863800*i^2*j*n - 34194599971074157536*j^2*n - 1798045360302281520*i*j^2*n + 1649805406655213600*j^3*n - 3199042123200*n^2 - 7740591463822032441*i*n^2 - 655717190632208102*i^2*n^2 + 17813937154094120682*j*n^2 + 3634106076921351608*i*j*n^2 - 4161911018674302008*j^2*n^2 - 467049013200*n^3 - 708006667694802256*i*n^3 + 1703789664648063392*j*n^3 - 25057771200*n^4)*f[i, j, 3 + n] + (-29317592304000 - 300633833530171806750*i - 71673742795992632613*i^2 + 5326935233804465688*i^3 + 1486932683670374356*i^4 + 673718496871351085100*j + 358179337608147953532*i*j - 16841973105207217008*i^2*j - 11025800197666925408*i^3*j - 389900285264404584612*j^2 + 15887393720472328416*i*j^2 + 31437630704148997344*i^2*j^2 - 6997082675214766464*j^3 - 41018566946937314432*i*j^3 + 20702089173450648256*j^4 - 22201185283200*n - 154185617622273951825*i*n - 20413626648190997562*i^2*n + 1574886432129828312*i^3*n + 353599552101703391370*j*n + 105764487481916448408*i*j*n - 7132503474019513872*i^2*j*n - 117446050822862028168*j^2*n + 11567455971310164384*i*j^2*n - 7199789048662220736*j^3*n - 5800874032800*n^2 - 25742388987464821650*i*n^2 - 1311333925353028044*i^2*n^2 + 60462306438935557140*j*n^2 + 7267822572308927856*i*j*n^2 - 8323444683527527536*j^2*n^2 - 636188968800*n^3 - 1399287644304894800*i*n^3 + 3373908408510255520*j*n^3 - 25057771200*n^4)* f[i, j, 6 + n] - 162*(38174114510730219462*i + 1583523138856961910*i^2 - 1107870676280635836*i^3 + 232801727443477920*i^4 - 88215840851998741572*j - 12148977650086313256*i*j + 2312251125605343648*i^2*j - 994037868143159040*i^3*j + 15405794444251527384*j^2 - 373415619849672888*i*j^2 + 1209116522674405440*i^2*j^2 + 357844671276917712*j^3 - 357941940579025920*i*j^3 + 106893228801588480*j^4 + 31186518838842243491*i*n + 74925755166383758*i^2*n + 182687078762633996*i^3*n - 74316451835963302270*j*n - 6478085079968617696*i*j*n - 383793052917889632*i^2*j*n + 6930983948148927472*j^2*n + 116359609239023640*i*j^2*n - 160307046709037200*j^3*n + 8630879131252331275*i*n^2 + 32900789180128884*i^2*n^2 - 19815232957102847654*j*n^2 - 581035875060282360*i*j*n^2 + 820637754444053880*j^2*n^2 + 691280945474924032*i*n^3 - 1670118677306645504*j*n^3)*f[i, 1 + j, 2 + n] + 3*(377608135774516961445*i + 28842891657568501392*i^2 + 919630200543216224*i^3 + 3073941210789096752*i^4 - 865265432635379724066*j - 159856602854733317826*i*j + 17656045785879866358*i^2*j - 12801832833033652192*i^3*j + 153215514570085019748*j^2 - 76704875353420962402*i*j^2 + 12853896534263876448*i^2*j^2 + 69769718574924348140*j^3 + 1184951363986199168*i*j^3 - 565575594414277504*j^4 + 181227115330454937771*i*n + 6901173198086506984*i^2*n + 1757180898199506456*i^3*n - 419604252667344078678*j*n - 36668030653432203016*i*j*n + 923168086354624320*i^2*j*n + 28497943245313242760*j^2*n - 15374451697778048976*i*j^2*n + 10361391979979722464*j^3*n + 27630972444628523030*i*n^2 + 65801578360257768*i^2*n^2 - 64682246090004341068*j*n^2 - 1162071620528859120*i*j*n^2 + 1641275395495365360*j^2*n^2 + 1382561890949848064*i*n^3 - 3340237354613291008*j*n^3)* f[i, 1 + j, 5 + n] - 972*(406193965431101550*i + 1475591415173900566*i^2 - 539905791525783360*i^3 + 4935625662060800*i^4 + 2742808611095425692*j - 611850160207694272*i*j + 1412977478096367360*i^2*j - 33829551436925440*i^3*j + 1297083581614871872*j^2 - 863362542576533760*i*j^2 + 85086387791247360*i^2*j^2 + 394027846555298880*j^3 - 92276089933619200*i*j^3 + 35873029604679680*j^4 + 87363575524654833*i*n + 108213950734687389*i^2*n - 215733144808540320*i^3*n + 1173087363451765314*j*n + 695097876662397024*i*j*n + 448558418418419520*i^2*j*n + 10528316535065376*j^2*n - 38309983033800960*i*j^2*n + 8361457736113920*j^3*n - 425096992141370451*i*n^2 - 138340483041315447*i^2*n^2 + 250188082029934074*j*n^2 + 16198963200*i*j*n^2 - 8099481600*j^2*n^2)*f[i, 2 + j, 1 + n] + 18*(-22133171976187577325*i - 9990666168706688606*i^2 - 8417823285813584590*i^3 + 246190014540891072*i^4 + 44661366149480042538*j + 20272878892442227073*i*j + 18677979175392646953*i^2*j - 984211350770639664*i^3*j + 17781810008050749802*j^2 + 377103912541796121*i*j^2 + 1142747081710135704*i^2*j^2 + 1379935961332088138*j^3 + 26307476359285680*i*j^3 - 374251210155000*j^4 - 7745143991588196539*i*n - 3518138967742572607*i^2*n - 1473806805123873600*i^3*n + 8850266532141638698*j*n + 4089111279380074048*i*j*n + 3099238949402040960*i^2*j*n + 1867383181778631872*j^2*n - 850193984282740902*i*n^2 - 276680966082630894*i^2*n^2 + 500376147860904948*j*n^2)*f[i, 2 + j, 4 + n] - 419904*(1162927592407646*i + 2053336350490650*i^2 - 58164782122160*i^3 + 1238276501280*i^4 + 1630201675982768*j - 1438078123749680*i*j + 213809307644800*i^2*j - 4762601928000*i^3*j + 906295994213960*j^2 - 254378472326160*i*j^2 + 4000585619520*i^2*j^2 + 118647466973280*j^3 + 1524032616960*i*j^3 - 762016308480*j^4 + 2520265785905983*i*n + 2675755618883695*i^2*n - 32446731710960*i^3*n + 1652060299722224*j*n - 1460462105133360*i*j*n + 162373206822400*i^2*j*n + 922393267743080*j^2*n - 256950277367280*i*j^2*n + 123791077055520*j^3*n + 1434492398786049*i*n^2 + 722624412958165*i^2*n^2 - 1833411888*j*n^2 + 247677920*i*j*n^2 - 320987520*j^2*n^2 + 54054112*i*n^3 - 114301824*j*n^3)*f[i, 3 + j, n] - 432*(-831448312483168836*i - 431928476470298028*i^2 + 139002367041014712*i^3 + 2233268248345652*i^4 - 1143556599917760768*j - 644613338576528934*i*j - 282258505685792700*i^2*j + 19319159924071652*i^3*j - 292702899727220808*j^2 - 220616603108205066*i*j^2 - 15995116629777615*i^2*j^2 + 73368412226725470*j^3 - 25549576767454474*i*j^3 + 11177168442143837*j^4 - 397515531851422602*i*n - 242816184272188738*i^2*n + 28799075891510208*i^3*n - 218985132330254832*j*n - 42995570421779312*i*j*n - 69580200002268096*i^2*j*n - 84469586139338800*j^2*n - 51641817051871908*i*n^2 - 26014550927172084*i^2*n^2)*f[i, 3 + j, 3 + n] - 32256*(-297089601*i^2 + 44976826*i^3 + 37674888*i^4 + 1458000*j + 1063067655*i*j - 354432568*i^2*j - 146970492*i^3*j - 937388106*j^2 + 670268236*i*j^2 + 127864152*i^2*j^2 - 283495608*j^3 + 41066880*i*j^3 - 20430240*j^4 - 297089601*i*n + 75485930*i^2*n + 74384524*i^3*n + 469957653*j*n - 262335466*i*j*n - 153434416*i^2*j*n + 15667488*j^2*n + 11031304*i*j^2*n - 9315936*j^3*n + 30509104*i*n^2 + 35744384*i^2*n^2 + 63356058*j*n^2 - 4422820*i*j*n^2 + 5731920*j^2*n^2 - 965252*i*n^3 + 2041104*j*n^3)*f[i, 3 + j, 6 + n] - 10368*(-77211626806357404*i + 29784124858296747*i^2 - 3948457246529908*i^3 + 311432774056940*i^4 + 68539580565724812*j - 109617299138821881*i*j + 11793734677132836*i^2*j - 1153936785576220*i^3*j + 66638328369416958*j^2 - 32825170642439100*i*j^2 + 2157768460585605*i^2*j^2 + 17370155087074940*j^3 - 2897864872354630*i*j^3 + 1249206165560750*j^4 + 12092227540405918*i*n - 337312951343108*i^2*n + 563884660278864*i^3*n - 17309347895028398*j*n + 1380308883722636*i*j*n - 1863035306349408*i^2*j*n - 4352796592263032*j^2*n + 29218963032*i*n^2 + 16816879296*i^2*n^2 + 2012907456*j*n^2 - 130418064*i*j*n^2 + 377504064*j^2*n^2)*f[i, 4 + j, 2 + n] - 96768*(1536381801*i + 278395382*i^2 - 458041368*i^3 + 5181600*i^4 - 104834412*j + 1162288328*i*j + 1019540700*i^2*j - 3390624*i^3*j + 246095163*j^2 - 173768454*i*j^2 + 12404952*i^2*j^2 + 91040766*j^3 - 15831456*i*j^3 + 7146828*j^4 - 561386077*i*n - 488632032*i^2*n - 61552048*i^3*n - 107736840*j*n + 228886554*i*j*n + 124862308*i^2*j*n - 12384024*j^2*n - 2996836*i*j^2*n + 1889424*j^3*n - 115948266*i*n^2 - 66733648*i^2*n^2 - 7987728*j*n^2 + 517532*i*j*n^2 - 1498032*j^2*n^2)* f[i, 4 + j, 5 + n] - 62208*(1460994774781068*i - 5816639044782786*i^2 - 1273064998296160*i^3 + 165668546566600*i^4 - 22178683810980*j + 8888728564717770*i*j - 1405765711219980*i^2*j - 392510190582020*i^3*j - 3166573907624610*j^2 + 3553476974483865*i*j^2 - 5576719393560*i^2*j^2 - 1337811211056340*j^3 + 360417756788740*i*j^3 - 140105208883640*j^4 - 7185082767638040*i*n + 1707106143355790*i^2*n - 12036206147780*i^3*n + 7400555865816300*j*n - 5309578383799610*i*j*n + 192300574051020*i^2*j*n + 3422922845373920*j^2*n - 710366334662760*i*j^2*n + 380258412190360*j^3*n - 7121123352*i*n^2 - 3386612376*i^2*n^2)*f[i, 5 + j, 1 + n] + 580608*(-1292221741*i - 816263861*i^2 + 38256774*i^3 + 1751144*i^4 - 11540835*j - 47067275*i*j - 59369745*i^2*j + 1225224*i^3*j - 3149472*j^2 - 3264333*i*j^2 - 947598*i^2*j^2 + 70356*j^3 - 83152*i*j^3 + 15876*j^4 - 388426605*i*n - 222408845*i^2*n + 4949760*i^3*n - 148800*j*n - 5911640*i*j*n - 9955320*i^2*j*n - 74400*j^2*n - 28258426*i*n^2 - 13438938*i^2*n^2)*f[i, 5 + j, 4 + n] + 26127360*(-9695236400406*i + 5083378741215*i^2 + 846603096622*i^3 + 48986762688*i^4 + 8872878066030*j - 9319932679266*i*j - 289642630695*i^2*j - 61233453360*i^3*j + 4412642953761*j^2 - 1027655728638*i*j^2 + 18370036008*i^2*j^2 + 480413134915*j^3 + 3061672668*i*j^3 - 1530836334*j^4 - 9603383451318*i*n + 4801709344023*i^2*n + 1067043528718*i^3*n + 8895840611040*j*n - 9249514207902*i*j*n - 454972954767*i^2*j*n + 4447852189443*j^2*n - 1027655728638*i*j^2*n + 494190661921*j^3*n + 2769048*i*n^2 + 4488264*i^2*n^2)*f[i, 6 + j, n] + 17418240*(-4572936*i - 6684138*i^2 + 127308*i^3 + 17936*i^4 + 537435*j - 600804*i*j - 55158*i^2*j + 22056*i^3*j + 385767*j^2 - 181650*i*j^2 - 9072*i^2*j^2 + 88701*j^3 - 16438*i*j^3 + 6609*j^4 - 1615278*i*n - 2618154*i^2*n - 153836*i*n^2 - 249348*i^2*n^2)*f[i, 6 + j, 3 + n] + 1224720*(-100851585365946*i + 972439858133*i^2 + 2222816340256*i^3 + 5451427112*i^4 - 99666551128464*j - 10958034163530*i*j - 9902399558688*i^2*j - 27454685616*i^3*j + 17475882176512*j^2 + 12680818752608*i*j^2 + 38751635552*i^2*j^2 - 3534264893952*j^3 - 22587784192*j^4 - 56110759683367*i*n + 1826654182159*i^2*n - 6854271304*i^3*n - 63647870689768*j*n - 7270682749462*i*j*n + 6789767037120*j^2*n + 54832960832*j^3*n - 7497870788415*i*n^2 - 10141852683240*j*n^2 - 2410560*i*j*n^2 - 87105312352*j^2*n^2)* f[1 + i, j, 2 + n] + 22680*(808295593446150*i + 22824137471335*i^2 - 18568539489700*i^3 + 13603511440*i^4 + 946369196341968*j + 33786006401994*i*j + 61547868344296*i^2*j - 27231670640*i^3*j - 151926159800944*j^2 - 22281212593064*i*j^2 - 174101895344*i^2*j^2 - 53077996920016*j^3 + 587819010816*i*j^3 - 479075386816*j^4 + 224689863873595*i*n - 3653102114650*i^2*n + 13604490640*i^3*n + 279429726807488*j*n + 14540207916836*i*j*n - 12267500638144*j^2*n - 108833505920*j^3*n + 14995741576830*i*n^2 + 20283704562960*j*n^2 + 174215445824*j^2*n^2)*f[1 + i, j, 5 + n] - 3265920*(-5403474469438*i + 5104644577028*i^2 - 1028666132130*i^3 + 680371704*i^4 + 315119817995*j - 11029158118342*i*j + 4326495133584*i^2*j - 1814324544*i^3*j + 1686465013794*j^2 - 4994457364938*i*j^2 + 912420139860*j^3 + 3628649088*j^4)* f[1 + i, 1 + j, 1 + n] - 204120*j*(13362271433659 + 3905371031572*j)* f[1 + i, 1 + j, 4 + n] + 529079040*(72006005340*i - 31750679520*i^2 + 3401858520*i^3 - 13213349447*j + 69624704376*i*j - 14287805784*i^2*j - 12222562217*j^2 + 16328920896*i*j^2 - 2721486816*j^3 + 167310805*j*n + 24145195*j^2*n + 16740*j*n^2 + 16740*j^2*n^2)*f[1 + i, 2 + j, n] - 3674160*j*(514891438822 + 110537571325*j)*f[1 + i, 2 + j, 3 + n] + 391910400*j*(27737 + 26917*j + 9480*j^2 + 1240*j^3)*f[1 + i, 2 + j, 6 + n] + 88179840*(153689363773*i - 92173933418*j - 11927429530*j^2)* f[1 + i, 3 + j, 2 + n] - 195955200*j*(146862 + 121283*j + 38466*j^2 + 4960*j^3)*f[1 + i, 3 + j, 5 + n] + 176359680*(144502327503*i - 61526185274*j - 6158155820*j^2)* f[1 + i, 4 + j, 1 + n] + 391910400*j*(40974 + 21671*j + 6672*j^2 + 1240*j^3)*f[1 + i, 4 + j, 4 + n] + 705438720*(-57831594840*i - 19050407712*i^2 - 13267248228*i^3 + 1530836334*i^4 + 9922250819*j - 26194310604*i*j - 3061672668*i^2*j - 3061672668*i^3*j + 4538424585*j^2 - 3061672668*i*j^2 + 503979040*j^3 - 113231815*j*n - 54084417*j^2*n - 6299738*j^3*n)*f[1 + i, 5 + j, n] + 391910400*j*(5491 + 12892*j + 3081*j^2)*f[1 + i, 5 + j, 3 + n] - 440899200*(-451887*i + 368280*i^2 + 620682*i^3 - 2140914*j - 613056*i*j - 1780082*i^2*j - 1996408*j^2 + 1984000*j^3 - 545844*j*n - 558128*j^2*n - 24800*j^3*n + 16740*j*n^2 + 6696*j^2*n^2)*f[2 + i, j, 1 + n] + 8164800*(-13006254*i - 17607583*i^2 - 3149529*i^3 + 30511*i^4 + 31685690*j + 21486993*i*j + 4702939*i^2*j - 56120*i^3*j + 21616396*j^2 + 3968000*j^3 + 6169880*j*n + 2092096*j^2*n - 49600*j^3*n)*f[2 + i, j, 4 + n] - 2645395200*(1 + n)*(-15345*i + 15345*i^2 - 128126*j - 43028*i*j - 17728*j*n - 1116*i*j*n - 2144*j*n^2)*f[3 + i, j, n] - 24494400*(-5484582*i - 6788813*i^2 - 1900379*i^3 + 8710*i^4 - 20446086*j - 436212*i*j + 4211242*i^2*j - 21704*i^3*j + 9984856*j^2 - 3486720*j^3 - 879288*j*n - 482400*j^2*n + 43584*j^3*n)*f[3 + i, j, 3 + n] - 14515200*j*(164430 - 44802*i - 9912*i^2 - 616*i^3 + 585*j + 8631*i*j + 150*i^2*j - 10464*j^2 + 1548*i*j^2 + 548*j^3 + 96462*n - 1263*j*n - 2724*j^2*n + 13008*n^2 + 558*j*n^2 + 536*n^3)*f[3 + i, j, 6 + n] + 48988800*(-2350296*i - 2072412*i^2 - 411804*i^3 + 837*i^4 - 2150298*j - 1248306*i*j + 452430*i^2*j - 2232*i^3*j + 11874984*j^2 + 2424384*i*j^2 - 2949120*j^3 + 118220*j*n + 503832*j^2*n + 36864*j^3*n - 226512*j*n^2 - 13392*j^2*n^2 - 14912*j*n^3)*f[4 + i, j, 2 + n] - 14515200*j*(-460647 + 142551*i + 28974*i^2 + 1592*i^3 - 86985*j - 33213*i*j - 66*i^2*j + 16068*j^2 - 8040*i*j^2 + 5444*j^3 - 298701*n - 5013*j*n + 4608*j^2*n - 42294*n^2 - 1674*j*n^2 - 1864*n^3)* f[4 + i, j, 5 + n] + 97977600*(368280*i + 276210*i^2 + 46035*i^3 - 28158*j - 912888*i*j - 183582*i^2*j + 473652*j^2 + 357120*j^3 + 775210*j*n + 162612*j^2*n - 4464*j^3*n + 117120*j*n^2 + 6696*j^2*n^2 + 8480*j*n^3)*f[5 + i, j, 1 + n] + 14515200*j*(-426636 + 147264*i + 27828*i^2 + 1336*i^3 - 181551*j - 42309*i*j + 318*i^2*j - 3798*j^2 - 12516*i*j^2 + 13072*j^3 - 303960*n - 13671*j*n + 1116*j^2*n - 45180*n^2 - 1674*j*n^2 - 2120*n^3)* f[5 + i, j, 4 + n] - 3527193600*j*(1 + n)*(16843 + 5053*i - 9982*j + 1018*n + 62*j*n + 88*n^2)*f[6 + i, j, n] - 130636800*j*(-13659 + 5587*i + 974*i^2 + 40*i^3 - 8951*j - 1799*i*j + 26*i^2*j - 298*j^2 - 584*i*j^2 + 744*j^3 - 11217*n - 651*j*n - 1766*n^2 - 62*j*n^2 - 88*n^3)*f[6 + i, j, 3 + n]: 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(Sn-1/Si-1/Sj-Si*Sj): 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 . `): print(`Plugging-in i=0,j=0, n->3n, we get that f[0,0,3n] satisfies`): gu00:=subs({i=0,j=0,n=3*n},gu): print(gu00=0): print(`But the very same recurrence is also satisfied by h(3n):=`): Kr:=4^n*(3*n)!/(n+1)!/(2*n+1)!: print(Kr): print(`since plugging this last expression indeed gives`): mu00:=subs({f[0,0,3*n]=Kr, f[0,0,3+3*n]=subs(n=n+1,Kr), f[0,0,6+3*n]=subs(n=n+2,Kr)},gu00): mu00:=normal(simplify(mu00/Kr)): print(mu00): print(`Since Kreweras' theorem is true for n=0,1 (check!) `): print(`It is true in general. QED `):