Consider the TRS R consisting of the rewrite rules

1: and(true,X) -> activate(X)
2: and(false,Y) -> false
3: if(true,X,Y) -> activate(X)
4: if(false,X,Y) -> activate(Y)
5: add(0,X) -> activate(X)
6: add(s(X),Y) -> s(n__add(activate(X),activate(Y)))
7: first(0,X) -> nil
8: first(s(X),cons(Y,Z)) -> cons(activate(Y),n__first(activate(X),activate(Z)))
9: from(X) -> cons(activate(X),n__from(n__s(activate(X))))
10: add(X1,X2) -> n__add(X1,X2)
11: first(X1,X2) -> n__first(X1,X2)
12: from(X) -> n__from(X)
13: s(X) -> n__s(X)
14: activate(n__add(X1,X2)) -> add(X1,X2)
15: activate(n__first(X1,X2)) -> first(X1,X2)
16: activate(n__from(X)) -> from(X)
17: activate(n__s(X)) -> s(X)
18: activate(X) -> X

There are 15 dependency pairs:

19: AND(true,X) -> ACTIVATE(X)
20: IF(true,X,Y) -> ACTIVATE(X)
21: IF(false,X,Y) -> ACTIVATE(Y)
22: ADD(0,X) -> ACTIVATE(X)
23: ADD(s(X),Y) -> S(n__add(activate(X),activate(Y)))
24: ADD(s(X),Y) -> ACTIVATE(X)
25: ADD(s(X),Y) -> ACTIVATE(Y)
26: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Y)
27: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(X)
28: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
29: FROM(X) -> ACTIVATE(X)
30: ACTIVATE(n__add(X1,X2)) -> ADD(X1,X2)
31: ACTIVATE(n__first(X1,X2)) -> FIRST(X1,X2)
32: ACTIVATE(n__from(X)) -> FROM(X)
33: ACTIVATE(n__s(X)) -> S(X)

The approximated dependency graph contains one SCC:
{22,24-32}.

- Consider the SCC {22,24-32}.
There are no usable rules.
By taking the polynomial interpretation
[0] = 1,
[ACTIVATE](x) = [FROM](x) = [n__from](x) = [s](x) = x + 1
and [ADD](x,y) = [cons](x,y) = [FIRST](x,y) = [n__add](x,y) = [n__first](x,y) = x + y + 1,
rule 29
is weakly decreasing and
the rules in {22,24-28,30-32}
are strictly decreasing.

Hence the TRS is terminating.