MAYBE

Problem:
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 bits(0()) -> 0()
 bits(s(x)) -> s(bits(half(s(x))))

Proof:
 DP Processor:
  DPs:
   half#(s(s(x))) -> half#(x)
   bits#(s(x)) -> half#(s(x))
   bits#(s(x)) -> bits#(half(s(x)))
  TRS:
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   bits(0()) -> 0()
   bits(s(x)) -> s(bits(half(s(x))))
  Usable Rule Processor:
   DPs:
    half#(s(s(x))) -> half#(x)
    bits#(s(x)) -> half#(s(x))
    bits#(s(x)) -> bits#(half(s(x)))
   TRS:
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    half(0()) -> 0()
   CDG Processor:
    DPs:
     half#(s(s(x))) -> half#(x)
     bits#(s(x)) -> half#(s(x))
     bits#(s(x)) -> bits#(half(s(x)))
    TRS:
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     half(0()) -> 0()
    graph:
     bits#(s(x)) -> bits#(half(s(x))) -> bits#(s(x)) -> half#(s(x))
     bits#(s(x)) -> bits#(half(s(x))) -> bits#(s(x)) -> bits#(half(s(x)))
     bits#(s(x)) -> half#(s(x)) -> half#(s(s(x))) -> half#(x)
     half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    Restore Modifier:
     DPs:
      half#(s(s(x))) -> half#(x)
      bits#(s(x)) -> half#(s(x))
      bits#(s(x)) -> bits#(half(s(x)))
     TRS:
      half(0()) -> 0()
      half(s(0())) -> 0()
      half(s(s(x))) -> s(half(x))
      bits(0()) -> 0()
      bits(s(x)) -> s(bits(half(s(x))))
     SCC Processor:
      #sccs: 2
      #rules: 2
      #arcs: 4/9
      DPs:
       bits#(s(x)) -> bits#(half(s(x)))
      TRS:
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       bits(0()) -> 0()
       bits(s(x)) -> s(bits(half(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))
       bits(0()) -> 0()
       bits(s(x)) -> s(bits(half(s(x))))
      Open