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