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) TDG 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: f#(g(x),x,y) -> f#(y,y,g(y)) -> f#(g(x),x,y) -> f#(y,y,g(y)) f#(g(x),x,y) -> f#(y,y,g(y)) -> f#(g(x),x,y) -> g#(y) EDG 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