MAYBE
Time: 0.060393
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,
       conv 0() -> cons(nil(), 0()),
       conv s x -> cons(conv half s x, lastbit s x)}
 DP:
  DP:
   {   half# s s x -> half# x,
    lastbit# s s x -> lastbit# x,
         conv# s x -> half# s x,
         conv# s x -> lastbit# s x,
         conv# s x -> conv# half s x}
  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,
        conv 0() -> cons(nil(), 0()),
        conv s x -> cons(conv half s x, lastbit s x)}
  EDG:
   {(conv# s x -> lastbit# s x, lastbit# s s x -> lastbit# x)
    (half# s s x -> half# x, half# s s x -> half# x)
    (lastbit# s s x -> lastbit# x, lastbit# s s x -> lastbit# x)
    (conv# s x -> conv# half s x, conv# s x -> half# s x)
    (conv# s x -> conv# half s x, conv# s x -> lastbit# s x)
    (conv# s x -> conv# half s x, conv# s x -> conv# half s x)
    (conv# s x -> half# s x, half# s s x -> half# x)}
   STATUS:
    arrows: 0.720000
    SCCS (3):
     Scc:
      {conv# s x -> conv# half s x}
     Scc:
      {lastbit# s s x -> lastbit# x}
     Scc:
      {half# s s x -> half# x}
     
     SCC (1):
      Strict:
       {conv# s x -> conv# half s 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,
            conv 0() -> cons(nil(), 0()),
            conv s x -> cons(conv half s x, lastbit s x)}
      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,
            conv 0() -> cons(nil(), 0()),
            conv s x -> cons(conv half s x, lastbit s x)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = x0,
        
        [half](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [lastbit](x0) = x0 + 1,
        
        [conv](x0) = x0 + 1,
        
        [0] = 1,
        
        [nil] = 0,
        
        [lastbit#](x0) = x0
       Strict:
        lastbit# s s x -> lastbit# x
        2 + 1x >= 0 + 1x
       Weak:
        conv s x -> cons(conv half s x, lastbit s x)
        2 + 1x >= 3 + 1x
        conv 0() -> cons(nil(), 0())
        2 >= 0
        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,
           conv 0() -> cons(nil(), 0()),
           conv s x -> cons(conv half s x, lastbit s x)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [cons](x0, x1) = x0,
       
       [half](x0) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [lastbit](x0) = x0 + 1,
       
       [conv](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 0,
       
       [half#](x0) = x0
      Strict:
       half# s s x -> half# x
       2 + 1x >= 0 + 1x
      Weak:
       conv s x -> cons(conv half s x, lastbit s x)
       2 + 1x >= 3 + 1x
       conv 0() -> cons(nil(), 0())
       2 >= 0
       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