Consider the TRS R consisting of the rewrite rules

1: active(c) -> mark(f(g(c)))
2: active(f(g(X))) -> mark(g(X))
3: proper(c) -> ok(c)
4: proper(f(X)) -> f(proper(X))
5: proper(g(X)) -> g(proper(X))
6: f(ok(X)) -> ok(f(X))
7: g(ok(X)) -> ok(g(X))
8: top(mark(X)) -> top(proper(X))
9: top(ok(X)) -> top(active(X))

There are 12 dependency pairs:

10: ACTIVE(c) -> F(g(c))
11: ACTIVE(c) -> G(c)
12: PROPER(f(X)) -> F(proper(X))
13: PROPER(f(X)) -> PROPER(X)
14: PROPER(g(X)) -> G(proper(X))
15: PROPER(g(X)) -> PROPER(X)
16: F(ok(X)) -> F(X)
17: G(ok(X)) -> G(X)
18: TOP(mark(X)) -> TOP(proper(X))
19: TOP(mark(X)) -> PROPER(X)
20: TOP(ok(X)) -> TOP(active(X))
21: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 4 SCCs:
{16},
{17},
{13,15}
and {18,20}.

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

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

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

- Consider the SCC {18,20}.
The usable rules are {1-7}.
By taking the polynomial interpretation
[g](x) = 0,
[proper](x) = 2x,
[mark](x) = 2x + 1,
[c] = 3,
[f](x) = 3x + 1,
[active](x) = [ok](x) = x
and [TOP](x) = x + 1,
the rules in {1,2,5-7,20}
are weakly decreasing and
the rules in {3,4,18}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {20}.
The usable rules are {1,2,6,7}.
By taking the polynomial interpretation
[c] = 1,
[active](x) = [f](x) = [g](x) = [mark](x) = x
and [ok](x) = [TOP](x) = x + 1,
the rules in {1,2,6,7}
are weakly decreasing and
rule 20
is strictly decreasing.


Hence the TRS is terminating.