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