Consider the TRS R consisting of the rewrite rules

1: fst(0,Z) -> nil
2: fst(s,cons(Y)) -> cons(Y)
3: from(X) -> cons(X)
4: add(0,X) -> X
5: add(s,Y) -> s
6: len(nil) -> 0
7: len(cons(X)) -> s

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