MAYBE
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:
  Strict:
   {   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)))}
  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)))}
  EDG:
   {(lastbit#(s(s(x))) -> lastbit#(x), lastbit#(s(s(x))) -> lastbit#(x))
    (conv#(s(x)) -> half#(s(x)), half#(s(s(x))) -> half#(x))
    (conv#(s(x)) -> lastbit#(s(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))))
    (half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))}
   SCCS:
    Scc:
     {conv#(s(x)) -> conv#(half(s(x)))}
    Scc:
     {lastbit#(s(s(x))) -> lastbit#(x)}
    Scc:
     {half#(s(s(x))) -> half#(x)}
    SCC:
     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:
     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)))}
     SPSC:
      Simple Projection:
       pi(lastbit#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)))}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed