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