YES O(n^2) TRS: { activate(X) -> X, and(tt(), X) -> activate(X), plus(N, 0()) -> N, plus(N, s(M)) -> s(plus(N, M)) } Natural interpretation: Strict: { activate(X) -> X, and(tt(), X) -> activate(X), plus(N, 0()) -> N, plus(N, s(M)) -> s(plus(N, M)) } Weak: {} Interpretation class: deltarestricted [s](delta, X0) = + 1*X0 + 1 + 0*X0*delta + 0*delta [0](delta) = + 0 + 1*delta [plus](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 1*X0*delta + 0*X1*delta + 0*delta [tt](delta) = + 0 + 1*delta [and](delta, X1, X0) = + 1*X0 + 1*X1 + 0 + 0*X0*delta + 0*X1*delta + 1*delta [activate](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 1*delta s_tau_1(delta) = delta/(1 + 0 * delta) plus_tau_1(delta) = delta/(1 + 0 * delta)plus_tau_2(delta) = delta/(1 + 1 * delta) and_tau_1(delta) = delta/(1 + 0 * delta)and_tau_2(delta) = delta/(1 + 0 * delta) activate_tau_1(delta) = delta/(1 + 0 * delta) Qed