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)) Usable Rule Processor: DPs: f#(x,y) -> g#(x,y) g#(h(x),y) -> f#(x,y) g#(h(x),y) -> g#(x,y) TRS: KBO Processor: argument filtering: pi(h) = [0] pi(f#) = [0] pi(g#) = 0 usable rules: weight function: w0 = 1 w(f#) = w(h) = 1 w(g#) = 0 precedence: h > g# ~ f# problem: DPs: TRS: Qed