YES O(n) TRS: { c(X) -> d(activate(X)), f(X) -> n__f(X), f(f(X)) -> c(n__f(g(n__f(X)))), d(X) -> n__d(X), activate(X) -> X, activate(n__f(X)) -> f(X), activate(n__d(X)) -> d(X), h(X) -> c(n__d(X)) } Natural interpretation: Strict: { c(X) -> d(activate(X)), f(X) -> n__f(X), f(f(X)) -> c(n__f(g(n__f(X)))), d(X) -> n__d(X), activate(X) -> X, activate(n__f(X)) -> f(X), activate(n__d(X)) -> d(X), h(X) -> c(n__d(X)) } Weak: {} Interpretation class: stronglylinear [h](X0) = + 1*X0 + 14 [n__d](X0) = + 1*X0 + 0 [activate](X0) = + 1*X0 + 9 [d](X0) = + 1*X0 + 1 [f](X0) = + 1*X0 + 11 [g](X0) = + 1*X0 + 0 [n__f](X0) = + 1*X0 + 5 [c](X0) = + 1*X0 + 11 Qed