(VAR X Y)
(RULES

le(0,Y) -> true
le(s(X),0) -> false
le(s(X),s(Y)) -> le(X,Y)
minus(0,Y) -> 0
minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y)
ifMinus(true,s(X),Y) -> 0
ifMinus(false,s(X),Y) -> s(minus(X,Y))
quot(0,s(Y)) -> 0
quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y)))

)