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