Consider the TRS R consisting of the rewrite rules

1: a__nats -> a__adx(a__zeros)
2: a__zeros -> cons(0,zeros)
3: a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
4: a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
5: a__hd(cons(X,Y)) -> mark(X)
6: a__tl(cons(X,Y)) -> mark(Y)
7: mark(nats) -> a__nats
8: mark(adx(X)) -> a__adx(mark(X))
9: mark(zeros) -> a__zeros
10: mark(incr(X)) -> a__incr(mark(X))
11: mark(hd(X)) -> a__hd(mark(X))
12: mark(tl(X)) -> a__tl(mark(X))
13: mark(cons(X1,X2)) -> cons(X1,X2)
14: mark(0) -> 0
15: mark(s(X)) -> s(X)
16: a__nats -> nats
17: a__adx(X) -> adx(X)
18: a__zeros -> zeros
19: a__incr(X) -> incr(X)
20: a__hd(X) -> hd(X)
21: a__tl(X) -> tl(X)

There are 15 dependency pairs:

22: A__NATS -> A__ADX(a__zeros)
23: A__NATS -> A__ZEROS
24: A__ADX(cons(X,Y)) -> A__INCR(cons(X,adx(Y)))
25: A__HD(cons(X,Y)) -> MARK(X)
26: A__TL(cons(X,Y)) -> MARK(Y)
27: MARK(nats) -> A__NATS
28: MARK(adx(X)) -> A__ADX(mark(X))
29: MARK(adx(X)) -> MARK(X)
30: MARK(zeros) -> A__ZEROS
31: MARK(incr(X)) -> A__INCR(mark(X))
32: MARK(incr(X)) -> MARK(X)
33: MARK(hd(X)) -> A__HD(mark(X))
34: MARK(hd(X)) -> MARK(X)
35: MARK(tl(X)) -> A__TL(mark(X))
36: MARK(tl(X)) -> MARK(X)

The approximated dependency graph contains one SCC:
{25,26,29,32-36}.

- Consider the SCC {25,26,29,32-36}.
By taking the polynomial interpretation
[0] = [a__zeros] = [zeros] = 0,
[a__nats] = [nats] = 1,
[a__incr](x) = [incr](x) = [s](x) = x,
[a__adx](x) = [a__hd](x) = [A__HD](x) = [a__tl](x) = [A__TL](x) = [adx](x) = [hd](x) = [mark](x) = [MARK](x) = [tl](x) = x + 1
and [cons](x,y) = x + y,
the rules in {1-6,8,10-12,16-21,25,26,32,33,35}
are weakly decreasing and
the rules in {7,9,13-15,29,34,36}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {25,26,32,33,35}.
By taking the polynomial interpretation
[0] = [a__zeros] = [zeros] = 0,
[a__nats] = [nats] = 1,
[a__incr](x) = [incr](x) = [mark](x) = [s](x) = x,
[a__adx](x) = [a__hd](x) = [A__HD](x) = [a__tl](x) = [A__TL](x) = [adx](x) = [hd](x) = [MARK](x) = [tl](x) = x + 1
and [cons](x,y) = x + y,
the rules in {1-4,7-21,25,26,32}
are weakly decreasing and
the rules in {5,6,33,35}
are strictly decreasing.
There is one new SCC.

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



Hence the TRS is terminating.