MAYBE
Time: 0.066620
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()}
  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