YES O(n) 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: stronglylinear [false] = + 3 [activate](X0) = + 1*X0 + 3 [f](X0) = + 1*X0 + 3 [true] = + 0 [n__f](X0) = + 1*X0 + 1 [c] = + 0 [if](X2, X1, X0) = + 1*X0 + 1*X1 + 1*X2 + 1 Qed