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