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