YES

TRS:

  half(0()) -> 0()
  half(s(0())) -> 0()
  half(s(s(x))) -> s(half(x))
  le(0(),y) -> true()
  le(s(x),0()) -> false()
  le(s(x),s(y)) -> le(x,y)
  inc(0()) -> 0()
  inc(s(x)) -> s(inc(x))
  log(x) -> log2(x,0())
  log2(x,y) -> if(le(x,s(0())),x,inc(y))
  if(true(),x,s(y)) -> y
  if(false(),x,y) -> log2(half(x),y)

max/plus interpretations on N:

  half_A(x1) = max{2, -1 + x1}
  half#_A(x1) = max{11, 12}
  0_A = 2
  0#_A = 4
  s_A(x1) = max{9, 4 + x1}
  s#_A(x1) = max{1, 2}
  le_A(x1,x2) = max{5, 1 + x1, 3}
  le#_A(x1,x2) = max{1, -1, 2}
  true_A = 4
  true#_A = 0
  false_A = 10
  false#_A = 3
  inc_A(x1) = max{1, x1}
  inc#_A(x1) = max{3, -6}
  log_A(x1) = max{2, 4}
  log#_A(x1) = max{12, 8 + x1}
  log2_A(x1,x2) = max{4, 3, 1 + x2}
  log2#_A(x1,x2) = max{5, 7 + x1, 11}
  if_A(x1,x2,x3) = max{0, 4, 2, 1 + x3}
  if#_A(x1,x2,x3) = max{10, 3 + x1, 6 + x2, 8}

precedence:

  log = if > log2 > half = inc > 0 > false > s = le > true