YES O(n) TRS: { d(x) -> e(u(x)), d(u(x)) -> c(x), c(u(x)) -> b(x), b(u(x)) -> a(e(x)), v(e(x)) -> x } Natural interpretation: Strict: { d(x) -> e(u(x)), d(u(x)) -> c(x), c(u(x)) -> b(x), b(u(x)) -> a(e(x)), v(e(x)) -> x } Weak: {} Interpretation class: stronglylinear [a](X0) = + 1*X0 + 0 [v](X0) = + 1*X0 + 2 [b](X0) = + 1*X0 + 3 [c](X0) = + 1*X0 + 3 [d](X0) = + 1*X0 + 3 [u](X0) = + 1*X0 + 1 [e](X0) = + 1*X0 + 0 Qed