YES

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))
  TDG 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))
   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) -> ifb#(lt(y,x),x,y)
    ifb#(true(),x,y) -> help#(half(x),s(y)) ->
    help#(x,y) -> lt#(y,x)
    help#(x,y) -> ifb#(lt(y,x),x,y) ->
    ifb#(true(),x,y) -> help#(half(x),s(y))
    help#(x,y) -> ifb#(lt(y,x),x,y) -> ifb#(true(),x,y) -> half#(x)
    help#(x,y) -> lt#(y,x) -> lt#(s(x),s(y)) -> lt#(x,y)
    ifa#(true(),x) -> help#(x,1()) -> help#(x,y) -> ifb#(lt(y,x),x,y)
    ifa#(true(),x) -> help#(x,1()) -> help#(x,y) -> lt#(y,x)
    logarithm#(x) -> ifa#(lt(0(),x),x) -> ifa#(true(),x) -> help#(x,1())
    logarithm#(x) -> lt#(0(),x) -> lt#(s(x),s(y)) -> lt#(x,y)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 12/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))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [ifb#](x0, x1, x2) = 1/2x0 + 1/2x1,
      
      [help#](x0, x1) = x0 + 1/2,
      
      [half](x0) = 1/2x0,
      
      [ifb](x0, x1, x2) = 3/2x0 + 3/2x1 + x2,
      
      [logZeroError] = 0,
      
      [help](x0, x1) = 3x0 + x1,
      
      [1] = 0,
      
      [ifa](x0, x1) = 1/2x0 + 3x1 + 3,
      
      [logarithm](x0) = 7/2x0 + 7/2,
      
      [false] = 0,
      
      [true] = 1,
      
      [lt](x0, x1) = x1,
      
      [s](x0) = x0 + 1,
      
      [0] = 0
     orientation:
      ifb#(true(),x,y) = 1/2x + 1/2 >= 1/2x + 1/2 = help#(half(x),s(y))
      
      help#(x,y) = x + 1/2 >= x = ifb#(lt(y,x),x,y)
      
      lt(0(),s(x)) = x + 1 >= 1 = true()
      
      lt(x,0()) = 0 >= 0 = false()
      
      lt(s(x),s(y)) = y + 1 >= y = lt(x,y)
      
      logarithm(x) = 7/2x + 7/2 >= 7/2x + 3 = ifa(lt(0(),x),x)
      
      ifa(true(),x) = 3x + 7/2 >= 3x = help(x,1())
      
      ifa(false(),x) = 3x + 3 >= 0 = logZeroError()
      
      help(x,y) = 3x + y >= 3x + y = ifb(lt(y,x),x,y)
      
      ifb(true(),x,y) = 3/2x + y + 3/2 >= 3/2x + y + 1 = help(half(x),s(y))
      
      ifb(false(),x,y) = 3/2x + y >= y = y
      
      half(0()) = 0 >= 0 = 0()
      
      half(s(0())) = 1/2 >= 0 = 0()
      
      half(s(s(x))) = 1/2x + 1 >= 1/2x + 1 = s(half(x))
     problem:
      DPs:
       ifb#(true(),x,y) -> help#(half(x),s(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))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 1
     problem:
      DPs:
       
      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))
     Qed
    
    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))
    Subterm Criterion Processor:
     simple projection:
      pi(half#) = 0
     problem:
      DPs:
       
      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))
     Qed