MAYBE
Time: 0.029218
TRS:
 {         half 0() -> 0(),
         half s 0() -> 0(),
         half s s x -> s half x,
        lastbit 0() -> 0(),
      lastbit s 0() -> s 0(),
      lastbit s s x -> lastbit x,
           zero 0() -> true(),
           zero s x -> false(),
     conviter(x, l) -> if(zero x, x, l),
             conv x -> conviter(x, cons(0(), nil())),
   if(true(), x, l) -> l,
  if(false(), x, l) -> conviter(half x, cons(lastbit x, l))}
 DP:
  DP:
   {       half# s s x -> half# x,
        lastbit# s s x -> lastbit# x,
       conviter#(x, l) -> zero# x,
       conviter#(x, l) -> if#(zero x, x, l),
               conv# x -> conviter#(x, cons(0(), nil())),
    if#(false(), x, l) -> half# x,
    if#(false(), x, l) -> lastbit# x,
    if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l))}
  TRS:
  {         half 0() -> 0(),
          half s 0() -> 0(),
          half s s x -> s half x,
         lastbit 0() -> 0(),
       lastbit s 0() -> s 0(),
       lastbit s s x -> lastbit x,
            zero 0() -> true(),
            zero s x -> false(),
      conviter(x, l) -> if(zero x, x, l),
              conv x -> conviter(x, cons(0(), nil())),
    if(true(), x, l) -> l,
   if(false(), x, l) -> conviter(half x, cons(lastbit x, l))}
  UR:
   {     half 0() -> 0(),
       half s 0() -> 0(),
       half s s x -> s half x,
      lastbit 0() -> 0(),
    lastbit s 0() -> s 0(),
    lastbit s s x -> lastbit x,
         zero 0() -> true(),
         zero s x -> false(),
          a(y, z) -> y,
          a(y, z) -> z}
   EDG:
    {(half# s s x -> half# x, half# s s x -> half# x)
     (if#(false(), x, l) -> lastbit# x, lastbit# s s x -> lastbit# x)
     (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> if#(zero x, x, l))
     (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> zero# x)
     (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> zero# x)
     (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> if#(zero x, x, l))
     (if#(false(), x, l) -> half# x, half# s s x -> half# x)
     (lastbit# s s x -> lastbit# x, lastbit# s s x -> lastbit# x)
     (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> half# x)
     (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> lastbit# x)
     (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)))}
    EDG:
     {(half# s s x -> half# x, half# s s x -> half# x)
      (if#(false(), x, l) -> lastbit# x, lastbit# s s x -> lastbit# x)
      (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> if#(zero x, x, l))
      (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> zero# x)
      (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> zero# x)
      (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> if#(zero x, x, l))
      (if#(false(), x, l) -> half# x, half# s s x -> half# x)
      (lastbit# s s x -> lastbit# x, lastbit# s s x -> lastbit# x)
      (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> half# x)
      (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> lastbit# x)
      (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)))}
     EDG:
      {(half# s s x -> half# x, half# s s x -> half# x)
       (if#(false(), x, l) -> lastbit# x, lastbit# s s x -> lastbit# x)
       (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> if#(zero x, x, l))
       (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> zero# x)
       (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> zero# x)
       (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> if#(zero x, x, l))
       (if#(false(), x, l) -> half# x, half# s s x -> half# x)
       (lastbit# s s x -> lastbit# x, lastbit# s s x -> lastbit# x)
       (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> half# x)
       (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> lastbit# x)
       (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)))}
      EDG:
       {(half# s s x -> half# x, half# s s x -> half# x)
        (if#(false(), x, l) -> lastbit# x, lastbit# s s x -> lastbit# x)
        (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> if#(zero x, x, l))
        (conv# x -> conviter#(x, cons(0(), nil())), conviter#(x, l) -> zero# x)
        (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> zero# x)
        (if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)), conviter#(x, l) -> if#(zero x, x, l))
        (if#(false(), x, l) -> half# x, half# s s x -> half# x)
        (lastbit# s s x -> lastbit# x, lastbit# s s x -> lastbit# x)
        (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> half# x)
        (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> lastbit# x)
        (conviter#(x, l) -> if#(zero x, x, l), if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l)))}
       STATUS:
        arrows: 0.828125
        SCCS (3):
         Scc:
          {   conviter#(x, l) -> if#(zero x, x, l),
           if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l))}
         Scc:
          {lastbit# s s x -> lastbit# x}
         Scc:
          {half# s s x -> half# x}
         
         
         SCC (2):
          Strict:
           {   conviter#(x, l) -> if#(zero x, x, l),
            if#(false(), x, l) -> conviter#(half x, cons(lastbit x, l))}
          Weak:
          {         half 0() -> 0(),
                  half s 0() -> 0(),
                  half s s x -> s half x,
                 lastbit 0() -> 0(),
               lastbit s 0() -> s 0(),
               lastbit s s x -> lastbit x,
                    zero 0() -> true(),
                    zero s x -> false(),
              conviter(x, l) -> if(zero x, x, l),
                      conv x -> conviter(x, cons(0(), nil())),
            if(true(), x, l) -> l,
           if(false(), x, l) -> conviter(half x, cons(lastbit x, l))}
          Fail
         
         
         SCC (1):
          Strict:
           {lastbit# s s x -> lastbit# x}
          Weak:
          {         half 0() -> 0(),
                  half s 0() -> 0(),
                  half s s x -> s half x,
                 lastbit 0() -> 0(),
               lastbit s 0() -> s 0(),
               lastbit s s x -> lastbit x,
                    zero 0() -> true(),
                    zero s x -> false(),
              conviter(x, l) -> if(zero x, x, l),
                      conv x -> conviter(x, cons(0(), nil())),
            if(true(), x, l) -> l,
           if(false(), x, l) -> conviter(half x, cons(lastbit x, l))}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [if](x0, x1, x2) = x0 + x1 + 1,
            
            [conviter](x0, x1) = 0,
            
            [cons](x0, x1) = 0,
            
            [half](x0) = x0 + 1,
            
            [s](x0) = x0 + 1,
            
            [lastbit](x0) = x0 + 1,
            
            [zero](x0) = x0 + 1,
            
            [conv](x0) = 0,
            
            [0] = 1,
            
            [true] = 1,
            
            [false] = 1,
            
            [nil] = 0,
            
            [lastbit#](x0) = x0
           Strict:
            lastbit# s s x -> lastbit# x
            2 + 1x >= 0 + 1x
           Weak:
            if(false(), x, l) -> conviter(half x, cons(lastbit x, l))
            2 + 1x + 0l >= 0 + 0x + 0l
            if(true(), x, l) -> l
            2 + 1x + 0l >= 1l
            conv x -> conviter(x, cons(0(), nil()))
            0 + 0x >= 0 + 0x
            conviter(x, l) -> if(zero x, x, l)
            0 + 0x + 0l >= 2 + 2x + 0l
            zero s x -> false()
            2 + 1x >= 1
            zero 0() -> true()
            2 >= 1
            lastbit s s x -> lastbit x
            3 + 1x >= 1 + 1x
            lastbit s 0() -> s 0()
            3 >= 2
            lastbit 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,
                lastbit 0() -> 0(),
              lastbit s 0() -> s 0(),
              lastbit s s x -> lastbit x,
                   zero 0() -> true(),
                   zero s x -> false(),
             conviter(x, l) -> if(zero x, x, l),
                     conv x -> conviter(x, cons(0(), nil())),
           if(true(), x, l) -> l,
          if(false(), x, l) -> conviter(half x, cons(lastbit x, l))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [if](x0, x1, x2) = x0 + x1 + 1,
           
           [conviter](x0, x1) = 0,
           
           [cons](x0, x1) = 0,
           
           [half](x0) = x0 + 1,
           
           [s](x0) = x0 + 1,
           
           [lastbit](x0) = x0 + 1,
           
           [zero](x0) = x0 + 1,
           
           [conv](x0) = 0,
           
           [0] = 1,
           
           [true] = 1,
           
           [false] = 1,
           
           [nil] = 0,
           
           [half#](x0) = x0
          Strict:
           half# s s x -> half# x
           2 + 1x >= 0 + 1x
          Weak:
           if(false(), x, l) -> conviter(half x, cons(lastbit x, l))
           2 + 1x + 0l >= 0 + 0x + 0l
           if(true(), x, l) -> l
           2 + 1x + 0l >= 1l
           conv x -> conviter(x, cons(0(), nil()))
           0 + 0x >= 0 + 0x
           conviter(x, l) -> if(zero x, x, l)
           0 + 0x + 0l >= 2 + 2x + 0l
           zero s x -> false()
           2 + 1x >= 1
           zero 0() -> true()
           2 >= 1
           lastbit s s x -> lastbit x
           3 + 1x >= 1 + 1x
           lastbit s 0() -> s 0()
           3 >= 2
           lastbit 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