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)
 zero(0()) -> true()
 zero(s(x)) -> false()
 conv(x) -> conviter(x,cons(0(),nil()))
 conviter(x,l) -> if(zero(x),x,l)
 if(true(),x,l) -> l
 if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))

Proof:
 DP Processor:
  DPs:
   half#(s(s(x))) -> half#(x)
   lastbit#(s(s(x))) -> lastbit#(x)
   conv#(x) -> conviter#(x,cons(0(),nil()))
   conviter#(x,l) -> zero#(x)
   conviter#(x,l) -> if#(zero(x),x,l)
   if#(false(),x,l) -> lastbit#(x)
   if#(false(),x,l) -> half#(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()
   conv(x) -> conviter(x,cons(0(),nil()))
   conviter(x,l) -> if(zero(x),x,l)
   if(true(),x,l) -> l
   if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
  Usable Rule Processor:
   DPs:
    half#(s(s(x))) -> half#(x)
    lastbit#(s(s(x))) -> lastbit#(x)
    conv#(x) -> conviter#(x,cons(0(),nil()))
    conviter#(x,l) -> zero#(x)
    conviter#(x,l) -> if#(zero(x),x,l)
    if#(false(),x,l) -> lastbit#(x)
    if#(false(),x,l) -> half#(x)
    if#(false(),x,l) -> conviter#(half(x),cons(lastbit(x),l))
   TRS:
    f18(x,y) -> x
    f18(x,y) -> y
    zero(0()) -> true()
    zero(s(x)) -> false()
    lastbit(0()) -> 0()
    lastbit(s(0())) -> s(0())
    lastbit(s(s(x))) -> lastbit(x)
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
   CDG Processor:
    DPs:
     half#(s(s(x))) -> half#(x)
     lastbit#(s(s(x))) -> lastbit#(x)
     conv#(x) -> conviter#(x,cons(0(),nil()))
     conviter#(x,l) -> zero#(x)
     conviter#(x,l) -> if#(zero(x),x,l)
     if#(false(),x,l) -> lastbit#(x)
     if#(false(),x,l) -> half#(x)
     if#(false(),x,l) -> conviter#(half(x),cons(lastbit(x),l))
    TRS:
     f18(x,y) -> x
     f18(x,y) -> y
     zero(0()) -> true()
     zero(s(x)) -> false()
     lastbit(0()) -> 0()
     lastbit(s(0())) -> s(0())
     lastbit(s(s(x))) -> lastbit(x)
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
    graph:
     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) -> lastbit#(x) ->
     lastbit#(s(s(x))) -> lastbit#(x)
     if#(false(),x,l) -> half#(x) -> half#(s(s(x))) -> 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) -> half#(x)
     conviter#(x,l) -> if#(zero(x),x,l) ->
     if#(false(),x,l) -> conviter#(half(x),cons(lastbit(x),l))
     conv#(x) -> conviter#(x,cons(0(),nil())) ->
     conviter#(x,l) -> zero#(x)
     conv#(x) -> conviter#(x,cons(0(),nil())) ->
     conviter#(x,l) -> if#(zero(x),x,l)
     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#(x) -> conviter#(x,cons(0(),nil()))
      conviter#(x,l) -> zero#(x)
      conviter#(x,l) -> if#(zero(x),x,l)
      if#(false(),x,l) -> lastbit#(x)
      if#(false(),x,l) -> half#(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()
      conv(x) -> conviter(x,cons(0(),nil()))
      conviter(x,l) -> if(zero(x),x,l)
      if(true(),x,l) -> l
      if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 11/64
      DPs:
       if#(false(),x,l) -> conviter#(half(x),cons(lastbit(x),l))
       conviter#(x,l) -> if#(zero(x),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()
       conv(x) -> conviter(x,cons(0(),nil()))
       conviter(x,l) -> if(zero(x),x,l)
       if(true(),x,l) -> l
       if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
      Open
      
      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)
       zero(0()) -> true()
       zero(s(x)) -> false()
       conv(x) -> conviter(x,cons(0(),nil()))
       conviter(x,l) -> if(zero(x),x,l)
       if(true(),x,l) -> l
       if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [lastbit#](x0) = x0,
        
        [if](x0, x1, x2) = x2,
        
        [conviter](x0, x1) = x1,
        
        [cons](x0, x1) = x1,
        
        [nil] = 1,
        
        [conv](x0) = 1,
        
        [false] = 0,
        
        [true] = 0,
        
        [zero](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)
        
        zero(0()) = 1 >= 0 = true()
        
        zero(s(x)) = x + 1 >= 0 = false()
        
        conv(x) = 1 >= 1 = conviter(x,cons(0(),nil()))
        
        conviter(x,l) = l >= l = if(zero(x),x,l)
        
        if(true(),x,l) = l >= l = l
        
        if(false(),x,l) = l >= l = conviter(half(x),cons(lastbit(x),l))
       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)
         zero(0()) -> true()
         zero(s(x)) -> false()
         conv(x) -> conviter(x,cons(0(),nil()))
         conviter(x,l) -> if(zero(x),x,l)
         if(true(),x,l) -> l
         if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
       Qed
      
      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)
       zero(0()) -> true()
       zero(s(x)) -> false()
       conv(x) -> conviter(x,cons(0(),nil()))
       conviter(x,l) -> if(zero(x),x,l)
       if(true(),x,l) -> l
       if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [half#](x0) = x0,
        
        [if](x0, x1, x2) = x2,
        
        [conviter](x0, x1) = x1,
        
        [cons](x0, x1) = x1,
        
        [nil] = 1,
        
        [conv](x0) = 1,
        
        [false] = 0,
        
        [true] = 0,
        
        [zero](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)
        
        zero(0()) = 1 >= 0 = true()
        
        zero(s(x)) = x + 1 >= 0 = false()
        
        conv(x) = 1 >= 1 = conviter(x,cons(0(),nil()))
        
        conviter(x,l) = l >= l = if(zero(x),x,l)
        
        if(true(),x,l) = l >= l = l
        
        if(false(),x,l) = l >= l = conviter(half(x),cons(lastbit(x),l))
       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)
         zero(0()) -> true()
         zero(s(x)) -> false()
         conv(x) -> conviter(x,cons(0(),nil()))
         conviter(x,l) -> if(zero(x),x,l)
         if(true(),x,l) -> l
         if(false(),x,l) -> conviter(half(x),cons(lastbit(x),l))
       Qed