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),
          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:
  Strict:
   {    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))}
  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))}
  EDG:
   {(if#(false(), x, l) -> conviter#(half(x), cons(lastbit(x), l)), conviter#(x, l) -> if#(zero(x), x, l))
    (if#(false(), x, l) -> conviter#(half(x), cons(lastbit(x), l)), conviter#(x, l) -> zero#(x))
    (lastbit#(s(s(x))) -> lastbit#(x), lastbit#(s(s(x))) -> lastbit#(x))
    (if#(false(), x, l) -> half#(x), half#(s(s(x))) -> half#(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) -> lastbit#(x), lastbit#(s(s(x))) -> lastbit#(x))
    (half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(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)))}
   SCCS:
    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:
     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:
     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))}
     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),
              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))}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed