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(n__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: s(X) -> n__s(X)
11: add(X1,X2) -> n__add(X1,X2)
12: len(X) -> n__len(X)
13: activate(n__fst(X1,X2)) -> fst(activate(X1),activate(X2))
14: activate(n__from(X)) -> from(activate(X))
15: activate(n__s(X)) -> s(X)
16: activate(n__add(X1,X2)) -> add(activate(X1),activate(X2))
17: activate(n__len(X)) -> len(activate(X))
18: activate(X) -> X

There are 17 dependency pairs:

19: FST(s(X),cons(Y,Z)) -> ACTIVATE(X)
20: FST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
21: ADD(s(X),Y) -> S(n__add(activate(X),Y))
22: ADD(s(X),Y) -> ACTIVATE(X)
23: LEN(cons(X,Z)) -> S(n__len(activate(Z)))
24: LEN(cons(X,Z)) -> ACTIVATE(Z)
25: ACTIVATE(n__fst(X1,X2)) -> FST(activate(X1),activate(X2))
26: ACTIVATE(n__fst(X1,X2)) -> ACTIVATE(X1)
27: ACTIVATE(n__fst(X1,X2)) -> ACTIVATE(X2)
28: ACTIVATE(n__from(X)) -> FROM(activate(X))
29: ACTIVATE(n__from(X)) -> ACTIVATE(X)
30: ACTIVATE(n__s(X)) -> S(X)
31: ACTIVATE(n__add(X1,X2)) -> ADD(activate(X1),activate(X2))
32: ACTIVATE(n__add(X1,X2)) -> ACTIVATE(X1)
33: ACTIVATE(n__add(X1,X2)) -> ACTIVATE(X2)
34: ACTIVATE(n__len(X)) -> LEN(activate(X))
35: ACTIVATE(n__len(X)) -> ACTIVATE(X)

The approximated dependency graph contains one SCC:
{19,20,22,24-27,29,31-35}.

- Consider the SCC {19,20,22,24-27,29,31-35}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[activate](x) = [n__s](x) = [s](x) = x,
[ACTIVATE](x) = [from](x) = [len](x) = [LEN](x) = [n__from](x) = [n__len](x) = x + 1,
[add](x,y) = [ADD](x,y) = [fst](x,y) = [FST](x,y) = [n__add](x,y) = [n__fst](x,y) = x + y + 1
and [cons](x,y) = y,
the rules in {2,3,5,7-20,22,24}
are weakly decreasing and
the rules in {1,4,6,25-27,29,31-35}
are strictly decreasing.

Hence the TRS is terminating.