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