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 TDG 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: +#(-(x,y),z) -> +#(x,z) -> +#(-(x,y),z) -> -#(+(x,z),y) +#(-(x,y),z) -> +#(x,z) -> +#(-(x,y),z) -> +#(x,z) 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