YES O(n^2) TRS: { a__f(X) -> f(X), a__f(f(a())) -> a__f(g(f(a()))), mark(g(X)) -> g(X), mark(f(X)) -> a__f(mark(X)), mark(a()) -> a() } Natural interpretation: Strict: { a__f(X) -> f(X), a__f(f(a())) -> a__f(g(f(a()))), mark(g(X)) -> g(X), mark(f(X)) -> a__f(mark(X)), mark(a()) -> a() } Weak: {} Interpretation class: deltarestricted [mark](delta, X0) = + 1*X0 + 0 + 2*X0*delta + 2*delta [a](delta) = + 0 + 0*delta [f](delta, X0) = + 1*X0 + 1 + 2*X0*delta + 2*delta [g](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [a__f](delta, X0) = + 1*X0 + 1 + 2*X0*delta + 3*delta mark_tau_1(delta) = delta/(1 + 2 * delta) f_tau_1(delta) = delta/(1 + 2 * delta) g_tau_1(delta) = delta/(0 + 1 * delta) a__f_tau_1(delta) = delta/(1 + 2 * delta) Qed