YES O(n^2) TRS: {f(s(s(x))) -> f(f(s(x))), f(s(0())) -> s(0()), f(0()) -> s(0())} Natural interpretation: Strict: {f(s(s(x))) -> f(f(s(x))), f(s(0())) -> s(0()), f(0()) -> s(0())} Weak: {} Interpretation class: deltarestricted [f](delta, X0) = + 0*X0 + 0 + 2*X0*delta + 1*delta [0](delta) = + 2 + 0*delta [s](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 2*delta f_tau_1(delta) = delta/(0 + 2 * delta) s_tau_1(delta) = delta/(0 + 1 * delta) Qed