(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

lt(x, 0) → false
lt(0, s(y)) → true
lt(s(x), s(y)) → lt(x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
quot(x, s(y)) → help(x, s(y), 0)
help(x, s(y), c) → if(lt(c, x), x, s(y), c)
if(true, x, s(y), c) → s(help(x, s(y), plus(c, s(y))))
if(false, x, s(y), c) → 0

Q is empty.