Consider the TRS R consisting of the rewrite rules

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

There are 44 dependency pairs:

28: ACTIVE(2nd(cons(X,X1))) -> 2nd#(cons1(X,X1))
29: ACTIVE(2nd(cons(X,X1))) -> CONS1(X,X1)
30: ACTIVE(from(X)) -> CONS(X,from(s(X)))
31: ACTIVE(from(X)) -> FROM(s(X))
32: ACTIVE(from(X)) -> S(X)
33: ACTIVE(2nd(X)) -> 2nd#(active(X))
34: ACTIVE(2nd(X)) -> ACTIVE(X)
35: ACTIVE(cons(X1,X2)) -> CONS(active(X1),X2)
36: ACTIVE(cons(X1,X2)) -> ACTIVE(X1)
37: ACTIVE(from(X)) -> FROM(active(X))
38: ACTIVE(from(X)) -> ACTIVE(X)
39: ACTIVE(s(X)) -> S(active(X))
40: ACTIVE(s(X)) -> ACTIVE(X)
41: ACTIVE(cons1(X1,X2)) -> CONS1(active(X1),X2)
42: ACTIVE(cons1(X1,X2)) -> ACTIVE(X1)
43: ACTIVE(cons1(X1,X2)) -> CONS1(X1,active(X2))
44: ACTIVE(cons1(X1,X2)) -> ACTIVE(X2)
45: 2nd#(mark(X)) -> 2nd#(X)
46: CONS(mark(X1),X2) -> CONS(X1,X2)
47: FROM(mark(X)) -> FROM(X)
48: S(mark(X)) -> S(X)
49: CONS1(mark(X1),X2) -> CONS1(X1,X2)
50: CONS1(X1,mark(X2)) -> CONS1(X1,X2)
51: PROPER(2nd(X)) -> 2nd#(proper(X))
52: PROPER(2nd(X)) -> PROPER(X)
53: PROPER(cons(X1,X2)) -> CONS(proper(X1),proper(X2))
54: PROPER(cons(X1,X2)) -> PROPER(X1)
55: PROPER(cons(X1,X2)) -> PROPER(X2)
56: PROPER(from(X)) -> FROM(proper(X))
57: PROPER(from(X)) -> PROPER(X)
58: PROPER(s(X)) -> S(proper(X))
59: PROPER(s(X)) -> PROPER(X)
60: PROPER(cons1(X1,X2)) -> CONS1(proper(X1),proper(X2))
61: PROPER(cons1(X1,X2)) -> PROPER(X1)
62: PROPER(cons1(X1,X2)) -> PROPER(X2)
63: 2nd#(ok(X)) -> 2nd#(X)
64: CONS(ok(X1),ok(X2)) -> CONS(X1,X2)
65: FROM(ok(X)) -> FROM(X)
66: S(ok(X)) -> S(X)
67: CONS1(ok(X1),ok(X2)) -> CONS1(X1,X2)
68: TOP(mark(X)) -> TOP(proper(X))
69: TOP(mark(X)) -> PROPER(X)
70: TOP(ok(X)) -> TOP(active(X))
71: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 8 SCCs:
{45,63},
{46,64},
{49,50,67},
{47,65},
{48,66},
{52,54,55,57,59,61,62},
{34,36,38,40,42,44}
and {68,70}.

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

- Consider the SCC {46,64}.
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 {46,64}
are strictly decreasing.

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

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

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

- Consider the SCC {52,54,55,57,59,61,62}.
There are no usable rules.
By taking the polynomial interpretation
[2nd](x) = [from](x) = [PROPER](x) = [s](x) = x + 1
and [cons](x,y) = [cons1](x,y) = x + y + 1,
the rules in {52,54,55,57,59,61,62}
are strictly decreasing.

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

- Consider the SCC {68,70}.
The usable rules are {1-25}.
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) = [cons1](x,y) = x + y,
the rules in {1-21,23,24,70}
are weakly decreasing and
the rules in {22,25,68}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {70}.
The usable rules are {1-15,21-25}.
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) = [cons1](x,y) = x + y + 1,
the rules in {3-9,21,23,24}
are weakly decreasing and
the rules in {1,2,10-15,22,25,70}
are strictly decreasing.


Hence the TRS is terminating.