YES
TRS:
 {    half(0()) -> 0(),
  half(s(s(x))) -> s(half(x)),
    log(s(0())) -> 0(),
   log(s(s(x))) -> s(log(s(half(x))))}
 DP:
  Strict:
   {half#(s(s(x))) -> half#(x),
     log#(s(s(x))) -> half#(x),
     log#(s(s(x))) -> log#(s(half(x)))}
  Weak:
  {    half(0()) -> 0(),
   half(s(s(x))) -> s(half(x)),
     log(s(0())) -> 0(),
    log(s(s(x))) -> s(log(s(half(x))))}
  EDG:
   {(half#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))
    (log#(s(s(x))) -> half#(x), half#(s(s(x))) -> half#(x))
    (log#(s(s(x))) -> log#(s(half(x))), log#(s(s(x))) -> half#(x))
    (log#(s(s(x))) -> log#(s(half(x))), log#(s(s(x))) -> log#(s(half(x))))}
   SCCS:
    Scc:
     {log#(s(s(x))) -> log#(s(half(x)))}
    Scc:
     {half#(s(s(x))) -> half#(x)}
    SCC:
     Strict:
      {log#(s(s(x))) -> log#(s(half(x)))}
     Weak:
     {    half(0()) -> 0(),
      half(s(s(x))) -> s(half(x)),
        log(s(0())) -> 0(),
       log(s(s(x))) -> s(log(s(half(x))))}
     POLY:
      Argument Filtering:
       pi(log#) = 0, pi(log) = [], pi(s) = [0], pi(half) = 0, pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [s](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {    half(0()) -> 0(),
        half(s(s(x))) -> s(half(x)),
          log(s(0())) -> 0(),
         log(s(s(x))) -> s(log(s(half(x))))}
      Qed
    SCC:
     Strict:
      {half#(s(s(x))) -> half#(x)}
     Weak:
     {    half(0()) -> 0(),
      half(s(s(x))) -> s(half(x)),
        log(s(0())) -> 0(),
       log(s(s(x))) -> s(log(s(half(x))))}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed