Consider the TRS R consisting of the rewrite rules

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

There are 38 dependency pairs:

26: ACTIVE(first(s(X),cons(Y,Z))) -> CONS(Y,first(X,Z))
27: ACTIVE(first(s(X),cons(Y,Z))) -> FIRST(X,Z)
28: ACTIVE(from(X)) -> CONS(X,from(s(X)))
29: ACTIVE(from(X)) -> FROM(s(X))
30: ACTIVE(from(X)) -> S(X)
31: ACTIVE(first(X1,X2)) -> FIRST(active(X1),X2)
32: ACTIVE(first(X1,X2)) -> ACTIVE(X1)
33: ACTIVE(first(X1,X2)) -> FIRST(X1,active(X2))
34: ACTIVE(first(X1,X2)) -> ACTIVE(X2)
35: ACTIVE(s(X)) -> S(active(X))
36: ACTIVE(s(X)) -> ACTIVE(X)
37: ACTIVE(cons(X1,X2)) -> CONS(active(X1),X2)
38: ACTIVE(cons(X1,X2)) -> ACTIVE(X1)
39: ACTIVE(from(X)) -> FROM(active(X))
40: ACTIVE(from(X)) -> ACTIVE(X)
41: FIRST(mark(X1),X2) -> FIRST(X1,X2)
42: FIRST(X1,mark(X2)) -> FIRST(X1,X2)
43: S(mark(X)) -> S(X)
44: CONS(mark(X1),X2) -> CONS(X1,X2)
45: FROM(mark(X)) -> FROM(X)
46: PROPER(first(X1,X2)) -> FIRST(proper(X1),proper(X2))
47: PROPER(first(X1,X2)) -> PROPER(X1)
48: PROPER(first(X1,X2)) -> PROPER(X2)
49: PROPER(s(X)) -> S(proper(X))
50: PROPER(s(X)) -> PROPER(X)
51: PROPER(cons(X1,X2)) -> CONS(proper(X1),proper(X2))
52: PROPER(cons(X1,X2)) -> PROPER(X1)
53: PROPER(cons(X1,X2)) -> PROPER(X2)
54: PROPER(from(X)) -> FROM(proper(X))
55: PROPER(from(X)) -> PROPER(X)
56: FIRST(ok(X1),ok(X2)) -> FIRST(X1,X2)
57: S(ok(X)) -> S(X)
58: CONS(ok(X1),ok(X2)) -> CONS(X1,X2)
59: FROM(ok(X)) -> FROM(X)
60: TOP(mark(X)) -> TOP(proper(X))
61: TOP(mark(X)) -> PROPER(X)
62: TOP(ok(X)) -> TOP(active(X))
63: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 7 SCCs:
{44,58},
{41,42,56},
{45,59},
{43,57},
{47,48,50,52,53,55},
{32,34,36,38,40}
and {60,62}.

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

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

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

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

- Consider the SCC {47,48,50,52,53,55}.
There are no usable rules.
By taking the polynomial interpretation
[from](x) = [PROPER](x) = [s](x) = x + 1
and [cons](x,y) = [first](x,y) = x + y + 1,
the rules in {47,48,50,52,53,55}
are strictly decreasing.

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

- Consider the SCC {60,62}.
The usable rules are {1-23}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[active](x) = [cons](x,y) = [ok](x) = [proper](x) = x,
[from](x) = [mark](x) = [s](x) = [TOP](x) = x + 1
and [first](x,y) = x + y + 1,
the rules in {1,3-23,62}
are weakly decreasing and
the rules in {2,60}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {62}.
The usable rules are {1-13,20-23}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[active](x) = [cons](x,y) = x,
[from](x) = [mark](x) = [ok](x) = [s](x) = [TOP](x) = x + 1
and [first](x,y) = x + y + 1,
the rules in {1,3-13,21-23}
are weakly decreasing and
the rules in {2,20,62}
are strictly decreasing.


Hence the TRS is terminating.