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