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