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