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