MAYBE
TRS:
 {        ge(x, 0()) -> true(),
       ge(0(), s(x)) -> false(),
      ge(s(x), s(y)) -> ge(x, y),
       minus(x, 0()) -> x,
   minus(s(x), s(y)) -> minus(x, y),
   ify(true(), x, y) -> if(ge(x, y), x, y),
  ify(false(), x, y) -> divByZeroError(),
           div(x, y) -> ify(ge(y, s(0())), x, y),
    if(true(), x, y) -> s(div(minus(x, y), y)),
   if(false(), x, y) -> 0()}
 DP:
  Strict:
   {   ge#(s(x), s(y)) -> ge#(x, y),
    minus#(s(x), s(y)) -> minus#(x, y),
    ify#(true(), x, y) -> ge#(x, y),
    ify#(true(), x, y) -> if#(ge(x, y), x, y),
            div#(x, y) -> ge#(y, s(0())),
            div#(x, y) -> ify#(ge(y, s(0())), x, y),
     if#(true(), x, y) -> minus#(x, y),
     if#(true(), x, y) -> div#(minus(x, y), y)}
  Weak:
  {        ge(x, 0()) -> true(),
        ge(0(), s(x)) -> false(),
       ge(s(x), s(y)) -> ge(x, y),
        minus(x, 0()) -> x,
    minus(s(x), s(y)) -> minus(x, y),
    ify(true(), x, y) -> if(ge(x, y), x, y),
   ify(false(), x, y) -> divByZeroError(),
            div(x, y) -> ify(ge(y, s(0())), x, y),
     if(true(), x, y) -> s(div(minus(x, y), y)),
    if(false(), x, y) -> 0()}
  EDG:
   {(ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> div#(minus(x, y), y))
    (ify#(true(), x, y) -> if#(ge(x, y), x, y), if#(true(), x, y) -> minus#(x, y))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ify#(ge(y, s(0())), x, y))
    (if#(true(), x, y) -> div#(minus(x, y), y), div#(x, y) -> ge#(y, s(0())))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (if#(true(), x, y) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (ify#(true(), x, y) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> ge#(x, y))
    (div#(x, y) -> ify#(ge(y, s(0())), x, y), ify#(true(), x, y) -> if#(ge(x, y), x, y))
    (div#(x, y) -> ge#(y, s(0())), ge#(s(x), s(y)) -> ge#(x, y))}
   SCCS:
    Scc:
     {ify#(true(), x, y) -> if#(ge(x, y), x, y),
              div#(x, y) -> ify#(ge(y, s(0())), x, y),
       if#(true(), x, y) -> div#(minus(x, y), y)}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    Scc:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    SCC:
     Strict:
      {ify#(true(), x, y) -> if#(ge(x, y), x, y),
               div#(x, y) -> ify#(ge(y, s(0())), x, y),
        if#(true(), x, y) -> div#(minus(x, y), y)}
     Weak:
     {        ge(x, 0()) -> true(),
           ge(0(), s(x)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
           minus(x, 0()) -> x,
       minus(s(x), s(y)) -> minus(x, y),
       ify(true(), x, y) -> if(ge(x, y), x, y),
      ify(false(), x, y) -> divByZeroError(),
               div(x, y) -> ify(ge(y, s(0())), x, y),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     Fail
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {        ge(x, 0()) -> true(),
           ge(0(), s(x)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
           minus(x, 0()) -> x,
       minus(s(x), s(y)) -> minus(x, y),
       ify(true(), x, y) -> if(ge(x, y), x, y),
      ify(false(), x, y) -> divByZeroError(),
               div(x, y) -> ify(ge(y, s(0())), x, y),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {ge#(s(x), s(y)) -> ge#(x, y)}
     Weak:
     {        ge(x, 0()) -> true(),
           ge(0(), s(x)) -> false(),
          ge(s(x), s(y)) -> ge(x, y),
           minus(x, 0()) -> x,
       minus(s(x), s(y)) -> minus(x, y),
       ify(true(), x, y) -> if(ge(x, y), x, y),
      ify(false(), x, y) -> divByZeroError(),
               div(x, y) -> ify(ge(y, s(0())), x, y),
        if(true(), x, y) -> s(div(minus(x, y), y)),
       if(false(), x, y) -> 0()}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed