YES TRS: active(f(f(X))) -> mark(c(f(g(f(X))))) active(c(X)) -> mark(d(X)) active(h(X)) -> mark(c(d(X))) active(f(X)) -> f(active(X)) active(h(X)) -> h(active(X)) f(mark(X)) -> mark(f(X)) h(mark(X)) -> mark(h(X)) proper(f(X)) -> f(proper(X)) proper(c(X)) -> c(proper(X)) proper(g(X)) -> g(proper(X)) proper(d(X)) -> d(proper(X)) proper(h(X)) -> h(proper(X)) f(ok(X)) -> ok(f(X)) c(ok(X)) -> ok(c(X)) g(ok(X)) -> ok(g(X)) d(ok(X)) -> ok(d(X)) h(ok(X)) -> ok(h(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) linear polynomial interpretations on N: active_A(x1) = x1 + 10 active#_A(x1) = x1 + 13 f_A(x1) = x1 + 1 f#_A(x1) = x1 + 3 mark_A(x1) = x1 + 4 mark#_A(x1) = x1 + 5 c_A(x1) = x1 + 3 c#_A(x1) = x1 + 5 g_A(x1) = x1 + 3 g#_A(x1) = x1 + 5 d_A(x1) = x1 + 1 d#_A(x1) = x1 + 1 h_A(x1) = x1 h#_A(x1) = x1 + 2 proper_A(x1) = x1 + 1 proper#_A(x1) = x1 + 4 ok_A(x1) = x1 + 11 ok#_A(x1) = 0 top_A(x1) = 0 top#_A(x1) = x1 + 5 precedence: top > active > g > f > mark > proper > h > d > ok > c