YES TRS: active(g(X)) -> mark(h(X)) active(c()) -> mark(d()) active(h(d())) -> mark(g(c())) mark(g(X)) -> active(g(X)) mark(h(X)) -> active(h(X)) mark(c()) -> active(c()) mark(d()) -> active(d()) g(mark(X)) -> g(X) g(active(X)) -> g(X) h(mark(X)) -> h(X) h(active(X)) -> h(X) linear polynomial interpretations on N: active_A(x1) = 1 active#_A(x1) = x1 + 3 g_A(x1) = 1 g#_A(x1) = x1 + 3 mark_A(x1) = 1 mark#_A(x1) = x1 + 3 h_A(x1) = 0 h#_A(x1) = x1 c_A = 2 c#_A = 2 d_A = 1 d#_A = 5 precedence: mark > active > d > c > h > g