YES Problem: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Proof: DP Processor: DPs: f#(g(x)) -> f#(x) TRS: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Qed