Consider the TRS R consisting of the rewrite rules

1: active(f(X)) -> mark(g(h(f(X))))
2: active(f(X)) -> f(active(X))
3: active(h(X)) -> h(active(X))
4: f(mark(X)) -> mark(f(X))
5: h(mark(X)) -> mark(h(X))
6: proper(f(X)) -> f(proper(X))
7: proper(g(X)) -> g(proper(X))
8: proper(h(X)) -> h(proper(X))
9: f(ok(X)) -> ok(f(X))
10: g(ok(X)) -> ok(g(X))
11: h(ok(X)) -> ok(h(X))
12: top(mark(X)) -> top(proper(X))
13: top(ok(X)) -> top(active(X))

There are 21 dependency pairs:

14: ACTIVE(f(X)) -> G(h(f(X)))
15: ACTIVE(f(X)) -> H(f(X))
16: ACTIVE(f(X)) -> F(active(X))
17: ACTIVE(f(X)) -> ACTIVE(X)
18: ACTIVE(h(X)) -> H(active(X))
19: ACTIVE(h(X)) -> ACTIVE(X)
20: F(mark(X)) -> F(X)
21: H(mark(X)) -> H(X)
22: PROPER(f(X)) -> F(proper(X))
23: PROPER(f(X)) -> PROPER(X)
24: PROPER(g(X)) -> G(proper(X))
25: PROPER(g(X)) -> PROPER(X)
26: PROPER(h(X)) -> H(proper(X))
27: PROPER(h(X)) -> PROPER(X)
28: F(ok(X)) -> F(X)
29: G(ok(X)) -> G(X)
30: H(ok(X)) -> H(X)
31: TOP(mark(X)) -> TOP(proper(X))
32: TOP(mark(X)) -> PROPER(X)
33: TOP(ok(X)) -> TOP(active(X))
34: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 6 SCCs:
{20,28},
{29},
{21,30},
{17,19},
{23,25,27}
and {31,33}.

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

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

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

- Consider the SCC {17,19}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVE](x) = [f](x) = [h](x) = x + 1,
the rules in {17,19}
are strictly decreasing.

- Consider the SCC {23,25,27}.
There are no usable rules.
By taking the polynomial interpretation
[f](x) = [g](x) = [h](x) = [PROPER](x) = x + 1,
the rules in {23,25,27}
are strictly decreasing.

- Consider the SCC {31,33}.
The usable rules are {1-11}.
By taking the polynomial interpretation
[g](x) = [h](x) = [proper](x) = x
and [active](x) = [f](x) = [mark](x) = [ok](x) = [TOP](x) = x + 1,
the rules in {1-11,33}
are weakly decreasing and
rule 31
is strictly decreasing.
There is one new SCC.

- Consider the SCC {33}.
The usable rules are {1-5,9-11}.
By taking the polynomial interpretation
[active](x) = [g](x) = [h](x) = [mark](x) = x
and [f](x) = [ok](x) = [TOP](x) = x + 1,
the rules in {1-5,9-11}
are weakly decreasing and
rule 33
is strictly decreasing.


Hence the TRS is terminating.