Termination issues of rewrite systems in general are handled in Abstract rewriting system. For term rewriting systems in particular, the following additional subtleties are to be considered.

Termination even of a system consisting of one rule with a linear left-hand side is undecidable. Termination is also undecidable for systems using only unary function symbols; however, it is decidable for finite ground