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