Consider the TRS R consisting of the rewrite rule

1: f(s(X),Y) -> h(s(f(h(Y),X)))

There is one dependency pair:

2: F(s(X),Y) -> F(h(Y),X)

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.