This is due to the internal use of Gröbner basis calculations which cannot accomodate unknown functions.
The code is correct in the case of the elimination of Tx, but not in the cas of the elimination of x.
The internal normalizer for elements in an Ore algebra is not correctly implemented. This functionality is not exported to the user (yet), but the bug hinders certain types of Gröbner basis calculations (inducing weaknesses in Groebner).
The bug is a lack of type-checking: term orderings defined by a matrix have to be defined by a matrix of full rank in order to be total orderings (which is needed for the termination of the algorithm).
All indeterminates that have been declared polynomial in an algebra have to be sorted by the term order description. Without this type-checking, one has a real pain realizing that one misspelled an indeterminate.
In the Weyl algebra Q<x,Dx>, Dx and x2 yield the S-polynomial 2x which is not considered by gbasis: for a strange reason, Buchberger's first criterion which is known not to apply in the non commutative case was mistakenly used.
The code for Gröbner bases for modules is wrong in Maple V Release 5. This is due to a subtle interaction between the module structure and the improved selection strategy.
[This bug is present in the release 5, but not in version 2.1 of Mgfun, which is available for release 4 only.]
Maple's data structure for polynomials will confuse me till the end of my life. Easy fix.
Easy fix.