TRS: {f(x, y) -> h(x, y), f(x, y) -> h(y, x), h(x, x) -> x} MPO: Prec: f > h empty Strict: {} Weak: {} Qed