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