Consider the TRS R consisting of the rewrite rules

1: a__from(X) -> cons(mark(X),from(s(X)))
2: a__length(nil) -> 0
3: a__length(cons(X,Y)) -> s(a__length1(Y))
4: a__length1(X) -> a__length(X)
5: mark(from(X)) -> a__from(mark(X))
6: mark(length(X)) -> a__length(X)
7: mark(length1(X)) -> a__length1(X)
8: mark(cons(X1,X2)) -> cons(mark(X1),X2)
9: mark(s(X)) -> s(mark(X))
10: mark(nil) -> nil
11: mark(0) -> 0
12: a__from(X) -> from(X)
13: a__length(X) -> length(X)
14: a__length1(X) -> length1(X)

There are 9 dependency pairs:

15: A__FROM(X) -> MARK(X)
16: A__LENGTH(cons(X,Y)) -> A__LENGTH1(Y)
17: A__LENGTH1(X) -> A__LENGTH(X)
18: MARK(from(X)) -> A__FROM(mark(X))
19: MARK(from(X)) -> MARK(X)
20: MARK(length(X)) -> A__LENGTH(X)
21: MARK(length1(X)) -> A__LENGTH1(X)
22: MARK(cons(X1,X2)) -> MARK(X1)
23: MARK(s(X)) -> MARK(X)

The approximated dependency graph contains 2 SCCs:
{16,17}
and {15,18,19,22,23}.

- Consider the SCC {16,17}.
There are no usable rules.
By taking the polynomial interpretation
[A__LENGTH](x) = [A__LENGTH1](x) = x + 1
and [cons](x,y) = x + y + 1,
rule 17
is weakly decreasing and
rule 16
is strictly decreasing.

- Consider the SCC {15,18,19,22,23}.
By taking the polynomial interpretation
[0] = [a__length](x) = [a__length1](x) = [length](x) = [length1](x) = [nil] = 1,
[cons](x,y) = [s](x) = x
and [a__from](x) = [A__FROM](x) = [from](x) = [mark](x) = [MARK](x) = x + 1,
the rules in {1-5,8,9,12-15,18,22,23}
are weakly decreasing and
the rules in {6,7,10,11,19}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {15,18,22,23}.
By taking the polynomial interpretation
[0] = [a__length](x) = [a__length1](x) = [length](x) = [length1](x) = [nil] = 1,
[mark](x) = [s](x) = x
and [a__from](x) = [A__FROM](x) = [cons](x,y) = [from](x) = [MARK](x) = x + 1,
the rules in {1-15,23}
are weakly decreasing and
the rules in {18,22}
are strictly decreasing.
There is one new SCC.

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



Hence the TRS is terminating.