YES O(n) TRS: { f(X) -> n__f(X), f(f(a())) -> f(g(n__f(a()))), activate(X) -> X, activate(n__f(X)) -> f(X) } Natural interpretation: Strict: { f(X) -> n__f(X), f(f(a())) -> f(g(n__f(a()))), activate(X) -> X, activate(n__f(X)) -> f(X) } Weak: {} Interpretation class: stronglylinear [activate](X0) = + 1*X0 + 2 [a] = + 0 [n__f](X0) = + 1*X0 + 0 [g](X0) = + 1*X0 + 0 [f](X0) = + 1*X0 + 1 Qed