MAYBE Problem: div(0(),y) -> 0() div(x,y) -> quot(x,y,y) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) quot(x,0(),s(z)) -> s(div(x,s(z))) Proof: DP Processor: DPs: div#(x,y) -> quot#(x,y,y) quot#(s(x),s(y),z) -> quot#(x,y,z) quot#(x,0(),s(z)) -> div#(x,s(z)) TRS: div(0(),y) -> 0() div(x,y) -> quot(x,y,y) quot(0(),s(y),z) -> 0() quot(s(x),s(y),z) -> quot(x,y,z) quot(x,0(),s(z)) -> s(div(x,s(z))) Open