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