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