Elimination of variables in linear solvable polynomial algebras and partial derivative-holonomicity

Let k be a field of characteristic 0. Based on the Gelfand-Kirillov dimensi on computation of modules over solvable polynomial k-algebras, where solvab le polynomial algebras are in the sense of A. Kandri-Rody and V. Weispfenni ng (1990, J. Symbolic Comput. 9, 1-26), we prove that the elimination lemma , obtained from D. Zeilberger (1990, J. Comput. Appl. Math. 32, 321-368) by using holonomic modules over the Weyl algebra A,(k) and used in the automa tic proving of special function identities, holds for a class of solvable p olynomial k-algebras without any "holonomicity" restriction. This opens a w ay to the solution of the extension/contraction problem stemming from the a utomatic proving of multivariate identities with respect to the partial der ivative -finiteness in the sense of F. Chyzak and B. Salvy (1998, J. Symbol ic Comput. 26, 187-227). It also yields a partial derivative -holonomicity so that automatic proving of multivariate identities may be dealt with by m anipulating polynomial function coefficients instead of rational functions. (C) 2000 Academic Press.