Definitions

(*ASMs*)
Clear[MTMatch,MT,ASM,NumberOfASM]
MTMatch[a_,b_]:=MTMatch[a,b]=And@@NonNegative[a-Most[b]]&&And@@NonNegative[Rest[b]-a]
MT[n_,m_]:=Module[{ss=Array[Composition[List,List],m]},Do[ss=Select[Flatten[Outer[Append,ss,Subsets[Range[m],{k}],1],1],
MTMatch[#[[k-1]],#[[k]]]&],{k,2,n}];ss]
ASM[0]:=ASM[0]={{}};ASM[1]:=ASM[1]={{{1}}}
ASM[n_?Positive]:=ASM[n]=Sort[Map[(Prepend[Rest[#]-Most[#],First[#]]&)@Append[Map[(Table[Boole[MemberQ[#,i]],{i,n}]&),#],Array[1&,n]]&,MT[n-1,n]]]
NumberOfASM[n_]:=NumberOfASM[n]=(∏_(i=0)^(n-1))(((3i+1)!)/((n+i)!))

(*ASM Statistics - Equations (2)-(3)*)
Clear[MinusNumber,InversionNumber,FirstRowNumber,LastRowNumber,FirstColumnNumber,LastColumnNumber]
MinusNumber[a_]:=MinusNumber[a]=Count[Flatten[a],-1]
InversionNumber[a_]:=InversionNumber[a]=Sum[a[[i,j]]a[[ii,jj]],{ii,2,Length[a]},{j,Length[a]},{i,ii-1},{jj,j}]
FirstRowNumber[a_]:=FirstRowNumber[a]=Position[First[a],1][[1,1]]-1
LastRowNumber[a_]:=LastRowNumber[a]=Length[a]-Position[Last[a],1][[1,1]]
FirstColumnNumber[a_]:=FirstColumnNumber[a]=Position[a[[All,1]],1][[1,1]]-1
LastColumnNumber[a_]:=LastColumnNumber[a]=Length[a]-Position[a[[All,-1]],1][[1,1]]

(*ASM generating functions - Equations (7), (9) & (10)*)
Clear[GeneralPower,QuadruplyRefinedZ,TriplyRefinedZ,AdjacentDoublyRefinedZ,OppositeDoublyRefinedZ,Z,QuadruplyRefinedAlternativeZ,AdjacentDoublyRefinedAlternativeZ]
GeneralPower[0,0]:=1
GeneralPower[a_,b_]:=(a^b)
QuadruplyRefinedZ[n_?Positive,x_,y_,z1_,z2_,z3_,z4_]:=QuadruplyRefinedZ[n,x,y,z1,z2,z3,z4]=
Plus@@Map[(x^(InversionNumber[#]))(y^(MinusNumber[#]))GeneralPower[z1,FirstRowNumber[#]]GeneralPower[z2,LastColumnNumber[#]]GeneralPower[z3,LastRowNumber[#]]GeneralPower[z4,FirstColumnNumber[#]]&,ASM[n]]
TriplyRefinedZ[n_,x_,y_,z1_,z2_,z3_]:=TriplyRefinedZ[n,x,y,z1,z2,z3]=QuadruplyRefinedZ[n,x,y,z1,1,z2,z3]
AdjacentDoublyRefinedZ[n_,x_,y_,z1_,z2_]:=AdjacentDoublyRefinedZ[n,x,y,z1,z2]=QuadruplyRefinedZ[n,x,y,z1,1,1,z2]
OppositeDoublyRefinedZ[n_,x_,y_,z1_,z2_]:=OppositeDoublyRefinedZ[n,x,y,z1,z2]=QuadruplyRefinedZ[n,x,y,z1,1,z2,1]
Z[n_,x_,y_,z_]:=Z[n,x,y,z]=QuadruplyRefinedZ[n,x,y,z,1,1,1]
Z[0,x_,y_]:=Z[0,x,y]=1
Z[n_,x_,y_]:=Z[n,x,y]=QuadruplyRefinedZ[n,x,y,1,1,1,1]
QuadruplyRefinedAlternativeZ[n_?Positive,x_,y_,z1_,z2_,z3_,z4_]:=QuadruplyRefinedAlternativeZ[n,x,y,z1,z2,z3,z4]=Expand[(((z2 z4))^(n-1))QuadruplyRefinedZ[n,x,y,z1,1/z2,z3,1/z4]]
AdjacentDoublyRefinedAlternativeZ[n_,x_,y_,z1_,z2_]:=AdjacentDoublyRefinedAlternativeZ[n,x,y,z1,z2]=QuadruplyRefinedZ[n,x,y,z1,z2,1,1]

(*Boundary-parameter coefficients in ASM generating functions - Equations (14)*)
Clear[AdjacentDoublyRefinedZCoefficient,ZCoefficient]
AdjacentDoublyRefinedZCoefficient[n_,x_,y_,k1_,k2_]:=AdjacentDoublyRefinedZCoefficient[n,x,y,zl,z2]=Coefficient[Coefficient[AdjacentDoublyRefinedZ[n,x,y,z1,z2],z1,k1],z2,k2]
ZCoefficient[n_,x_,y_,k_]:=ZCoefficient[n,x,y,k]=Factor[Coefficient[Z[n,x,y,z],z,k]]

Demonstrations

(*ASM(1), ASM(2) & ASM(3) - Equation (1)*)
Table[Map[MatrixForm,ASM[n]],{n,3}]

(*Quadruply-refined ASM generating functions for n=1,2,3 - Equation (8)*)
Table[QuadruplyRefinedZ[n,x,y,z1,z2,z3,z4],{n,3}]

(*Theorem 1 for n=2,...,6*)
Table[Factor[y(z4-z2) (z1-z3) QuadruplyRefinedZ[n,x,y,z1,z2,z3,z4] Z[n-2,x,y]-
(((z1-1)(z2-1)-y z1 z2)((z3-1)(z4-1)-y z3 z4) AdjacentDoublyRefinedZ[n-1,x,y,z4,z1]AdjacentDoublyRefinedZ[n-1,x,y,z2,z3]-
 (x (z4-1)(z1-1)-y)(x (z2-1)(z3-1)-y)z1 z2 z3 z4 AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,z2]AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z3,z4]-
(z2-1) (z3-1) ((z4-1)(z1-1)-y z4 z1)AdjacentDoublyRefinedZ[n-1,x,y,z4,z1] Z[n-2,x,y]+
(z3-1) (z4-1)(x(z1-1)(z2-1)-y)z1 z2(((x z3 z4))^(n-1))AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,z2] Z[n-2,x,y]-
 (z4-1)(z1-1) ((z2-1)(z3-1)-y z2 z3)  AdjacentDoublyRefinedZ[n-1,x,y,z2,z3] Z[n-2,x,y]+
(z1-1) (z2-1)(x(z3-1)(z4-1)-y)z3 z4(((x z1 z2))^(n-1))AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z3,z4] Z[n-2,x,y]+
(z1-1)(z2-1)(z3-1)(z4-1)(1-((((x^2) z1 z2 z3 z4))^(n-1)))((Z[n-2,x,y])^2))],{n,2,6}]

(*Recursive computation of quadruply-refined ASM generating function using Theorem 1*)
Clear[RecursiveQuadruplyRefinedZ,RecursiveAdjacentDoublyRefinedZ,RecursiveAdjacentDoublyRefinedAlternativeZ,RecursiveZ]
RecursiveQuadruplyRefinedZ[1,x_,y_,z1_,z2_,z3_,z4_]:=RecursiveQuadruplyRefinedZ[1,x,y,z1,z2,z3,z4]=1
RecursiveQuadruplyRefinedZ[2,x_,y_,z1_,z2_,z3_,z4_]:=RecursiveQuadruplyRefinedZ[2,x,y,z1,z2,z3,z4]=1+x z1 z2 z3 z4
RecursiveQuadruplyRefinedZ[n_,x_,y_,z1_,z2_,z3_,z4_]:=RecursiveQuadruplyRefinedZ[n,x,y,z1,z2,z3,z4]=Factor[
(((z1-1)(z2-1)-y z1 z2)((z3-1)(z4-1)-y z3 z4) RecursiveAdjacentDoublyRefinedZ[n-1,x,y,z4,z1]RecursiveAdjacentDoublyRefinedZ[n-1,x,y,z2,z3]-
 (x (z4-1)(z1-1)-y)(x (z2-1)(z3-1)-y)z1 z2 z3 z4 RecursiveAdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,z2]RecursiveAdjacentDoublyRefinedAlternativeZ[n-1,x,y,z3,z4]-
(z2-1) (z3-1) ((z4-1)(z1-1)-y z4 z1)RecursiveAdjacentDoublyRefinedZ[n-1,x,y,z4,z1] RecursiveZ[n-2,x,y]+
(z3-1) (z4-1)(x(z1-1)(z2-1)-y)z1 z2(((x z3 z4))^(n-1))RecursiveAdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,z2] RecursiveZ[n-2,x,y]-
 (z4-1)(z1-1) ((z2-1)(z3-1)-y z2 z3)  RecursiveAdjacentDoublyRefinedZ[n-1,x,y,z2,z3] RecursiveZ[n-2,x,y]+
(z1-1) (z2-1)(x(z3-1)(z4-1)-y)z3 z4(((x z1 z2))^(n-1))RecursiveAdjacentDoublyRefinedAlternativeZ[n-1,x,y,z3,z4]RecursiveZ[n-2,x,y]+
(z1-1)(z2-1)(z3-1)(z4-1)(1-((((x^2) z1 z2 z3 z4))^(n-1)))((RecursiveZ[n-2,x,y])^2))/(y(z4-z2) (z1-z3)  RecursiveZ[n-2,x,y])]
RecursiveAdjacentDoublyRefinedZ[n_,x_,y_,z1_,z2_]:=RecursiveAdjacentDoublyRefinedZ[n,x,y,z1,z2]=Module[{t},RecursiveQuadruplyRefinedZ[n,x,y,z1,t,t,z2]/.t->1]
RecursiveAdjacentDoublyRefinedAlternativeZ[n_,x_,y_,z1_,z2_]:=RecursiveAdjacentDoublyRefinedAlternativeZ[n,x,y,z1,z2]=Module[{t},RecursiveQuadruplyRefinedZ[n,x,y,z1,z2,t,t]/.t->1]
RecursiveZ[n_,x_,y_]:=RecursiveZ[n,x,y]=Module[{t1,t2},RecursiveQuadruplyRefinedZ[n,x,y,t1,t2,t2,t1]/.{t1->1,t2->1}]

Table[RecursiveQuadruplyRefinedZ[n,x,y,z1,z2,z3,z4]-QuadruplyRefinedZ[n,x,y,z1,z2,z3,z4],{n,3,6}]

(*Equation (80) for n=2,...,6*)
Table[Factor[y (z1-z3) (z2-z4)QuadruplyRefinedAlternativeZ[n,x,y,z1,z2,z3,z4] Z[n-2,x,y]-
(((z1-1)(z2-1)+y z1)((z3-1)(z4-1)+y z3 )(((z2 z4))^(n-1))AdjacentDoublyRefinedZ[n-1,x,y,1/z4,z1]AdjacentDoublyRefinedZ[n-1,x,y,1/z2,z3]-
(x (z4-1)(z1-1)+y z4)(x (z2-1)(z3-1)+y z2)z1 z3(((z2 z4))^(n-2)) AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,1/z2]AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z3,1/z4]-
(z2-1) (z3-1) ((z4-1)(z1-1)+y z1)(((z2 z4))^(n-1))AdjacentDoublyRefinedZ[n-1,x,y,1/z4,z1] Z[n-2,x,y]+
(z3-1) (z4-1)(x(z1-1)(z2-1)+y z2) z1 (z2^(n-2))(((x z3))^(n-1)) AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,1/z2] Z[n-2,x,y]-
(z4-1)(z1-1) ((z2-1)(z3-1)+y z3) (((z2 z4))^(n-1)) AdjacentDoublyRefinedZ[n-1,x,y,1/z2,z3] Z[n-2,x,y]+
(z1-1) (z2-1)(x(z3-1)(z4-1)+y z4)z3 (z4^(n-2))(((x z1))^(n-1))AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z3,1/z4] Z[n-2,x,y]+
(z1-1)(z2-1)(z3-1)(z4-1)((((z2 z4))^(n-1))-((((x^2) z1 z3))^(n-1)))((Z[n-2,x,y])^2))],{n,2,6}]

(*Corollary 2 for n=2,...,6*)
Table[Factor[(z2-z1)(z3-1)TriplyRefinedZ[n,x,y,z1,z2,z3]Z[n-2,x,y]-
(((z2-1)(z3-1)-y z2 z3)z1  AdjacentDoublyRefinedZ[n-1,x,y,z1,z3]Z[n-1,x,y,z2] -
(x(z1-1)(z3-1)-y) z1 z2 z3 AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z2,z3]Z[n-1,x,y,z1]-
(z1-1)(z3-1)z2 Z[n-1,x,y,z2]Z[n-2,x,y]+
(z2-1)(z3-1)z1 (((x z2 z3))^(n-1)) Z[n-1,x,y,z1]Z[n-2,x,y])],{n,2,6}]

(*Corollary 3 for n=2,...,6*)
Table[Factor[(z1-1) (z2-1) AdjacentDoublyRefinedZ[n,x,y,z1,z2]Z[n-2,x,y]-
(y z1 z2 AdjacentDoublyRefinedZ[n-1,x,y,z1,z2]Z[n-1,x,y]+(x(z1-1)(z2-1)-y)z1 z2 Z[n-1,x,y,z1]Z[n-1,x,y,z2]+
(z1-1) (z2-1)Z[n-1,x,y]Z[n-2,x,y])],{n,2,6}]
Table[Factor[(z1-1) (z2-1)AdjacentDoublyRefinedAlternativeZ[n,x,y,z1,z2]Z[n-2,x,y]-
(y z1 z2 AdjacentDoublyRefinedAlternativeZ[n-1,x,y,z1,z2]Z[n-1,x,y]+((z1-1)(z2-1)-y z1 z2)Z[n-1,x,y,z1]Z[n-1,x,y,z2]+
(z1-1) (z2-1)(((x z1 z2))^(n-1))Z[n-1,x,y]Z[n-2,x,y])],{n,2,6}]

(*Corollary 4 for n=2,...,6*)
Table[Factor[y(z2-z1)z3 TriplyRefinedZ[n,x,y,z1,z2,z3]Z[n-1,x,y]-
((z1-1)((z2-1)(z3-1)-y z2 z3) AdjacentDoublyRefinedZ[n,x,y,z1,z3]Z[n-1,x,y,z2] -
(z2-1)(x(z1-1)(z3-1)-y) z1 z3 AdjacentDoublyRefinedAlternativeZ[n,x,y,z2,z3]Z[n-1,x,y,z1]-
(z1-1)(z2-1)(z3-1) Z[n-1,x,y,z2]Z[n-1,x,y]+
(z1-1)(z2-1)(z3-1)z1 (z2^(n-1)) (((x z3))^n)Z[n-1,x,y,z1]Z[n-1,x,y])],{n,2,6}]

(*Corollary 5 for n=2,...,6*)
Table[Factor[(z1-z2) OppositeDoublyRefinedZ[n,x,y,z1,z2]Z[n-1,x,y]-
((z1-1)z2 Z[n,x,y,z1]Z[n-1,x,y,z2]-z1(z2-1)Z[n-1,x,y,z1]Z[n,x,y,z2])],{n,2,6}]

(*Corollary 6 for n=1,...,6*)
Table[Factor[AdjacentDoublyRefinedZ[n,x,y,z1,z2]-
Z[n-1,x,y](1+(∑_(i=1)^(n-1))(((((y z1 z2)/((z1-1)(z2-1)))))^(n-i))(1+(((x(z1-1)(z2-1)-y)Z[i,x,y,z1]Z[i,x,y,z2])/(y Z[i-1,x,y]Z[i,x,y]))))],{n,6}]
Table[Factor[AdjacentDoublyRefinedAlternativeZ[n,x,y,z1,z2]-
Z[n-1,x,y]((((x z1 z2))^(n-1))+(∑_(i=1)^(n-1))((((y/((z1-1)(z2-1)))))^(n-i))((x^(i-1))(((z1 z2))^(n-1))+(((((z1 z2))^(n-i-1))((z1-1)(z2-1)-y z1 z2)Z[i,x,y,z1]Z[i,x,y,z2])/(y Z[i-1,x,y]Z[i,x,y]))))],{n,6}]

(*Corollary 7 for n=1,...,6*)
Table[Factor[((z1-1)(z2-1)-y z1 z2) AdjacentDoublyRefinedZ[n,x,y,z1,z2]-
(x(z1-1)(z2-1)-y) z1 z2 AdjacentDoublyRefinedAlternativeZ[n,x,y,z1,z2]-
(z1-1)(z2-1)(1- (((x z1 z2))^n))Z[n-1,x,y]],{n,6}]

(*Corollary 8 for n=1,...,6, k=0,...,n-1*)
Table[Factor[ZCoefficient[n,x,y,k]-(Z[n-1,x,y]KroneckerDelta[k]+Z[n-1,x,y](∑_(i=0)^(k-1))((y^(i+1))Binomial[k-1,i]Binomial[n-1,i+1]+
(y^i)(∑_(j1=0)^(k-i-1))(∑_(j2=0)^(n-i-2))(((ZCoefficient[n-i-1,x,y,j1]ZCoefficient[n-i-1,x,y,j2])/( Z[n-i-1,x,y]Z[n-i-2,x,y]))(x Binomial[k-j1-2,i-1]Binomial[n-j2-2,i]-
y Binomial[k-j1-1,i]Binomial[n-j2-1,i+1]))))],{n,6},{k,0,n-1}]

(*Corollary 9 for n=2,...,6*)
Table[Factor[Z[n,x,y]-Z[n-1,x,y](1+(∑_(i=0)^(n-2))((y^(i+1))((Binomial[n-1,i+1])^2)+
((x (y^i)((((∑_(j=0)^(n-i-2))Binomial[n-j-2,i]ZCoefficient[n-i-1,x,y,j]))^2)-(y^(i+1))((((∑_(j=0)^(n-i-2))Binomial[n-j-1,i+1]ZCoefficient[n-i-1,x,y,j]))^2))/( Z[n-i-1,x,y]Z[n-i-2,x,y]))))],{n,2,6}]

(*Corollary 10 for n=2,...,6*)
Table[Factor[(z4 z1-z4+1)(z1 z2-z1+1)(z2 z3-z2+1)(z3 z4-z3+1)QuadruplyRefinedAlternativeZ[n,1,1,z1,z2,z3,z4]-
(((z1 z2 z3 z4)/(NumberOfASM[n-2](z1-z3)(z2-z4)))((z1 z2-z1+1)(z1 z2-z2+1)(z3 z4-z3+1)(z3 z4-z4+1)OppositeDoublyRefinedZ[n-1,1,1,z4,z1]OppositeDoublyRefinedZ[n-1,1,1,z2,z3]-
(z4 z1-z4+1)(z4 z1-z1+1)(z2 z3-z2+1)(z2 z3-z3+1)OppositeDoublyRefinedZ[n-1,1,1,z1,z2]OppositeDoublyRefinedZ[n-1,1,1,z3,z4])+
(z2-1) (z3-1)(z1 z2-z1+1)(z3 z4-z3+1)z4 z1 (z2^(n-1)) OppositeDoublyRefinedZ[n-1,1,1,z4,z1]+
(z3 -1)(z4-1)(z2 z3-z2+1)(z4 z1-z4+1)z1 z2 (z3^(n-1)) OppositeDoublyRefinedZ[n-1,1,1,z1,z2]+
(z4-1)(z1-1)(z3 z4-z3+1)(z1 z2-z1+1)z2 z3 (z4^(n-1)) OppositeDoublyRefinedZ[n-1,1,1,z2,z3]+
(z1 -1)(z2-1)(z4 z1-z4+1)(z2 z3-z2+1)z3 z4 (z1^(n-1))OppositeDoublyRefinedZ[n-1,1,1,z3,z4]+
(z1-1)(z2-1)(z3-1)(z4-1)((z1 z2-z1+1)(z3 z4-z3+1)(((z2 z4))^(n-1))+(z2 z3-z2+1)(z4 z1-z4+1)(((z1 z3))^(n-1)))NumberOfASM[n-2])],{n,2,6}]

(*Corollary 11 for n=2,...,6*)
Table[Factor[(z1 z3-z3+1)(z2 z3-z2+1)(z3^(n-1))TriplyRefinedZ[n,1,1,z1,z2,1/z3]-
(((z1  z3)/(NumberOfASM[n-2](z1-z2)(z3-1)))((z1 z3-z1+1)(z1 z3-z3+1)z2 Z[n-1,1,1,z1]OppositeDoublyRefinedZ[n-1,1,1,z2,z3]-
(z2 z3-z2+1)(z2 z3-z3+1)z1 Z[n-1,1,1,z2]OppositeDoublyRefinedZ[n-1,1,1,z1,z3])
+(z2 -1)(z3-1)(z1 z3-z3+1)z1  (z2^(n-1)) Z[n-1,1,1,z1]+
(z1-1)(z3-1) (z2 z3-z2+1) (z3^(n-1)) Z[n-1,1,1,z2])],{n,2,6}]