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))))
  TDG 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))))
   graph:
    bits#(s(x)) -> bits#(half(s(x))) ->
    bits#(s(x)) -> bits#(half(s(x)))
    bits#(s(x)) -> bits#(half(s(x))) -> bits#(s(x)) -> 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)
   CDG 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))))
    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)))
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 2/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