Consider the TRS R consisting of the rewrite rules

1: fst(0,Z) -> nil
2: fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
3: from(X) -> cons(X,n__from(s(X)))
4: add(0,X) -> X
5: add(s(X),Y) -> s(n__add(activate(X),Y))
6: len(nil) -> 0
7: len(cons(X,Z)) -> s(n__len(activate(Z)))
8: fst(X1,X2) -> n__fst(X1,X2)
9: from(X) -> n__from(X)
10: add(X1,X2) -> n__add(X1,X2)
11: len(X) -> n__len(X)
12: activate(n__fst(X1,X2)) -> fst(X1,X2)
13: activate(n__from(X)) -> from(X)
14: activate(n__add(X1,X2)) -> add(X1,X2)
15: activate(n__len(X)) -> len(X)
16: activate(X) -> X

There are 8 dependency pairs:

17: FST(s(X),cons(Y,Z)) -> ACTIVATE(X)
18: FST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
19: ADD(s(X),Y) -> ACTIVATE(X)
20: LEN(cons(X,Z)) -> ACTIVATE(Z)
21: ACTIVATE(n__fst(X1,X2)) -> FST(X1,X2)
22: ACTIVATE(n__from(X)) -> FROM(X)
23: ACTIVATE(n__add(X1,X2)) -> ADD(X1,X2)
24: ACTIVATE(n__len(X)) -> LEN(X)

The approximated dependency graph contains one SCC:
{17-21,23,24}.

- Consider the SCC {17-21,23,24}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [LEN](x) = [n__len](x) = [s](x) = x + 1
and [ADD](x,y) = [cons](x,y) = [FST](x,y) = [n__add](x,y) = [n__fst](x,y) = x + y + 1,
the rules in {17-21,23,24}
are strictly decreasing.

Hence the TRS is terminating.