Consider the TRS R consisting of the rewrite rules

1: active(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
2: active(f(X1,X2)) -> f(active(X1),X2)
3: active(g(X)) -> g(active(X))
4: f(mark(X1),X2) -> mark(f(X1,X2))
5: g(mark(X)) -> mark(g(X))
6: proper(f(X1,X2)) -> f(proper(X1),proper(X2))
7: proper(g(X)) -> g(proper(X))
8: f(ok(X1),ok(X2)) -> ok(f(X1,X2))
9: g(ok(X)) -> ok(g(X))
10: top(mark(X)) -> top(proper(X))
11: top(ok(X)) -> top(active(X))

There are 18 dependency pairs:

12: ACTIVE(f(g(X),Y)) -> F(X,f(g(X),Y))
13: ACTIVE(f(X1,X2)) -> F(active(X1),X2)
14: ACTIVE(f(X1,X2)) -> ACTIVE(X1)
15: ACTIVE(g(X)) -> G(active(X))
16: ACTIVE(g(X)) -> ACTIVE(X)
17: F(mark(X1),X2) -> F(X1,X2)
18: G(mark(X)) -> G(X)
19: PROPER(f(X1,X2)) -> F(proper(X1),proper(X2))
20: PROPER(f(X1,X2)) -> PROPER(X1)
21: PROPER(f(X1,X2)) -> PROPER(X2)
22: PROPER(g(X)) -> G(proper(X))
23: PROPER(g(X)) -> PROPER(X)
24: F(ok(X1),ok(X2)) -> F(X1,X2)
25: G(ok(X)) -> G(X)
26: TOP(mark(X)) -> TOP(proper(X))
27: TOP(mark(X)) -> PROPER(X)
28: TOP(ok(X)) -> TOP(active(X))
29: TOP(ok(X)) -> ACTIVE(X)

The approximated dependency graph contains 5 SCCs:
{17,24},
{18,25},
{14,16},
{20,21,23}
and {26,28}.

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

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

- Consider the SCC {14,16}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVE](x) = [g](x) = x + 1
and [f](x,y) = x + y + 1,
the rules in {14,16}
are strictly decreasing.

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

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

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


Hence the TRS is terminating.