YES(?,O(n^1)) TRS: {f f a() -> f g()} DUP: We consider a non-duplicating system. Trs: {f f a() -> f g()} Natural interpretation: Strict: {f f a() -> f g()} Weak: {} Interpretation class: stronglylinear [a] = + 6 [g] = + 0 [f](X0) = + 1*X0 + 3 Qed