MAYBE

Problem:
 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)))

Proof:
 DP Processor:
  DPs:
   half#(s(s(x))) -> half#(x)
   lastbit#(s(s(x))) -> lastbit#(x)
   conv#(s(x)) -> lastbit#(s(x))
   conv#(s(x)) -> half#(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)))
  Usable Rule Processor:
   DPs:
    half#(s(s(x))) -> half#(x)
    lastbit#(s(s(x))) -> lastbit#(x)
    conv#(s(x)) -> lastbit#(s(x))
    conv#(s(x)) -> half#(s(x))
    conv#(s(x)) -> conv#(half(s(x)))
   TRS:
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    half(0()) -> 0()
   TDG Processor:
    DPs:
     half#(s(s(x))) -> half#(x)
     lastbit#(s(s(x))) -> lastbit#(x)
     conv#(s(x)) -> lastbit#(s(x))
     conv#(s(x)) -> half#(s(x))
     conv#(s(x)) -> conv#(half(s(x)))
    TRS:
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
    graph:
     conv#(s(x)) -> conv#(half(s(x))) ->
     conv#(s(x)) -> conv#(half(s(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)) -> lastbit#(s(x)) -> lastbit#(s(s(x))) -> lastbit#(x)
     conv#(s(x)) -> half#(s(x)) -> half#(s(s(x))) -> half#(x)
     lastbit#(s(s(x))) -> lastbit#(x) -> lastbit#(s(s(x))) -> lastbit#(x)
     half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    Restore Modifier:
     DPs:
      half#(s(s(x))) -> half#(x)
      lastbit#(s(s(x))) -> lastbit#(x)
      conv#(s(x)) -> lastbit#(s(x))
      conv#(s(x)) -> half#(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)))
     SCC Processor:
      #sccs: 3
      #rules: 3
      #arcs: 7/25
      DPs:
       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)))
      Open
      
      DPs:
       half#(s(s(x))) -> half#(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)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [half#](x0) = x0,
        
        [cons](x0, x1) = 1,
        
        [nil] = 0,
        
        [conv](x0) = x0,
        
        [lastbit](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [half](x0) = x0,
        
        [0] = 1
       orientation:
        half#(s(s(x))) = x + 2 >= x = half#(x)
        
        half(0()) = 1 >= 1 = 0()
        
        half(s(0())) = 2 >= 1 = 0()
        
        half(s(s(x))) = x + 2 >= x + 1 = s(half(x))
        
        lastbit(0()) = 1 >= 1 = 0()
        
        lastbit(s(0())) = 2 >= 2 = s(0())
        
        lastbit(s(s(x))) = x + 2 >= x = lastbit(x)
        
        conv(0()) = 1 >= 1 = cons(nil(),0())
        
        conv(s(x)) = x + 1 >= 1 = cons(conv(half(s(x))),lastbit(s(x)))
       problem:
        DPs:
         
        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)))
       Qed
      
      DPs:
       lastbit#(s(s(x))) -> lastbit#(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)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [lastbit#](x0) = x0,
        
        [cons](x0, x1) = 1,
        
        [nil] = 0,
        
        [conv](x0) = x0,
        
        [lastbit](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [half](x0) = x0,
        
        [0] = 1
       orientation:
        lastbit#(s(s(x))) = x + 2 >= x = lastbit#(x)
        
        half(0()) = 1 >= 1 = 0()
        
        half(s(0())) = 2 >= 1 = 0()
        
        half(s(s(x))) = x + 2 >= x + 1 = s(half(x))
        
        lastbit(0()) = 1 >= 1 = 0()
        
        lastbit(s(0())) = 2 >= 2 = s(0())
        
        lastbit(s(s(x))) = x + 2 >= x = lastbit(x)
        
        conv(0()) = 1 >= 1 = cons(nil(),0())
        
        conv(s(x)) = x + 1 >= 1 = cons(conv(half(s(x))),lastbit(s(x)))
       problem:
        DPs:
         
        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)))
       Qed