YES TRS: active(f(f(a()))) -> mark(f(g(f(a())))) active(f(X)) -> f(active(X)) f(mark(X)) -> mark(f(X)) proper(f(X)) -> f(proper(X)) proper(a()) -> ok(a()) proper(g(X)) -> g(proper(X)) f(ok(X)) -> ok(f(X)) g(ok(X)) -> ok(g(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) max/plus interpretations on N: active_A(x1) = max{4, -3 + x1} active#_A(x1) = max{0, 23} f_A(x1) = max{2, x1} f#_A(x1) = max{6, 2} a_A = 25 a#_A = 24 mark_A(x1) = max{8, 6 + x1} mark#_A(x1) = max{1, -1} g_A(x1) = max{14, 16} g#_A(x1) = max{1, 5} proper_A(x1) = max{4, 1 + x1} proper#_A(x1) = max{16, 3} ok_A(x1) = max{15, -2 + x1} ok#_A(x1) = max{4, -1} top_A(x1) = max{0, 0} top#_A(x1) = max{13, 8 + x1} precedence: f > ok = top > a = g > active > mark > proper