Consider the TRS R consisting of the rewrite rules

1: active(f(x)) -> mark(x)
2: top(active(c)) -> top(mark(c))
3: top(mark(x)) -> top(check(x))
4: check(f(x)) -> f(check(x))
5: check(x) -> start(match(f(X),x))
6: match(f(x),f(y)) -> f(match(x,y))
7: match(X,x) -> proper(x)
8: proper(c) -> ok(c)
9: proper(f(x)) -> f(proper(x))
10: f(ok(x)) -> ok(f(x))
11: start(ok(x)) -> found(x)
12: f(found(x)) -> found(f(x))
13: top(found(x)) -> top(active(x))
14: active(f(x)) -> f(active(x))
15: f(mark(x)) -> mark(f(x))

There are 20 dependency pairs:

16: TOP(active(c)) -> TOP(mark(c))
17: TOP(mark(x)) -> TOP(check(x))
18: TOP(mark(x)) -> CHECK(x)
19: CHECK(f(x)) -> F(check(x))
20: CHECK(f(x)) -> CHECK(x)
21: CHECK(x) -> START(match(f(X),x))
22: CHECK(x) -> MATCH(f(X),x)
23: CHECK(x) -> F(X)
24: MATCH(f(x),f(y)) -> F(match(x,y))
25: MATCH(f(x),f(y)) -> MATCH(x,y)
26: MATCH(X,x) -> PROPER(x)
27: PROPER(f(x)) -> F(proper(x))
28: PROPER(f(x)) -> PROPER(x)
29: F(ok(x)) -> F(x)
30: F(found(x)) -> F(x)
31: TOP(found(x)) -> TOP(active(x))
32: TOP(found(x)) -> ACTIVE(x)
33: ACTIVE(f(x)) -> F(active(x))
34: ACTIVE(f(x)) -> ACTIVE(x)
35: F(mark(x)) -> F(x)

The approximated dependency graph contains 6 SCCs:
{29,30,35},
{34},
{28},
{25},
{20}
and {16,17,31}.

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

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

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

- Consider the SCC {25}.
There are no usable rules.
By taking the polynomial interpretation
[f](x) = x + 1
and [MATCH](x,y) = x + y + 1,
rule 25
is strictly decreasing.

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

- Consider the SCC {16,17,31}.
The usable rules are {1,4-12,14,15}.
By taking the polynomial interpretation
[check](x) = [f](x) = [mark](x) = 0,
[X] = [c] = [proper](x) = 1,
[active](x) = [found](x) = [match](x,y) = [ok](x) = [start](x) = x
and [TOP](x) = x + 1,
the rules in {1,4-8,10-12,14,15,17,31}
are weakly decreasing and
the rules in {9,16}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {17,31}.
By taking the polynomial interpretation
[X] = [c] = 1,
[active](x) = [ok](x) = [proper](x) = x,
[check](x) = [f](x) = [found](x) = [mark](x) = [start](x) = [TOP](x) = x + 1
and [match](x,y) = y,
the rules in {1,4-12,14,15,17}
are weakly decreasing and
rule 31
is strictly decreasing.
There is one new SCC.

- Consider the SCC {17}.
The usable rules are {4-12,15}.
By taking the polynomial interpretation
[X] = [c] = 1,
[check](x) = [found](x) = [ok](x) = [proper](x) = [start](x) = x,
[f](x) = [mark](x) = [TOP](x) = x + 1
and [match](x,y) = y,
the rules in {4-12,15}
are weakly decreasing and
rule 17
is strictly decreasing.



Hence the TRS is terminating.