(VAR x y )
(RULES 
        lt(0, s(x)) -> true
        lt(x, 0) -> false
        lt(s(x), s(y)) -> lt(x, y)
        minus(x, y) -> help(lt(y, x), x, y)
        help(true, x, y) -> s(minus(x, s(y)))
        help(false, x, y) -> 0
        
)