(COMMENT
 div(x,y) computes floor(x/y)


 problems:
  - div uses tests and there are calls to plus and inc inside recursion
  - plus terminates by bounded increase
  - not confluent

)
(VAR x y z b i j)
(RULES
 div(x,y) -> div2(x,y,0)
 div2(x,y,i) -> if1(le(y,0),le(y,x),x,y,plus(i,0),inc(i))
 if1(true,b,x,y,i,j) -> divZeroError
 if1(false,b,x,y,i,j) -> if2(b,x,y,i,j)
 if2(true,x,y,i,j) -> div2(minus(x,y),y,j)
 if2(false,x,y,i,j) -> i

 inc(0) -> 0
 inc(s(i)) -> s(inc(i))

 le(s(x), 0) -> false
 le(0, y) -> true
 le(s(x), s(y)) -> le(x, y)

 minus(x,0) -> x
 minus(0,y) -> 0
 minus(s(x),s(y)) -> minus(x,y)
 
 plus(x,y) -> plusIter(x,y,0)
 plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
 ifPlus(true,x,y,z) -> y
 ifPlus(false,x,y,z) -> plusIter(x,s(y),s(z))

 a -> c
 a -> d
)