MAYBE

Problem:
 lt(0(),s(x)) -> true()
 lt(x,0()) -> false()
 lt(s(x),s(y)) -> lt(x,y)
 logarithm(x) -> ifa(lt(0(),x),x)
 ifa(true(),x) -> help(x,1())
 ifa(false(),x) -> logZeroError()
 help(x,y) -> ifb(lt(y,x),x,y)
 ifb(true(),x,y) -> help(half(x),s(y))
 ifb(false(),x,y) -> y
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))

Proof:
 DP Processor:
  DPs:
   lt#(s(x),s(y)) -> lt#(x,y)
   logarithm#(x) -> lt#(0(),x)
   logarithm#(x) -> ifa#(lt(0(),x),x)
   ifa#(true(),x) -> help#(x,1())
   help#(x,y) -> lt#(y,x)
   help#(x,y) -> ifb#(lt(y,x),x,y)
   ifb#(true(),x,y) -> half#(x)
   ifb#(true(),x,y) -> help#(half(x),s(y))
   half#(s(s(x))) -> half#(x)
  TRS:
   lt(0(),s(x)) -> true()
   lt(x,0()) -> false()
   lt(s(x),s(y)) -> lt(x,y)
   logarithm(x) -> ifa(lt(0(),x),x)
   ifa(true(),x) -> help(x,1())
   ifa(false(),x) -> logZeroError()
   help(x,y) -> ifb(lt(y,x),x,y)
   ifb(true(),x,y) -> help(half(x),s(y))
   ifb(false(),x,y) -> y
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
  Usable Rule Processor:
   DPs:
    lt#(s(x),s(y)) -> lt#(x,y)
    logarithm#(x) -> lt#(0(),x)
    logarithm#(x) -> ifa#(lt(0(),x),x)
    ifa#(true(),x) -> help#(x,1())
    help#(x,y) -> lt#(y,x)
    help#(x,y) -> ifb#(lt(y,x),x,y)
    ifb#(true(),x,y) -> half#(x)
    ifb#(true(),x,y) -> help#(half(x),s(y))
    half#(s(s(x))) -> half#(x)
   TRS:
    f18(x,y) -> x
    f18(x,y) -> y
    lt(0(),s(x)) -> true()
    lt(x,0()) -> false()
    lt(s(x),s(y)) -> lt(x,y)
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
   CDG Processor:
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
     logarithm#(x) -> lt#(0(),x)
     logarithm#(x) -> ifa#(lt(0(),x),x)
     ifa#(true(),x) -> help#(x,1())
     help#(x,y) -> lt#(y,x)
     help#(x,y) -> ifb#(lt(y,x),x,y)
     ifb#(true(),x,y) -> half#(x)
     ifb#(true(),x,y) -> help#(half(x),s(y))
     half#(s(s(x))) -> half#(x)
    TRS:
     f18(x,y) -> x
     f18(x,y) -> y
     lt(0(),s(x)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
    graph:
     half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
     ifb#(true(),x,y) -> half#(x) ->
     half#(s(s(x))) -> half#(x)
     ifb#(true(),x,y) -> help#(half(x),s(y)) ->
     help#(x,y) -> lt#(y,x)
     ifb#(true(),x,y) -> help#(half(x),s(y)) ->
     help#(x,y) -> ifb#(lt(y,x),x,y)
     help#(x,y) -> ifb#(lt(y,x),x,y) -> ifb#(true(),x,y) -> half#(x)
     help#(x,y) -> ifb#(lt(y,x),x,y) ->
     ifb#(true(),x,y) -> help#(half(x),s(y))
     help#(x,y) -> lt#(y,x) -> lt#(s(x),s(y)) -> lt#(x,y)
     ifa#(true(),x) -> help#(x,1()) -> help#(x,y) -> lt#(y,x)
     ifa#(true(),x) -> help#(x,1()) ->
     help#(x,y) -> ifb#(lt(y,x),x,y)
     logarithm#(x) -> ifa#(lt(0(),x),x) -> ifa#(true(),x) -> help#(x,1())
     lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
    Restore Modifier:
     DPs:
      lt#(s(x),s(y)) -> lt#(x,y)
      logarithm#(x) -> lt#(0(),x)
      logarithm#(x) -> ifa#(lt(0(),x),x)
      ifa#(true(),x) -> help#(x,1())
      help#(x,y) -> lt#(y,x)
      help#(x,y) -> ifb#(lt(y,x),x,y)
      ifb#(true(),x,y) -> half#(x)
      ifb#(true(),x,y) -> help#(half(x),s(y))
      half#(s(s(x))) -> half#(x)
     TRS:
      lt(0(),s(x)) -> true()
      lt(x,0()) -> false()
      lt(s(x),s(y)) -> lt(x,y)
      logarithm(x) -> ifa(lt(0(),x),x)
      ifa(true(),x) -> help(x,1())
      ifa(false(),x) -> logZeroError()
      help(x,y) -> ifb(lt(y,x),x,y)
      ifb(true(),x,y) -> help(half(x),s(y))
      ifb(false(),x,y) -> y
      half(0()) -> 0()
      half(s(0())) -> 0()
      half(s(s(x))) -> s(half(x))
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 11/81
      DPs:
       ifb#(true(),x,y) -> help#(half(x),s(y))
       help#(x,y) -> ifb#(lt(y,x),x,y)
      TRS:
       lt(0(),s(x)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       logarithm(x) -> ifa(lt(0(),x),x)
       ifa(true(),x) -> help(x,1())
       ifa(false(),x) -> logZeroError()
       help(x,y) -> ifb(lt(y,x),x,y)
       ifb(true(),x,y) -> help(half(x),s(y))
       ifb(false(),x,y) -> y
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
      Open
      
      DPs:
       lt#(s(x),s(y)) -> lt#(x,y)
      TRS:
       lt(0(),s(x)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       logarithm(x) -> ifa(lt(0(),x),x)
       ifa(true(),x) -> help(x,1())
       ifa(false(),x) -> logZeroError()
       help(x,y) -> ifb(lt(y,x),x,y)
       ifb(true(),x,y) -> help(half(x),s(y))
       ifb(false(),x,y) -> y
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
      Open
      
      DPs:
       half#(s(s(x))) -> half#(x)
      TRS:
       lt(0(),s(x)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       logarithm(x) -> ifa(lt(0(),x),x)
       ifa(true(),x) -> help(x,1())
       ifa(false(),x) -> logZeroError()
       help(x,y) -> ifb(lt(y,x),x,y)
       ifb(true(),x,y) -> help(half(x),s(y))
       ifb(false(),x,y) -> y
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
      Open