Consider the TRS R consisting of the rewrite rules

1: terms(N) -> cons(recip(sqr(N)),n__terms(n__s(N)))
2: sqr(0) -> 0
3: sqr(s(X)) -> s(add(sqr(X),dbl(X)))
4: dbl(0) -> 0
5: dbl(s(X)) -> s(s(dbl(X)))
6: add(0,X) -> X
7: add(s(X),Y) -> s(add(X,Y))
8: first(0,X) -> nil
9: first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
10: terms(X) -> n__terms(X)
11: s(X) -> n__s(X)
12: first(X1,X2) -> n__first(X1,X2)
13: activate(n__terms(X)) -> terms(activate(X))
14: activate(n__s(X)) -> s(activate(X))
15: activate(n__first(X1,X2)) -> first(activate(X1),activate(X2))
16: activate(X) -> X

There are 18 dependency pairs:

17: TERMS(N) -> SQR(N)
18: SQR(s(X)) -> S(add(sqr(X),dbl(X)))
19: SQR(s(X)) -> ADD(sqr(X),dbl(X))
20: SQR(s(X)) -> SQR(X)
21: SQR(s(X)) -> DBL(X)
22: DBL(s(X)) -> S(s(dbl(X)))
23: DBL(s(X)) -> S(dbl(X))
24: DBL(s(X)) -> DBL(X)
25: ADD(s(X),Y) -> S(add(X,Y))
26: ADD(s(X),Y) -> ADD(X,Y)
27: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
28: ACTIVATE(n__terms(X)) -> TERMS(activate(X))
29: ACTIVATE(n__terms(X)) -> ACTIVATE(X)
30: ACTIVATE(n__s(X)) -> S(activate(X))
31: ACTIVATE(n__s(X)) -> ACTIVATE(X)
32: ACTIVATE(n__first(X1,X2)) -> FIRST(activate(X1),activate(X2))
33: ACTIVATE(n__first(X1,X2)) -> ACTIVATE(X1)
34: ACTIVATE(n__first(X1,X2)) -> ACTIVATE(X2)

The approximated dependency graph contains 4 SCCs:
{26},
{24},
{20}
and {27,29,31-34}.

- Consider the SCC {26}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [ADD](x,y) = x + y + 1,
rule 26
is strictly decreasing.

- Consider the SCC {24}.
There are no usable rules.
By taking the polynomial interpretation
[DBL](x) = [s](x) = x + 1,
rule 24
is strictly decreasing.

- Consider the SCC {20}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = [SQR](x) = x + 1,
rule 20
is strictly decreasing.

- Consider the SCC {27,29,31-34}.
By taking the polynomial interpretation
[recip](x) = 0,
[0] = [nil] = 1,
[activate](x) = [dbl](x) = [n__s](x) = [s](x) = x,
[ACTIVATE](x) = [n__terms](x) = [sqr](x) = [terms](x) = x + 1,
[cons](x,y) = x + y,
[first](x,y) = [FIRST](x,y) = [n__first](x,y) = x + y + 1
and [add](x,y) = y + 1,
the rules in {1,3-5,7,9-16,27,31}
are weakly decreasing and
the rules in {2,6,8,29,32-34}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {31}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [n__s](x) = x + 1,
rule 31
is strictly decreasing.


Hence the TRS is terminating.