(COMMENT div(x,y) computes a random number between 0 and x/y. leading example of a paper about predictive labeling (submitted to WRS '07) not terminating, but innermost terminating ) (VAR x y 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) div(x,y) -> if(ge(y,s(0)),ge(x,y),x,y) if(false,b,x,y) -> div_by_zero if(true,false,x,y) -> 0 if(true,true,x,y) -> id_inc(div(minus(x,y),y)) )