YES O(n^2) TRS: { d(x) -> e(u(x)), d(u(x)) -> c(x), c(u(x)) -> b(x), b(u(x)) -> a(e(x)), v(e(x)) -> x } Natural interpretation: Strict: { d(x) -> e(u(x)), d(u(x)) -> c(x), c(u(x)) -> b(x), b(u(x)) -> a(e(x)), v(e(x)) -> x } Weak: {} Interpretation class: deltarestricted [a](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [v](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 1*delta [b](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [c](delta, X0) = + 0*X0 + 0 + 1*X0*delta + 0*delta [d](delta, X0) = + 0*X0 + 1 + 1*X0*delta + 1*delta [u](delta, X0) = + 0*X0 + 1 + 1*X0*delta + 0*delta [e](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 0*delta a_tau_1(delta) = delta/(0 + 1 * delta) v_tau_1(delta) = delta/(1 + 0 * delta) b_tau_1(delta) = delta/(0 + 1 * delta) c_tau_1(delta) = delta/(0 + 1 * delta) d_tau_1(delta) = delta/(0 + 1 * delta) u_tau_1(delta) = delta/(0 + 1 * delta) e_tau_1(delta) = delta/(1 + 0 * delta) Qed