Consider the TRS R consisting of the rewrite rules

1: active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
2: active(from(X)) -> mark(cons(X,from(s(X))))
3: active(2nd(X)) -> 2nd(active(X))
4: active(cons(X1,X2)) -> cons(active(X1),X2)
5: active(from(X)) -> from(active(X))
6: active(s(X)) -> s(active(X))
7: 2nd(mark(X)) -> mark(2nd(X))
8: cons(mark(X1),X2) -> mark(cons(X1,X2))
9: from(mark(X)) -> mark(from(X))
10: s(mark(X)) -> mark(s(X))
11: proper(2nd(X)) -> 2nd(proper(X))
12: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
13: proper(from(X)) -> from(proper(X))
14: proper(s(X)) -> s(proper(X))
15: 2nd(ok(X)) -> ok(2nd(X))
16: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
17: from(ok(X)) -> ok(from(X))
18: s(ok(X)) -> ok(s(X))
19: top(mark(X)) -> top(proper(X))
20: top(ok(X)) -> top(active(X))

There are 32 dependency pairs:

21: ACTIVE(from(X)) -> CONS(X,from(s(X)))
22: ACTIVE(from(X)) -> FROM(s(X))
23: ACTIVE(from(X)) -> S(X)
24: ACTIVE(2nd(X)) -> 2nd#(active(X))
25: ACTIVE(2nd(X)) -> ACTIVE(X)
26: ACTIVE(cons(X1,X2)) -> CONS(active(X1),X2)
27: ACTIVE(cons(X1,X2)) -> ACTIVE(X1)
28: ACTIVE(from(X)) -> FROM(active(X))
29: ACTIVE(from(X)) -> ACTIVE(X)
30: ACTIVE(s(X)) -> S(active(X))
31: ACTIVE(s(X)) -> ACTIVE(X)
32: 2nd#(mark(X)) -> 2nd#(X)
33: CONS(mark(X1),X2) -> CONS(X1,X2)
34: FROM(mark(X)) -> FROM(X)
35: S(mark(X)) -> S(X)
36: PROPER(2nd(X)) -> 2nd#(proper(X))
37: PROPER(2nd(X)) -> PROPER(X)
38: PROPER(cons(X1,X2)) -> CONS(proper(X1),proper(X2))
39: PROPER(cons(X1,X2)) -> PROPER(X1)
40: PROPER(cons(X1,X2)) -> PROPER(X2)
41: PROPER(from(X)) -> FROM(proper(X))
42: PROPER(from(X)) -> PROPER(X)
43: PROPER(s(X)) -> S(proper(X))
44: PROPER(s(X)) -> PROPER(X)
45: 2nd#(ok(X)) -> 2nd#(X)
46: CONS(ok(X1),ok(X2)) -> CONS(X1,X2)
47: FROM(ok(X)) -> FROM(X)
48: S(ok(X)) -> S(X)
49: TOP(mark(X)) -> TOP(proper(X))
50: TOP(mark(X)) -> PROPER(X)
51: TOP(ok(X)) -> TOP(active(X))
52: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 7 SCCs:
{32,45},
{33,46},
{34,47},
{35,48},
{37,39,40,42,44},
{25,27,29,31}
and {49,51}.

- Consider the SCC {32,45}.
There are no usable rules.
By taking the polynomial interpretation
[2nd#](x) = [mark](x) = [ok](x) = x + 1,
the rules in {32,45}
are strictly decreasing.

- Consider the SCC {33,46}.
There are no usable rules.
By taking the polynomial interpretation
[mark](x) = [ok](x) = x + 1
and [CONS](x,y) = x + y + 1,
the rules in {33,46}
are strictly decreasing.

- Consider the SCC {34,47}.
There are no usable rules.
By taking the polynomial interpretation
[FROM](x) = [mark](x) = [ok](x) = x + 1,
the rules in {34,47}
are strictly decreasing.

- Consider the SCC {35,48}.
There are no usable rules.
By taking the polynomial interpretation
[mark](x) = [ok](x) = [S](x) = x + 1,
the rules in {35,48}
are strictly decreasing.

- Consider the SCC {37,39,40,42,44}.
There are no usable rules.
By taking the polynomial interpretation
[2nd](x) = [from](x) = [PROPER](x) = [s](x) = x + 1
and [cons](x,y) = x + y + 1,
the rules in {37,39,40,42,44}
are strictly decreasing.

- Consider the SCC {25,27,29,31}.
There are no usable rules.
By taking the polynomial interpretation
[2nd](x) = [ACTIVE](x) = [from](x) = [s](x) = x + 1
and [cons](x,y) = x + y + 1,
the rules in {25,27,29,31}
are strictly decreasing.

- Consider the SCC {49,51}.
The usable rules are {1-18}.
By taking the polynomial interpretation
[proper](x) = 0,
[mark](x) = 1,
[2nd](x) = [from](x) = [s](x) = x,
[active](x) = [ok](x) = [TOP](x) = x + 1
and [cons](x,y) = x + y,
the rules in {1-15,17,18,51}
are weakly decreasing and
the rules in {16,49}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {51}.
The usable rules are {1-10,15-18}.
By taking the polynomial interpretation
[mark](x) = 1,
[active](x) = x,
[2nd](x) = [from](x) = [ok](x) = [s](x) = [TOP](x) = x + 1
and [cons](x,y) = x + y + 1,
the rules in {2-6,15,17,18}
are weakly decreasing and
the rules in {1,7-10,16,51}
are strictly decreasing.


Hence the TRS is terminating.