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)) KBO Processor: argument filtering: pi(0) = [] pi(add) = [0,1] pi(s) = [0] pi(add#) = 0 weight function: w0 = 1 w(add#) = w(s) = w(add) = w(0) = 1 precedence: add# ~ add ~ 0 > s problem: DPs: TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) Qed