(COMMENT variant of AG01 3.5)
(VAR b x y z)
(RULES
le(0,y) -> true
le(s(x),0) -> false
le(s(x),s(y)) -> le(x,y)
minus(x,x) -> 0
minus(x,0) -> x
minus(0,x) -> 0
minus(s(x),s(y)) -> minus(x,y)

isZero(0) -> true
isZero(s(x)) -> false

mod(x,y) -> if_mod(isZero(y), le(y,x), x, y, minus(x,y))
if_mod(true, b, x, y, z) -> divByZeroError
if_mod(false, false, x, y, z) -> x
if_mod(false, true, x, y, z) -> mod(z, y) 
)