(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))) )