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