YES 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)) TDG 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)) graph: mult#(s(x),y) -> mult#(x,y) -> mult#(s(x),y) -> add#(y,mult(x,y)) mult#(s(x),y) -> mult#(x,y) -> mult#(s(x),y) -> mult#(x,y) mult#(s(x),y) -> add#(y,mult(x,y)) -> add#(s(x),y) -> add#(x,y) add#(s(x),y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: mult#(s(x),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)) LPO Processor: argument filtering: pi(0) = [] pi(add) = [0,1] pi(s) = [0] pi(mult) = [0,1] pi(mult#) = 0 precedence: mult > add > mult# ~ s ~ 0 problem: DPs: 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)) Qed DPs: add#(s(x),y) -> add#(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)) LPO Processor: argument filtering: pi(0) = [] pi(add) = [0,1] pi(s) = [0] pi(mult) = [0,1] pi(add#) = 0 precedence: mult > add > add# ~ s ~ 0 problem: DPs: 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)) Qed