Consider the TRS R consisting of the rewrite rules

1: zeros -> cons(0,n__zeros)
2: tail(cons(X,XS)) -> activate(XS)
3: zeros -> n__zeros
4: activate(n__zeros) -> zeros
5: activate(X) -> X

There are 2 dependency pairs:

6: TAIL(cons(X,XS)) -> ACTIVATE(XS)
7: ACTIVATE(n__zeros) -> ZEROS

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