YES TRS: {h(x, x) -> x, f(x, y) -> h(x, y), f(x, y) -> h(y, x)} RUF: Strict: {h(x, x) -> x} Weak: {} RUF: Strict: {} Weak: {} Qed