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))) LPO Processor: argument filtering: pi(g) = [0] pi(f) = [0] pi(f#) = [0] precedence: f > f# ~ g problem: DPs: TRS: f(g(x)) -> g(g(f(x))) f(g(x)) -> g(g(g(x))) Qed