(VAR b x y ) (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)) )