YES Problem: f(x,x) -> a() f(g(x),y) -> f(x,y) Proof: DP Processor: DPs: f#(g(x),y) -> f#(x,y) TRS: f(x,x) -> a() f(g(x),y) -> f(x,y) CDG Processor: DPs: f#(g(x),y) -> f#(x,y) TRS: f(x,x) -> a() f(g(x),y) -> f(x,y) graph: Qed