TRS:
 {             le(0(), y) -> true(),
            le(s(x), 0()) -> false(),
           le(s(x), s(y)) -> le(x, y),
            minus(x, 0()) -> x,
         minus(0(), s(y)) -> 0(),
        minus(s(x), s(y)) -> minus(x, y),
             plus(x, 0()) -> x,
            plus(x, s(y)) -> s(plus(x, y)),
           mod(s(x), 0()) -> 0(),
             mod(x, s(y)) -> help(x, s(y), 0()),
         help(x, s(y), c) -> if(le(c, x), x, s(y), c),
   if(true(), x, s(y), c) -> help(x, s(y), plus(c, s(y))),
  if(false(), x, s(y), c) -> minus(x, minus(c, s(y)))}
 Fail