YES O(n^2) TRS: { if(true(), X, Y) -> X, if(false(), X, Y) -> activate(Y), f(X) -> if(X, c(), n__f(true())), f(X) -> n__f(X), activate(X) -> X, activate(n__f(X)) -> f(X) } Natural interpretation: Strict: { if(true(), X, Y) -> X, if(false(), X, Y) -> activate(Y), f(X) -> if(X, c(), n__f(true())), f(X) -> n__f(X), activate(X) -> X, activate(n__f(X)) -> f(X) } Weak: {} Interpretation class: deltarestricted [false](delta) = + 0 + 3*delta [activate](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 3*delta [f](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 2*delta [true](delta) = + 0 + 0*delta [n__f](delta, X0) = + 1*X0 + 0 + 0*X0*delta + 0*delta [c](delta) = + 0 + 0*delta [if](delta, X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 0 + 0*X0*delta + 0*X1*delta + 0*X2*delta + 1*delta activate_tau_1(delta) = delta/(1 + 0 * delta) f_tau_1(delta) = delta/(1 + 0 * delta) n__f_tau_1(delta) = delta/(1 + 0 * delta) if_tau_1(delta) = delta/(1 + 0 * delta)if_tau_2(delta) = delta/(1 + 0 * delta)if_tau_3(delta) = delta/(1 + 0 * delta) Qed