YES Problem: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) Proof: DP Processor: DPs: f#(g(X)) -> f#(X) f#(g(X)) -> f#(f(X)) TRS: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) KBO Processor: argument filtering: pi(g) = [0] pi(f) = 0 pi(h) = [] pi(f#) = 0 weight function: w0 = 1 w(f#) = w(h) = 1 w(f) = w(g) = 0 precedence: f# ~ h ~ f ~ g problem: DPs: TRS: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) Qed