Consider the TRS R consisting of the rewrite rules

1: first(0,X) -> nil
2: first(s(X),cons(Y)) -> cons(Y)
3: from(X) -> cons(X)

There are no dependency pairs.
Hence the TRS is trivially terminating.