YES O(n) TRS: {h(x, x) -> x, f(x, y) -> h(x, y), f(x, y) -> h(y, x)} Natural interpretation: Strict: {h(x, x) -> x, f(x, y) -> h(x, y), f(x, y) -> h(y, x)} Weak: {} Interpretation class: stronglylinear [f](X1, X0) = + 1*X0 + 1*X1 + 3 [h](X1, X0) = + 1*X0 + 1*X1 + 2 Qed