(COMMENT
 quot(x,y) computes a random number between 0 and x/y.
 Example 4.1 in a paper about predictive labeling (submitted to WRS '07)
 not terminating, but innermost terminating
)
(VAR x y z b)
(RULES
 ge(x,0) -> true
 ge(0,s(y)) -> false
 ge(s(x),s(y)) -> ge(x,y)
 minus(x,0) -> x
 minus(0,y) -> 0
 minus(s(x),s(y)) -> minus(x,y)
 id_inc(x) -> x
 id_inc(x) -> s(x)
 quot(x,y) -> div(x,y,0)
 div(x,y,z) -> if(ge(y,s(0)),ge(x,y),x,y,z)
 if(false,b,x,y,z) -> div_by_zero
 if(true,false,x,y,z) -> z
 if(true,true,x,y,z) -> div(minus(x,y),y,id_inc(z))
)