MAYBE
Time: 0.417530
TRS:
 {         half 0() -> 0(),
         half s 0() -> 0(),
         half s s x -> s half x,
            inc 0() -> 0(),
            inc s x -> s inc x,
           zero 0() -> true(),
           zero s x -> false(),
              p 0() -> 0(),
              p s x -> x,
      bitIter(x, y) -> if(zero x, x, inc y),
             bits x -> bitIter(x, 0()),
   if(true(), x, y) -> p y,
  if(false(), x, y) -> bitIter(half x, y)}
 DP:
  DP:
   {       half# s s x -> half# x,
              inc# s x -> inc# x,
        bitIter#(x, y) -> inc# y,
        bitIter#(x, y) -> zero# x,
        bitIter#(x, y) -> if#(zero x, x, inc y),
               bits# x -> bitIter#(x, 0()),
     if#(true(), x, y) -> p# y,
    if#(false(), x, y) -> half# x,
    if#(false(), x, y) -> bitIter#(half x, y)}
  TRS:
  {         half 0() -> 0(),
          half s 0() -> 0(),
          half s s x -> s half x,
             inc 0() -> 0(),
             inc s x -> s inc x,
            zero 0() -> true(),
            zero s x -> false(),
               p 0() -> 0(),
               p s x -> x,
       bitIter(x, y) -> if(zero x, x, inc y),
              bits x -> bitIter(x, 0()),
    if(true(), x, y) -> p y,
   if(false(), x, y) -> bitIter(half x, y)}
  UR:
   {  half 0() -> 0(),
    half s 0() -> 0(),
    half s s x -> s half x,
       inc 0() -> 0(),
       inc s x -> s inc x,
      zero 0() -> true(),
      zero s x -> false(),
       a(z, w) -> z,
       a(z, w) -> w}
   EDG:
    {(inc# s x -> inc# x, inc# s x -> inc# x)
     (if#(false(), x, y) -> half# x, half# s s x -> half# x)
     (if#(false(), x, y) -> bitIter#(half x, y), bitIter#(x, y) -> if#(zero x, x, inc y))
     (if#(false(), x, y) -> bitIter#(half x, y), bitIter#(x, y) -> zero# x)
     (if#(false(), x, y) -> bitIter#(half x, y), bitIter#(x, y) -> inc# y)
     (bitIter#(x, y) -> if#(zero x, x, inc y), if#(true(), x, y) -> p# y)
     (bitIter#(x, y) -> if#(zero x, x, inc y), if#(false(), x, y) -> half# x)
     (bitIter#(x, y) -> if#(zero x, x, inc y), if#(false(), x, y) -> bitIter#(half x, y))
     (bitIter#(x, y) -> inc# y, inc# s x -> inc# x)
     (bits# x -> bitIter#(x, 0()), bitIter#(x, y) -> inc# y)
     (bits# x -> bitIter#(x, 0()), bitIter#(x, y) -> zero# x)
     (bits# x -> bitIter#(x, 0()), bitIter#(x, y) -> if#(zero x, x, inc y))
     (half# s s x -> half# x, half# s s x -> half# x)}
    STATUS:
     arrows: 0.839506
     SCCS (3):
      Scc:
       {    bitIter#(x, y) -> if#(zero x, x, inc y),
        if#(false(), x, y) -> bitIter#(half x, y)}
      Scc:
       {inc# s x -> inc# x}
      Scc:
       {half# s s x -> half# x}
      
      
      SCC (2):
       Strict:
        {    bitIter#(x, y) -> if#(zero x, x, inc y),
         if#(false(), x, y) -> bitIter#(half x, y)}
       Weak:
       {         half 0() -> 0(),
               half s 0() -> 0(),
               half s s x -> s half x,
                  inc 0() -> 0(),
                  inc s x -> s inc x,
                 zero 0() -> true(),
                 zero s x -> false(),
                    p 0() -> 0(),
                    p s x -> x,
            bitIter(x, y) -> if(zero x, x, inc y),
                   bits x -> bitIter(x, 0()),
         if(true(), x, y) -> p y,
        if(false(), x, y) -> bitIter(half x, y)}
       Fail
      
      
      
      
      SCC (1):
       Strict:
        {inc# s x -> inc# x}
       Weak:
       {         half 0() -> 0(),
               half s 0() -> 0(),
               half s s x -> s half x,
                  inc 0() -> 0(),
                  inc s x -> s inc x,
                 zero 0() -> true(),
                 zero s x -> false(),
                    p 0() -> 0(),
                    p s x -> x,
            bitIter(x, y) -> if(zero x, x, inc y),
                   bits x -> bitIter(x, 0()),
         if(true(), x, y) -> p y,
        if(false(), x, y) -> bitIter(half x, y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = 0,
         
         [bitIter](x0, x1) = x0 + x1 + 1,
         
         [half](x0) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [inc](x0) = x0 + 1,
         
         [zero](x0) = 0,
         
         [p](x0) = x0 + 1,
         
         [bits](x0) = 0,
         
         [0] = 1,
         
         [true] = 0,
         
         [false] = 0,
         
         [inc#](x0) = x0
        Strict:
         inc# s x -> inc# x
         1 + 1x >= 0 + 1x
        Weak:
         if(false(), x, y) -> bitIter(half x, y)
         0 + 0x + 0y >= 2 + 1x + 1y
         if(true(), x, y) -> p y
         0 + 0x + 0y >= 1 + 1y
         bits x -> bitIter(x, 0())
         0 + 0x >= 2 + 1x
         bitIter(x, y) -> if(zero x, x, inc y)
         1 + 1x + 1y >= 0 + 0x + 0y
         p s x -> x
         2 + 1x >= 1x
         p 0() -> 0()
         2 >= 1
         zero s x -> false()
         0 + 0x >= 0
         zero 0() -> true()
         0 >= 0
         inc s x -> s inc x
         2 + 1x >= 2 + 1x
         inc 0() -> 0()
         2 >= 1
         half s s x -> s half x
         3 + 1x >= 2 + 1x
         half s 0() -> 0()
         3 >= 1
         half 0() -> 0()
         2 >= 1
       Qed
     SCC (1):
      Strict:
       {half# s s x -> half# x}
      Weak:
      {         half 0() -> 0(),
              half s 0() -> 0(),
              half s s x -> s half x,
                 inc 0() -> 0(),
                 inc s x -> s inc x,
                zero 0() -> true(),
                zero s x -> false(),
                   p 0() -> 0(),
                   p s x -> x,
           bitIter(x, y) -> if(zero x, x, inc y),
                  bits x -> bitIter(x, 0()),
        if(true(), x, y) -> p y,
       if(false(), x, y) -> bitIter(half x, y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = 0,
        
        [bitIter](x0, x1) = 0,
        
        [half](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [inc](x0) = 0,
        
        [zero](x0) = 0,
        
        [p](x0) = 0,
        
        [bits](x0) = 0,
        
        [0] = 0,
        
        [true] = 0,
        
        [false] = 0,
        
        [half#](x0) = x0
       Strict:
        half# s s x -> half# x
        2 + 1x >= 0 + 1x
       Weak:
        if(false(), x, y) -> bitIter(half x, y)
        0 + 0x + 0y >= 0 + 0x + 0y
        if(true(), x, y) -> p y
        0 + 0x + 0y >= 0 + 0y
        bits x -> bitIter(x, 0())
        0 + 0x >= 0 + 0x
        bitIter(x, y) -> if(zero x, x, inc y)
        0 + 0x + 0y >= 0 + 0x + 0y
        p s x -> x
        0 + 0x >= 1x
        p 0() -> 0()
        0 >= 0
        zero s x -> false()
        0 + 0x >= 0
        zero 0() -> true()
        0 >= 0
        inc s x -> s inc x
        0 + 0x >= 1 + 0x
        inc 0() -> 0()
        0 >= 0
        half s s x -> s half x
        0 + 0x >= 1 + 0x
        half s 0() -> 0()
        0 >= 0
        half 0() -> 0()
        0 >= 0
      Qed