######################################################################
## ZipeiNie.txt: Save this file as  ZipeiNie.txt      to use it,     #
# stay in the                                                        #
## same directory, get into Maple (by typing: maple <Enter> )        #
#then type: read `ZipeiNie.txt`: <Enter>                             #
## Then follow the instructions given there                          #
##                                                                   #
## Written by George Spahn and Doron Zeilberger, Rutgers University ,#
##  DoronZeil@gmail.com      .                                       # 
######################################################################

with(combinat):

Digits:=100:

print(`First Written: Jan. 2023: tested for Maple 20  `):
print():
print(`This is ZipeiNie.txt, A Maple package`):
print(`accompanying George Spahn and Doron Zeilberger's  article: `):
print(` Automating Zipei Nie's Human-Generated Proof of a Conjecture of Svante Janson`):
print(`-------------------------------`):

print(`-------------------------------`):
print():
print(`The most current version is available on WWW at:`):
print(` http://www.math.rutgers.edu/~zeilberg/tokhniot/ZipeiNie.txt .`):
print(`Please report all bugs to: zeilberg at math dot rutgers dot edu .`):
print():
print(`-------------------------------`):
print(`For general help, and a list of the MAIN functions,`):
print(` type "ezra();". For specific help type "ezra(procedure_name);" `):

print(`-------------------------------`):
print(`For a list of the supporting functions type: ezra1();`):
print(`For help with a specific procedure, type "ezra(procedure_name);"`):
print():
 print(`-------------------------------`):



ezra1:=proc()
if args=NULL then

print(` The supporting procedures are:     Gn,`):
print(` `):

else
 ezra(args):
fi:
end:



ezra:=proc()

if args=NULL then

print(` ZipeiNie.txt: A Maple package for automatic Zipei Nie's human-generated proof of Svante Janson's conjecture`):
print(`The main procedures are :  Fkn,  GenT, Th21, Th22, Th23, Th14  `):

elif nargs=1 and args[1]=GenT then
print(`GenT(S,n,w,n1): Given the object S=[a(n,w),[b1,b2,b3],[c1,c2,c3]] where a is an expression in n and w and b1,b2,b3,c1,c2,c3 are constants, outputs`):
print(`the n1-th term of the sequence defined by the Svante Janson style quadratic functional equation`):
print(`f_n(w)=a(n,w)*Sum(f_k(w+b1+b2*k+b3*n)*f_{n-k}(w+c1+c2*k+c3*n),k=1..n-1), f_0(w)=a(0,w). Note that for any pos. integer n1`):
print(`Gn(n1,w,x,z); should be the same as:`):
print(`GenT([1/(w+(n-1)*x),[0,0,0],[0,z,0]],n,w,n1);`):

elif nargs=1 and args[1]=Gn then
print(`Gn(n,w,x,z): \hat G_n(1-w,x,z) in Zipei Nie's paper. Try:`):
print(`Gn(4,w,x,z);`):

elif nargs=1 and args[1]=Th14 then
print(`Th14(n): Verifies Theorem 1.4 in Zipei Nie's paper for n from 1 to N. Try`):
print(`Th14(8);`):


elif nargs=1 and args[1]=Th21 then
print(`Th21(n): Verifies Theorem 2.1 in Zipei Nie's paper for n>=3. Try`):
print(`{seq(Th21(n),n=3..8)};`):


elif nargs=1 and args[1]=Th22 then
print(`Th22(n): Verifies Theorem 2.2 in Zipei Nie's paper for n. Try`):
print(`{seq(Th22(n),n=1..8)};`):


elif nargs=1 and args[1]=Th23 then
print(`Th23(n): Verifies Theorem 2.3 in Zipei Nie's paper for n>=3. Try`):
print(`{seq(Th23(n),n=3..10)};`):


else
 print(`There is no such thing as`, args):

fi:



end:





#GenT(S,n,w,n1): Given the object S=[a(n,w),[b1,b2,b3],[c1,c2,c3]] where a is an expression in n and w and b1,b2,b3,c1,c2,c3 are constants, outputs
#the n1-th term of the sequence defined by the Svante Janson style quadratic functional equation
#f_n(w)=a(n,w)*Sum(f_k(w+b1+b2*k+b3*n)*f_{n-k}(w+c1+c2*k+c3*n),k=1..n-1), f_0(w)=a(0,w). Note that for any pos. integer n1
#Gn(n1,w,x,z); should be the same as:
#GenT([1/(w+(n-1)*x),[0,0,0],[0,z,0]],n,w,n1);
GenT:=proc(S,n,w,n1) local k1,a,b,c:
option remember:

a:=S[1]:
b:=S[2]:
c:=S[3]:

if n1=1 then
 RETURN(subs(n=1,a)):
else

normal(subs(n=n1,a)*add(subs(w=w+b[1]+b[2]*k1+b[3]*n1, GenT(S,n,w,k1))*subs(w=w+c[1]+c[2]*k1+c[3]*n1, GenT(S,n,w,n1-k1)),k1=1..n1-1)):
fi:
end:




#Verifies empirically Theorem 1.4 in Zipei Nei's paper, i.e. Svante Janson's conjecture for n from 1 to N.
Th14:=proc(N) local w,x,z,n,n1:
evalb({seq(GenT([1/(1-w-(n-1)*x),[0,0,0],[0,z,0]],n,w,n1)-GenT([1/(1-w),[x,0,0],[0,z,0]],n,w,n1),n1=1..N)}={0}):
end:


#Gn(n1,w,x,z): \hat G_n(1-w,x,z) in Zipei Nie's paper. Try
#Gn(4,w,x,z);
Gn:=proc(n1,w,x,z) local n:
option remember:
GenT([1/(w+(n-1)*x),[0,0,0],[0,z,0]],n,w,n1):
end:



#Fkn(k,n,w,x,z): F_{k,n}(w) in p.3 of Zipei Nie's paper, where 1<=k<n. Try:
#Fkn(2,4,w,x,z);
Fkn:=proc(k,n,w,x,z) local i:
option remember:

if k=1 then
 Gn(n,w,x,z):
else
normal(
add(subs(w=w+(k+i)*z,Gn(n-k-i,w,x,z))*Fkn(k,k+i,w,x,z),i=1..n-k-1)/(w+(n-1)*x)+
add((w+i*z)*subs(w=w+x,Gn(i,w,x,z))*subs(w=w+i*z,Fkn(k-i,n-i,w,x,z)),i=1..k-1)/(w+(n-1)*x)/w
):
fi:
end:



#Th21(n)
Th21:=proc(n) local w,x,z:

if not (type(n,integer) and n>=3) then
 print(`The argument`, n, `should have been an ingetger >=3`):
 RETURN(FAIL):
fi:

evalb(normal(Gn(n,w,x,z)-subs(w=w+z,Gn(n-1,w,x,z))/w/(w+x)-Fkn(2,n,w,x,z))=0):
end:



#Th22(n)
Th22:=proc(n) local w,x,z:
evalb(normal(subs(w=w+x,Gn(n-1,w,x,z))/w/(w+(n-1)*z)-Fkn(n-1,n,w,x,z))=0):
end:



#Th23a(k,n)
Th23a:=proc(k,n) local w,x,z:
evalb(normal(Fkn(k,n,w,x,z)-Fkn(k+1,n,w,x,z)-subs(w=w+x,Gn(k,w,x,z))*subs(w=w+k*z,Gn(n-k,w,x,z))/w)=0):
end:


#Th23(n):
Th23:=proc(n) local k:

if not (type(n,integer) and n>=3) then
 print(`The argument`, n, `should have been an ingetger >=3`):
 RETURN(FAIL):
fi:


evalb({seq(Th23a(k,n),k=1..n-2)}={true}):
end: