MAYBE 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)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 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)) Open