(VAR x y z u)
(RULES
le(0,y) -> true
le(s(x),0) -> false
le(s(x),s(y)) -> le(x,y)

mod(x,0) -> modZeroErro
mod(x,s(y)) -> modIter(x,s(y),0,0)
modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
if(true,x,y,z,u) -> u 
if(false,x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
if2(false,x,y,z,u) -> modIter(x,y,z,u)
if2(true,x,y,z,u) -> modIter(x,y,z,0)
)