Consider the TRS R consisting of the rewrite rules 1: 1 . x -> x 2: x . 1 -> x 3: i(x) . x -> 1 4: x . i(x) -> 1 5: i(1) -> 1 6: i(i(x)) -> x 7: i(y) . (y . z) -> z 8: y . (i(y) . z) -> z There are no dependency pairs. Hence the TRS is trivially terminating.