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