Consider the TRS R consisting of the rewrite rule 1: f(f(x)) -> g(f(x)) There are no dependency pairs. Hence the TRS is trivially terminating.