(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR x y )
(STRATEGY INNERMOST)
(RULES 
        pred(s(x)) -> x
        minus(x, 0) -> x
        minus(x, s(y)) -> pred(minus(x, y))
        quot(0, s(y)) -> 0
        quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
        
)