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