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