MAYBE
Time: 0.132279
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:
  DP:
   {     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)}
  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()}
  UR:
   {     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),
            a(z, w) -> z,
            a(z, w) -> w}
   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))}
    STATUS:
     arrows: 0.828125
     SCCS (3):
      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 (3):
       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 (1):
       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()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [ify](x0, x1, x2) = x0 + 1,
         
         [if](x0, x1, x2) = 0,
         
         [ge](x0, x1) = x0 + 1,
         
         [minus](x0, x1) = x0 + 1,
         
         [div](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [true] = 1,
         
         [0] = 1,
         
         [false] = 1,
         
         [divByZeroError] = 0,
         
         [minus#](x0, x1) = x0
        Strict:
         minus#(s x, s y) -> minus#(x, y)
         1 + 0x + 1y >= 0 + 0x + 1y
        Weak:
         if(false(), x, y) -> 0()
         0 + 0x + 0y >= 1
         if(true(), x, y) -> s div(minus(x, y), y)
         0 + 0x + 0y >= 3 + 0x + 1y
         div(x, y) -> ify(ge(y, s 0()), x, y)
         1 + 1x + 0y >= 4 + 0x + 0y
         ify(false(), x, y) -> divByZeroError()
         2 + 0x + 0y >= 0
         ify(true(), x, y) -> if(ge(x, y), x, y)
         2 + 0x + 0y >= 0 + 0x + 0y
         minus(s x, s y) -> minus(x, y)
         2 + 0x + 1y >= 1 + 0x + 1y
         minus(x, 0()) -> x
         2 + 0x >= 1x
         ge(s x, s y) -> ge(x, y)
         2 + 0x + 1y >= 1 + 0x + 1y
         ge(0(), s x) -> false()
         2 + 1x >= 1
         ge(x, 0()) -> true()
         2 + 0x >= 1
       Qed
     
     SCC (1):
      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()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [ify](x0, x1, x2) = x0 + 1,
        
        [if](x0, x1, x2) = 0,
        
        [ge](x0, x1) = x0 + 1,
        
        [minus](x0, x1) = x0 + 1,
        
        [div](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [true] = 1,
        
        [0] = 1,
        
        [false] = 1,
        
        [divByZeroError] = 0,
        
        [ge#](x0, x1) = x0
       Strict:
        ge#(s x, s y) -> ge#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        if(false(), x, y) -> 0()
        0 + 0x + 0y >= 1
        if(true(), x, y) -> s div(minus(x, y), y)
        0 + 0x + 0y >= 3 + 0x + 1y
        div(x, y) -> ify(ge(y, s 0()), x, y)
        1 + 1x + 0y >= 4 + 0x + 0y
        ify(false(), x, y) -> divByZeroError()
        2 + 0x + 0y >= 0
        ify(true(), x, y) -> if(ge(x, y), x, y)
        2 + 0x + 0y >= 0 + 0x + 0y
        minus(s x, s y) -> minus(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        minus(x, 0()) -> x
        2 + 0x >= 1x
        ge(s x, s y) -> ge(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        ge(0(), s x) -> false()
        2 + 1x >= 1
        ge(x, 0()) -> true()
        2 + 0x >= 1
      Qed