YES O(n^2) TRS: {f() -> g(), c() -> f()} Natural interpretation: Strict: {f() -> g(), c() -> f()} Weak: {} Interpretation class: deltarestricted [g](delta) = + 0 + 0*delta [c](delta) = + 2 + 3*delta [f](delta) = + 2 + 1*delta Qed