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