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