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