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

quot(x,0) -> quotZeroErro
quot(x,s(y)) -> quotIter(x,s(y),0,0,0)
quotIter(x,s(y),z,u,v) -> if(le(x,z),x,s(y),z,u,v)
if(true,x,y,z,u,v) -> v
if(false,x,y,z,u,v) -> if2(le(y,s(u)),x,y,s(z),s(u),v)
if2(false,x,y,z,u,v) -> quotIter(x,y,z,u,v)
if2(true,x,y,z,u,v) -> quotIter(x,y,z,0,s(v))
)