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