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)) Usable Rule Processor: DPs: +#(s(x),y) -> +#(x,y) +#(s(x),y) -> +#(x,s(y)) TRS: CDG Processor: DPs: +#(s(x),y) -> +#(x,y) +#(s(x),y) -> +#(x,s(y)) TRS: graph: Qed