Consider the TRS R consisting of the rewrite rules

1: active(fst(0,Z)) -> mark(nil)
2: active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
3: active(from(X)) -> mark(cons(X,from(s(X))))
4: active(add(0,X)) -> mark(X)
5: active(add(s(X),Y)) -> mark(s(add(X,Y)))
6: active(len(nil)) -> mark(0)
7: active(len(cons(X,Z))) -> mark(s(len(Z)))
8: active(cons(X1,X2)) -> cons(active(X1),X2)
9: active(fst(X1,X2)) -> fst(active(X1),X2)
10: active(fst(X1,X2)) -> fst(X1,active(X2))
11: active(from(X)) -> from(active(X))
12: active(add(X1,X2)) -> add(active(X1),X2)
13: active(add(X1,X2)) -> add(X1,active(X2))
14: active(len(X)) -> len(active(X))
15: cons(mark(X1),X2) -> mark(cons(X1,X2))
16: fst(mark(X1),X2) -> mark(fst(X1,X2))
17: fst(X1,mark(X2)) -> mark(fst(X1,X2))
18: from(mark(X)) -> mark(from(X))
19: add(mark(X1),X2) -> mark(add(X1,X2))
20: add(X1,mark(X2)) -> mark(add(X1,X2))
21: len(mark(X)) -> mark(len(X))
22: proper(0) -> ok(0)
23: proper(s(X)) -> s(proper(X))
24: proper(nil) -> ok(nil)
25: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
26: proper(fst(X1,X2)) -> fst(proper(X1),proper(X2))
27: proper(from(X)) -> from(proper(X))
28: proper(add(X1,X2)) -> add(proper(X1),proper(X2))
29: proper(len(X)) -> len(proper(X))
30: s(ok(X)) -> ok(s(X))
31: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
32: fst(ok(X1),ok(X2)) -> ok(fst(X1,X2))
33: from(ok(X)) -> ok(from(X))
34: add(ok(X1),ok(X2)) -> ok(add(X1,X2))
35: len(ok(X)) -> ok(len(X))
36: top(mark(X)) -> top(proper(X))
37: top(ok(X)) -> top(active(X))

There are 55 dependency pairs:

38: ACTIVE(fst(s(X),cons(Y,Z))) -> CONS(Y,fst(X,Z))
39: ACTIVE(fst(s(X),cons(Y,Z))) -> FST(X,Z)
40: ACTIVE(from(X)) -> CONS(X,from(s(X)))
41: ACTIVE(from(X)) -> FROM(s(X))
42: ACTIVE(from(X)) -> S(X)
43: ACTIVE(add(s(X),Y)) -> S(add(X,Y))
44: ACTIVE(add(s(X),Y)) -> ADD(X,Y)
45: ACTIVE(len(cons(X,Z))) -> S(len(Z))
46: ACTIVE(len(cons(X,Z))) -> LEN(Z)
47: ACTIVE(cons(X1,X2)) -> CONS(active(X1),X2)
48: ACTIVE(cons(X1,X2)) -> ACTIVE(X1)
49: ACTIVE(fst(X1,X2)) -> FST(active(X1),X2)
50: ACTIVE(fst(X1,X2)) -> ACTIVE(X1)
51: ACTIVE(fst(X1,X2)) -> FST(X1,active(X2))
52: ACTIVE(fst(X1,X2)) -> ACTIVE(X2)
53: ACTIVE(from(X)) -> FROM(active(X))
54: ACTIVE(from(X)) -> ACTIVE(X)
55: ACTIVE(add(X1,X2)) -> ADD(active(X1),X2)
56: ACTIVE(add(X1,X2)) -> ACTIVE(X1)
57: ACTIVE(add(X1,X2)) -> ADD(X1,active(X2))
58: ACTIVE(add(X1,X2)) -> ACTIVE(X2)
59: ACTIVE(len(X)) -> LEN(active(X))
60: ACTIVE(len(X)) -> ACTIVE(X)
61: CONS(mark(X1),X2) -> CONS(X1,X2)
62: FST(mark(X1),X2) -> FST(X1,X2)
63: FST(X1,mark(X2)) -> FST(X1,X2)
64: FROM(mark(X)) -> FROM(X)
65: ADD(mark(X1),X2) -> ADD(X1,X2)
66: ADD(X1,mark(X2)) -> ADD(X1,X2)
67: LEN(mark(X)) -> LEN(X)
68: PROPER(s(X)) -> S(proper(X))
69: PROPER(s(X)) -> PROPER(X)
70: PROPER(cons(X1,X2)) -> CONS(proper(X1),proper(X2))
71: PROPER(cons(X1,X2)) -> PROPER(X1)
72: PROPER(cons(X1,X2)) -> PROPER(X2)
73: PROPER(fst(X1,X2)) -> FST(proper(X1),proper(X2))
74: PROPER(fst(X1,X2)) -> PROPER(X1)
75: PROPER(fst(X1,X2)) -> PROPER(X2)
76: PROPER(from(X)) -> FROM(proper(X))
77: PROPER(from(X)) -> PROPER(X)
78: PROPER(add(X1,X2)) -> ADD(proper(X1),proper(X2))
79: PROPER(add(X1,X2)) -> PROPER(X1)
80: PROPER(add(X1,X2)) -> PROPER(X2)
81: PROPER(len(X)) -> LEN(proper(X))
82: PROPER(len(X)) -> PROPER(X)
83: S(ok(X)) -> S(X)
84: CONS(ok(X1),ok(X2)) -> CONS(X1,X2)
85: FST(ok(X1),ok(X2)) -> FST(X1,X2)
86: FROM(ok(X)) -> FROM(X)
87: ADD(ok(X1),ok(X2)) -> ADD(X1,X2)
88: LEN(ok(X)) -> LEN(X)
89: TOP(mark(X)) -> TOP(proper(X))
90: TOP(mark(X)) -> PROPER(X)
91: TOP(ok(X)) -> TOP(active(X))
92: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 9 SCCs:
{65,66,87},
{61,84},
{64,86},
{62,63,85},
{67,88},
{83},
{69,71,72,74,75,77,79,80,82},
{48,50,52,54,56,58,60}
and {89,91}.

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

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

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

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

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

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

- Consider the SCC {69,71,72,74,75,77,79,80,82}.
There are no usable rules.
By taking the polynomial interpretation
[from](x) = [len](x) = [PROPER](x) = [s](x) = x + 1
and [add](x,y) = [cons](x,y) = [fst](x,y) = x + y + 1,
the rules in {69,71,72,74,75,77,79,80,82}
are strictly decreasing.

- Consider the SCC {48,50,52,54,56,58,60}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVE](x) = [from](x) = [len](x) = x + 1
and [add](x,y) = [cons](x,y) = [fst](x,y) = x + y + 1,
the rules in {48,50,52,54,56,58,60}
are strictly decreasing.

- Consider the SCC {89,91}.
The usable rules are {1-35}.
By taking the polynomial interpretation
[s](x) = 0,
[0] = [nil] = 1,
[active](x) = [cons](x,y) = [ok](x) = [proper](x) = x,
[from](x) = [len](x) = [mark](x) = [TOP](x) = x + 1
and [add](x,y) = [fst](x,y) = x + y + 1,
the rules in {1-3,5-35,91}
are weakly decreasing and
the rules in {4,89}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {91}.
The usable rules are {1-21,30-35}.
By taking the polynomial interpretation
[0] = [mark](x) = [nil] = 1,
[active](x) = x,
[from](x) = [len](x) = [ok](x) = [s](x) = [TOP](x) = x + 1
and [add](x,y) = [cons](x,y) = [fst](x,y) = x + y + 1,
the rules in {3,8-14,30,33,35}
are weakly decreasing and
the rules in {1,2,4-7,15-21,31,32,34,91}
are strictly decreasing.


Hence the TRS is terminating.