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)
   EDG 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) -> 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)
    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))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [ifb#](x0, x1, x2) = 3x0 + 3/2x1,
       
       [help#](x0, x1) = 3x0 + 1,
       
       [half](x0) = 1/2x0,
       
       [ifb](x0, x1, x2) = 2x0 + 3/2x1 + x2,
       
       [logZeroError] = 0,
       
       [help](x0, x1) = 3x0 + x1,
       
       [1] = 0,
       
       [ifa](x0, x1) = 3x1 + 7/2,
       
       [logarithm](x0) = 3x0 + 7/2,
       
       [false] = 0,
       
       [true] = 1/2,
       
       [lt](x0, x1) = 1/2x1,
       
       [s](x0) = x0 + 1,
       
       [0] = 0
      orientation:
       ifb#(true(),x,y) = 3/2x + 3/2 >= 3/2x + 1 = help#(half(x),s(y))
       
       help#(x,y) = 3x + 1 >= 3x = ifb#(lt(y,x),x,y)
       
       lt(0(),s(x)) = 1/2x + 1/2 >= 1/2 = true()
       
       lt(x,0()) = 0 >= 0 = false()
       
       lt(s(x),s(y)) = 1/2y + 1/2 >= 1/2y = lt(x,y)
       
       logarithm(x) = 3x + 7/2 >= 3x + 7/2 = ifa(lt(0(),x),x)
       
       ifa(true(),x) = 3x + 7/2 >= 3x = help(x,1())
       
       ifa(false(),x) = 3x + 7/2 >= 0 = logZeroError()
       
       help(x,y) = 3x + y >= 5/2x + y = ifb(lt(y,x),x,y)
       
       ifb(true(),x,y) = 3/2x + y + 1 >= 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:
        
       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:
      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))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [lt#](x0, x1) = 2x0,
       
       [half](x0) = 1/2x0,
       
       [ifb](x0, x1, x2) = 1/2x0 + x1 + x2,
       
       [logZeroError] = 0,
       
       [help](x0, x1) = 2x0 + x1,
       
       [1] = 1/2,
       
       [ifa](x0, x1) = 2x1 + 1/2,
       
       [logarithm](x0) = 3x0 + 2,
       
       [false] = 0,
       
       [true] = 2,
       
       [lt](x0, x1) = 2x1,
       
       [s](x0) = x0 + 1,
       
       [0] = 0
      orientation:
       lt#(s(x),s(y)) = 2x + 2 >= 2x = lt#(x,y)
       
       lt(0(),s(x)) = 2x + 2 >= 2 = true()
       
       lt(x,0()) = 0 >= 0 = false()
       
       lt(s(x),s(y)) = 2y + 2 >= 2y = lt(x,y)
       
       logarithm(x) = 3x + 2 >= 2x + 1/2 = ifa(lt(0(),x),x)
       
       ifa(true(),x) = 2x + 1/2 >= 2x + 1/2 = help(x,1())
       
       ifa(false(),x) = 2x + 1/2 >= 0 = logZeroError()
       
       help(x,y) = 2x + y >= 2x + y = ifb(lt(y,x),x,y)
       
       ifb(true(),x,y) = x + y + 1 >= x + y + 1 = help(half(x),s(y))
       
       ifb(false(),x,y) = x + 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:
        
       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))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [half#](x0) = 1/2x0 + 1/2,
       
       [half](x0) = 1/2x0,
       
       [ifb](x0, x1, x2) = x0 + 3/2x1 + x2,
       
       [logZeroError] = 0,
       
       [help](x0, x1) = 3x0 + x1,
       
       [1] = 1/2,
       
       [ifa](x0, x1) = 3x1 + 1/2,
       
       [logarithm](x0) = 3x0 + 1/2,
       
       [false] = 0,
       
       [true] = 3/2,
       
       [lt](x0, x1) = 3/2x1,
       
       [s](x0) = x0 + 1,
       
       [0] = 0
      orientation:
       half#(s(s(x))) = 1/2x + 3/2 >= 1/2x + 1/2 = half#(x)
       
       lt(0(),s(x)) = 3/2x + 3/2 >= 3/2 = true()
       
       lt(x,0()) = 0 >= 0 = false()
       
       lt(s(x),s(y)) = 3/2y + 3/2 >= 3/2y = lt(x,y)
       
       logarithm(x) = 3x + 1/2 >= 3x + 1/2 = ifa(lt(0(),x),x)
       
       ifa(true(),x) = 3x + 1/2 >= 3x + 1/2 = help(x,1())
       
       ifa(false(),x) = 3x + 1/2 >= 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:
        
       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