MAYBE Problem: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) mult(0(),x) -> 0() mult(s(x),y) -> add(y,mult(x,y)) Proof: DP Processor: DPs: add#(s(x),y) -> add#(x,y) mult#(s(x),y) -> mult#(x,y) mult#(s(x),y) -> add#(y,mult(x,y)) TRS: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) mult(0(),x) -> 0() mult(s(x),y) -> add(y,mult(x,y)) Open