Consider the TRS R consisting of the rewrite rules

1: a__eq(0,0) -> true
2: a__eq(s(X),s(Y)) -> a__eq(X,Y)
3: a__eq(X,Y) -> false
4: a__inf(X) -> cons(X,inf(s(X)))
5: a__take(0,X) -> nil
6: a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
7: a__length(nil) -> 0
8: a__length(cons(X,L)) -> s(length(L))
9: mark(eq(X1,X2)) -> a__eq(X1,X2)
10: mark(inf(X)) -> a__inf(mark(X))
11: mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
12: mark(length(X)) -> a__length(mark(X))
13: mark(0) -> 0
14: mark(true) -> true
15: mark(s(X)) -> s(X)
16: mark(false) -> false
17: mark(cons(X1,X2)) -> cons(X1,X2)
18: mark(nil) -> nil
19: a__eq(X1,X2) -> eq(X1,X2)
20: a__inf(X) -> inf(X)
21: a__take(X1,X2) -> take(X1,X2)
22: a__length(X) -> length(X)

There are 9 dependency pairs:

23: A__EQ(s(X),s(Y)) -> A__EQ(X,Y)
24: MARK(eq(X1,X2)) -> A__EQ(X1,X2)
25: MARK(inf(X)) -> A__INF(mark(X))
26: MARK(inf(X)) -> MARK(X)
27: MARK(take(X1,X2)) -> A__TAKE(mark(X1),mark(X2))
28: MARK(take(X1,X2)) -> MARK(X1)
29: MARK(take(X1,X2)) -> MARK(X2)
30: MARK(length(X)) -> A__LENGTH(mark(X))
31: MARK(length(X)) -> MARK(X)

The approximated dependency graph contains 2 SCCs:
{23}
and {26,28,29,31}.

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

- Consider the SCC {26,28,29,31}.
There are no usable rules.
By taking the polynomial interpretation
[inf](x) = [length](x) = [MARK](x) = x + 1
and [take](x,y) = x + y + 1,
the rules in {26,28,29,31}
are strictly decreasing.

Hence the TRS is terminating.