YES TRS: active(f(X)) -> mark(g(h(f(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(g(X)) -> g(proper(X)) proper(h(X)) -> h(proper(X)) f(ok(X)) -> ok(f(X)) g(ok(X)) -> ok(g(X)) h(ok(X)) -> ok(h(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) max/plus interpretations on N: active_A(x1) = max{48, 23 + x1} active#_A(x1) = max{1, -3 + x1} f_A(x1) = max{51, 26 + x1} f#_A(x1) = max{22, -2 + x1} mark_A(x1) = max{53, 7 + x1} mark#_A(x1) = max{6, 7} g_A(x1) = max{43, 8 + x1} g#_A(x1) = max{41, -1} h_A(x1) = max{53, 7 + x1} h#_A(x1) = max{48, -4} proper_A(x1) = max{2, 1 + x1} proper#_A(x1) = max{49, 42 + x1} ok_A(x1) = max{95, 49 + x1} ok#_A(x1) = max{0, 40} top_A(x1) = max{0, 0} top#_A(x1) = max{39, 36 + x1} precedence: active > top > proper > f > mark > h > ok > g