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