MAYBE
TRS:
 {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                    div(x, y) -> div2(x, y, 0()),
   if1(true(), b, x, y, i, j) -> divZeroError(),
  if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                   le(0(), y) -> true(),
                le(s(x), 0()) -> false(),
               le(s(x), s(y)) -> le(x, y),
                   plus(x, y) -> plusIter(x, y, 0()),
                     inc(0()) -> 0(),
                    inc(s(i)) -> s(inc(i)),
      if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
     if2(false(), x, y, i, j) -> i,
                minus(x, 0()) -> x,
                minus(0(), y) -> 0(),
            minus(s(x), s(y)) -> minus(x, y),
            plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
      ifPlus(true(), x, y, z) -> y,
     ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                          a() -> c(),
                          a() -> d()}
 DP:
  Strict:
   {              div2#(x, y, i) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                  div2#(x, y, i) -> le#(y, x),
                  div2#(x, y, i) -> le#(y, 0()),
                  div2#(x, y, i) -> plus#(i, 0()),
                  div2#(x, y, i) -> inc#(i),
                      div#(x, y) -> div2#(x, y, 0()),
    if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j),
                 le#(s(x), s(y)) -> le#(x, y),
                     plus#(x, y) -> plusIter#(x, y, 0()),
                      inc#(s(i)) -> inc#(i),
        if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j),
        if2#(true(), x, y, i, j) -> minus#(x, y),
              minus#(s(x), s(y)) -> minus#(x, y),
              plusIter#(x, y, z) -> le#(x, z),
              plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
       ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z))}
  Weak:
  {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                     div(x, y) -> div2(x, y, 0()),
    if1(true(), b, x, y, i, j) -> divZeroError(),
   if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                    le(0(), y) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
                    plus(x, y) -> plusIter(x, y, 0()),
                      inc(0()) -> 0(),
                     inc(s(i)) -> s(inc(i)),
       if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
      if2(false(), x, y, i, j) -> i,
                 minus(x, 0()) -> x,
                 minus(0(), y) -> 0(),
             minus(s(x), s(y)) -> minus(x, y),
             plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
       ifPlus(true(), x, y, z) -> y,
      ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                           a() -> c(),
                           a() -> d()}
  EDG:
   {(div2#(x, y, i) -> plus#(i, 0()), plus#(x, y) -> plusIter#(x, y, 0()))
    (plusIter#(x, y, z) -> le#(x, z), le#(s(x), s(y)) -> le#(x, y))
    (div2#(x, y, i) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j))
    (inc#(s(i)) -> inc#(i), inc#(s(i)) -> inc#(i))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (if2#(true(), x, y, i, j) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z))
    (ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)), plusIter#(x, y, z) -> le#(x, z))
    (div2#(x, y, i) -> le#(y, x), le#(s(x), s(y)) -> le#(x, y))
    (plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z)))
    (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))
    (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> le#(x, z))
    (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z))
    (div#(x, y) -> div2#(x, y, 0()), div2#(x, y, i) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)))
    (div#(x, y) -> div2#(x, y, 0()), div2#(x, y, i) -> le#(y, x))
    (div#(x, y) -> div2#(x, y, 0()), div2#(x, y, i) -> le#(y, 0()))
    (div#(x, y) -> div2#(x, y, 0()), div2#(x, y, i) -> plus#(i, 0()))
    (div#(x, y) -> div2#(x, y, 0()), div2#(x, y, i) -> inc#(i))
    (div2#(x, y, i) -> inc#(i), inc#(s(i)) -> inc#(i))
    (if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j), div2#(x, y, i) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)))
    (if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j), div2#(x, y, i) -> le#(y, x))
    (if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j), div2#(x, y, i) -> le#(y, 0()))
    (if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j), div2#(x, y, i) -> plus#(i, 0()))
    (if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j), div2#(x, y, i) -> inc#(i))
    (if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j), if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j))
    (if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j), if2#(true(), x, y, i, j) -> minus#(x, y))}
   SCCS:
    Scc:
     {       plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
      ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z))}
    Scc:
     {minus#(s(x), s(y)) -> minus#(x, y)}
    Scc:
     {inc#(s(i)) -> inc#(i)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {              div2#(x, y, i) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
      if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j),
          if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j)}
    SCC:
     Strict:
      {       plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
       ifPlus#(false(), x, y, z) -> plusIter#(x, s(y), s(z))}
     Weak:
     {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                        div(x, y) -> div2(x, y, 0()),
       if1(true(), b, x, y, i, j) -> divZeroError(),
      if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
                       plus(x, y) -> plusIter(x, y, 0()),
                         inc(0()) -> 0(),
                        inc(s(i)) -> s(inc(i)),
          if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
         if2(false(), x, y, i, j) -> i,
                    minus(x, 0()) -> x,
                    minus(0(), y) -> 0(),
                minus(s(x), s(y)) -> minus(x, y),
                plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
          ifPlus(true(), x, y, z) -> y,
         ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                              a() -> c(),
                              a() -> d()}
     Fail
    SCC:
     Strict:
      {minus#(s(x), s(y)) -> minus#(x, y)}
     Weak:
     {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                        div(x, y) -> div2(x, y, 0()),
       if1(true(), b, x, y, i, j) -> divZeroError(),
      if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
                       plus(x, y) -> plusIter(x, y, 0()),
                         inc(0()) -> 0(),
                        inc(s(i)) -> s(inc(i)),
          if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
         if2(false(), x, y, i, j) -> i,
                    minus(x, 0()) -> x,
                    minus(0(), y) -> 0(),
                minus(s(x), s(y)) -> minus(x, y),
                plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
          ifPlus(true(), x, y, z) -> y,
         ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                              a() -> c(),
                              a() -> d()}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {inc#(s(i)) -> inc#(i)}
     Weak:
     {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                        div(x, y) -> div2(x, y, 0()),
       if1(true(), b, x, y, i, j) -> divZeroError(),
      if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
                       plus(x, y) -> plusIter(x, y, 0()),
                         inc(0()) -> 0(),
                        inc(s(i)) -> s(inc(i)),
          if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
         if2(false(), x, y, i, j) -> i,
                    minus(x, 0()) -> x,
                    minus(0(), y) -> 0(),
                minus(s(x), s(y)) -> minus(x, y),
                plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
          ifPlus(true(), x, y, z) -> y,
         ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                              a() -> c(),
                              a() -> d()}
     SPSC:
      Simple Projection:
       pi(inc#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                        div(x, y) -> div2(x, y, 0()),
       if1(true(), b, x, y, i, j) -> divZeroError(),
      if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
                       plus(x, y) -> plusIter(x, y, 0()),
                         inc(0()) -> 0(),
                        inc(s(i)) -> s(inc(i)),
          if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
         if2(false(), x, y, i, j) -> i,
                    minus(x, 0()) -> x,
                    minus(0(), y) -> 0(),
                minus(s(x), s(y)) -> minus(x, y),
                plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
          ifPlus(true(), x, y, z) -> y,
         ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                              a() -> c(),
                              a() -> d()}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {              div2#(x, y, i) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
       if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j),
           if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j)}
     Weak:
     {              div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)),
                        div(x, y) -> div2(x, y, 0()),
       if1(true(), b, x, y, i, j) -> divZeroError(),
      if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j),
                       le(0(), y) -> true(),
                    le(s(x), 0()) -> false(),
                   le(s(x), s(y)) -> le(x, y),
                       plus(x, y) -> plusIter(x, y, 0()),
                         inc(0()) -> 0(),
                        inc(s(i)) -> s(inc(i)),
          if2(true(), x, y, i, j) -> div2(minus(x, y), y, j),
         if2(false(), x, y, i, j) -> i,
                    minus(x, 0()) -> x,
                    minus(0(), y) -> 0(),
                minus(s(x), s(y)) -> minus(x, y),
                plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
          ifPlus(true(), x, y, z) -> y,
         ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
                              a() -> c(),
                              a() -> d()}
     Fail