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