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