Elimination in Weyl Algebra and q-Identities

For the algorithmic proof of q-proper-hypergeometric identities, H.Wilf and D.Zeiberggave a theoretical frame work. In [1], they proved that q-proper-hypergeometric termssatisfy recurrence relations with polynomial coefficients and could obtain quite explicitbounds for the order of such a recurrence. But how can we find the recurrence relations?We consider single-variable q-proper-hypergeometric identities based on Zeilberg's basicidea. To find the recurrence relations, an elimination in the non-conuntative Weyl algebra