TRS: { f(X) -> g(n__h(n__f(X))), h(X) -> n__h(X), f(X) -> n__f(X), activate(n__h(X)) -> h(activate(X)), activate(n__f(X)) -> f(activate(X)), activate(X) -> X} MPO: Prec: h > n__h, f > n__f, f > n__h, f > g, activate > h, activate > f empty Strict: {} Weak: {} Qed