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