MAYBE
Time: 0.008231
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)}
   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)}
     SPSC:
      Simple Projection:
       pi(lastbit#) = 0
      Strict:
       {}
      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)}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed