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