MAYBE
Time: 0.008846
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:
  DP:
   {              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)}
  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()}
  EDG:
   {(if1#(false(), b, x, y, i, j) -> if2#(b, x, y, i, j), if2#(true(), x, y, i, j) -> minus#(x, y))
    (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))
    (if2#(true(), x, y, i, j) -> minus#(x, y), minus#(s x, s y) -> minus#(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))
    (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z))
    (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> le#(x, z))
    (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) -> inc# i, inc# s i -> inc# i)
    (if2#(true(), x, y, i, j) -> div2#(minus(x, y), y, j), div2#(x, y, i) -> inc# i)
    (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) -> le#(y, 0()))
    (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) -> if1#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc i))
    (inc# s i -> inc# i, inc# s i -> inc# i)
    (plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z))
    (div2#(x, y, i) -> le#(y, x), le#(s x, s y) -> le#(x, y))
    (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) -> plus#(i, 0()), plus#(x, y) -> plusIter#(x, y, 0()))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (plusIter#(x, y, z) -> le#(x, z), le#(s x, s y) -> le#(x, y))}
   STATUS:
    arrows: 0.898438
    SCCS (5):
     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:
      {minus#(s x, s y) -> minus#(x, y)}
     Scc:
      {inc# s i -> inc# i}
     Scc:
      {       plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z),
       ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     
     SCC (3):
      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()}
      Open
     
     SCC (1):
      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()}
      Open
     
     SCC (1):
      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()}
      Open
     
     
     SCC (2):
      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()}
      Open
     
     
     
     SCC (1):
      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()}
      Open