Consider the TRS R consisting of the rewrite rules

1: a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N)))
2: a__sqr(0) -> 0
3: a__sqr(s(X)) -> s(add(sqr(X),dbl(X)))
4: a__dbl(0) -> 0
5: a__dbl(s(X)) -> s(s(dbl(X)))
6: a__add(0,X) -> mark(X)
7: a__add(s(X),Y) -> s(add(X,Y))
8: a__first(0,X) -> nil
9: a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
10: mark(terms(X)) -> a__terms(mark(X))
11: mark(sqr(X)) -> a__sqr(mark(X))
12: mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
13: mark(dbl(X)) -> a__dbl(mark(X))
14: mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
15: mark(cons(X1,X2)) -> cons(mark(X1),X2)
16: mark(recip(X)) -> recip(mark(X))
17: mark(s(X)) -> s(X)
18: mark(0) -> 0
19: mark(nil) -> nil
20: a__terms(X) -> terms(X)
21: a__sqr(X) -> sqr(X)
22: a__add(X1,X2) -> add(X1,X2)
23: a__dbl(X) -> dbl(X)
24: a__first(X1,X2) -> first(X1,X2)

There are 18 dependency pairs:

25: A__TERMS(N) -> A__SQR(mark(N))
26: A__TERMS(N) -> MARK(N)
27: A__ADD(0,X) -> MARK(X)
28: A__FIRST(s(X),cons(Y,Z)) -> MARK(Y)
29: MARK(terms(X)) -> A__TERMS(mark(X))
30: MARK(terms(X)) -> MARK(X)
31: MARK(sqr(X)) -> A__SQR(mark(X))
32: MARK(sqr(X)) -> MARK(X)
33: MARK(add(X1,X2)) -> A__ADD(mark(X1),mark(X2))
34: MARK(add(X1,X2)) -> MARK(X1)
35: MARK(add(X1,X2)) -> MARK(X2)
36: MARK(dbl(X)) -> A__DBL(mark(X))
37: MARK(dbl(X)) -> MARK(X)
38: MARK(first(X1,X2)) -> A__FIRST(mark(X1),mark(X2))
39: MARK(first(X1,X2)) -> MARK(X1)
40: MARK(first(X1,X2)) -> MARK(X2)
41: MARK(cons(X1,X2)) -> MARK(X1)
42: MARK(recip(X)) -> MARK(X)

The approximated dependency graph contains one SCC:
{26-30,32-35,37-42}.

- Consider the SCC {26-30,32-35,37-42}.
By taking the polynomial interpretation
[0] = [nil] = [s](x) = 1,
[cons](x,y) = [mark](x) = [recip](x) = x,
[a__dbl](x) = [a__sqr](x) = [a__terms](x) = [A__TERMS](x) = [dbl](x) = [MARK](x) = [sqr](x) = [terms](x) = x + 1
and [a__add](x,y) = [A__ADD](x,y) = [a__first](x,y) = [A__FIRST](x,y) = [add](x,y) = [first](x,y) = x + y + 1,
the rules in {1,10-24,26,41,42}
are weakly decreasing and
the rules in {2-9,27-30,32-35,37-40}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {41,42}.
There are no usable rules.
By taking the polynomial interpretation
[MARK](x) = [recip](x) = x + 1
and [cons](x,y) = x + y + 1,
the rules in {41,42}
are strictly decreasing.


Hence the TRS is terminating.