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