(VAR x y v u)
(RULES
minus(x, y) -> cond(min(x, y), x, y)
cond(y, x, y) -> s(minus(x, s(y)))
min(0, v) -> 0
min(u, 0) -> 0
min(s(u), s(v)) -> s(min(u, v))
)