MAYBE
Time: 0.005818
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))}
  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))}
      Open
     
     
     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))}
      Open
     
     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))}
      Open