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: half(0) -> 0
11: half(s(0)) -> 0
12: half(s(s(X))) -> s(half(X))
13: half(dbl(X)) -> X
14: terms(X) -> n__terms(X)
15: s(X) -> n__s(X)
16: first(X1,X2) -> n__first(X1,X2)
17: activate(n__terms(X)) -> terms(activate(X))
18: activate(n__s(X)) -> s(activate(X))
19: activate(n__first(X1,X2)) -> first(activate(X1),activate(X2))
20: activate(X) -> X

There are 20 dependency pairs:

21: TERMS(N) -> SQR(N)
22: SQR(s(X)) -> S(add(sqr(X),dbl(X)))
23: SQR(s(X)) -> ADD(sqr(X),dbl(X))
24: SQR(s(X)) -> SQR(X)
25: SQR(s(X)) -> DBL(X)
26: DBL(s(X)) -> S(s(dbl(X)))
27: DBL(s(X)) -> S(dbl(X))
28: DBL(s(X)) -> DBL(X)
29: ADD(s(X),Y) -> S(add(X,Y))
30: ADD(s(X),Y) -> ADD(X,Y)
31: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
32: HALF(s(s(X))) -> S(half(X))
33: HALF(s(s(X))) -> HALF(X)
34: ACTIVATE(n__terms(X)) -> TERMS(activate(X))
35: ACTIVATE(n__terms(X)) -> ACTIVATE(X)
36: ACTIVATE(n__s(X)) -> S(activate(X))
37: ACTIVATE(n__s(X)) -> ACTIVATE(X)
38: ACTIVATE(n__first(X1,X2)) -> FIRST(activate(X1),activate(X2))
39: ACTIVATE(n__first(X1,X2)) -> ACTIVATE(X1)
40: ACTIVATE(n__first(X1,X2)) -> ACTIVATE(X2)

The approximated dependency graph contains 5 SCCs:
{30},
{28},
{33},
{24}
and {31,35,37-40}.

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

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

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

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

- Consider the SCC {31,35,37-40}.
The usable rules are {1-9,14-20}.
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,14-20,31,37}
are weakly decreasing and
the rules in {2,6,8,35,38-40}
are strictly decreasing.
There is one new SCC.

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


Hence the TRS is terminating.