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