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