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