YES(?,O(n^2))
TRS:
 {
    half 0() -> 0(),
  half s 0() -> 0(),
  half s s x -> s half x,
   s log 0() -> s 0(),
     log s x -> s log half s x
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
      half 0() -> 0(),
    half s 0() -> 0(),
    half s s x -> s half x,
     s log 0() -> s 0(),
       log s x -> s log half s x
   }
  RLAB:
   Strict:
    {
     half(half) half(0) 0() -> half(0) 0(),
     half(half) half(s) s(0) 0() -> half(0) 0(),
       half(half) half(s) s(s) s(0) x -> half(s) s(half) half(0) x,
       half(half) half(s) s(s) s(half) x -> half(s) s(half) half(half) x,
       half(half) half(s) s(s) s(s) x -> half(s) s(half) half(s) x,
       half(half) half(s) s(s) s(log) x -> half(s) s(half) half(log) x,
       half(log) log(s) s(0) x -> half(s) s(log) log(half) half(s) s(0) x,
       half(log) log(s) s(half) x ->
     half(s) s(log) log(half) half(s) s(half) x,
       half(log) log(s) s(s) x -> half(s) s(log) log(half) half(s) s(s) x,
       half(log) log(s) s(log) x -> half(s) s(log) log(half) half(s) s(log) x,
     s(half) half(0) 0() -> s(0) 0(),
     s(half) half(s) s(0) 0() -> s(0) 0(),
       s(half) half(s) s(s) s(0) x -> s(s) s(half) half(0) x,
       s(half) half(s) s(s) s(half) x -> s(s) s(half) half(half) x,
       s(half) half(s) s(s) s(s) x -> s(s) s(half) half(s) x,
       s(half) half(s) s(s) s(log) x -> s(s) s(half) half(log) x,
     s(log) log(0) 0() -> s(0) 0(),
       s(log) log(s) s(0) x -> s(s) s(log) log(half) half(s) s(0) x,
       s(log) log(s) s(half) x -> s(s) s(log) log(half) half(s) s(half) x,
       s(log) log(s) s(s) x -> s(s) s(log) log(half) half(s) s(s) x,
       s(log) log(s) s(log) x -> s(s) s(log) log(half) half(s) s(log) x,
     log(half) half(0) 0() -> log(0) 0(),
     log(half) half(s) s(0) 0() -> log(0) 0(),
       log(half) half(s) s(s) s(0) x -> log(s) s(half) half(0) x,
       log(half) half(s) s(s) s(half) x -> log(s) s(half) half(half) x,
       log(half) half(s) s(s) s(s) x -> log(s) s(half) half(s) x,
       log(half) half(s) s(s) s(log) x -> log(s) s(half) half(log) x,
       log(log) log(s) s(0) x -> log(s) s(log) log(half) half(s) s(0) x,
       log(log) log(s) s(half) x -> log(s) s(log) log(half) half(s) s(half) x,
       log(log) log(s) s(s) x -> log(s) s(log) log(half) half(s) s(s) x,
       log(log) log(s) s(log) x -> log(s) s(log) log(half) half(s) s(log) x
    }
   Weak:
    {}
   Matrix Interpretation:
    Interpretation class: triangular
             [X1]    [1 3][X1]   [0]
    [log(3)]([X0]) = [0 1][X0] + [3]
    
             [X1]    [1 2][X1]   [3]
    [log(2)]([X0]) = [0 1][X0] + [3]
    
             [X1]    [1 2][X1]   [0]
    [log(1)]([X0]) = [0 1][X0] + [0]
    
             [X1]    [1 2][X1]   [0]
    [log(0)]([X0]) = [0 0][X0] + [1]
    
           [X1]    [1 1][X1]   [0]
    [s(3)]([X0]) = [0 1][X0] + [1]
    
           [X1]    [1 0][X1]   [1]
    [s(2)]([X0]) = [0 1][X0] + [3]
    
           [X1]    [1 0][X1]   [0]
    [s(1)]([X0]) = [0 1][X0] + [0]
    
           [X1]    [1 0][X1]   [1]
    [s(0)]([X0]) = [0 1][X0] + [0]
    
              [X1]    [1 1][X1]   [1]
    [half(3)]([X0]) = [0 1][X0] + [0]
    
              [X1]    [1 0][X1]   [2]
    [half(2)]([X0]) = [0 1][X0] + [0]
    
              [X1]    [1 0][X1]   [1]
    [half(1)]([X0]) = [0 1][X0] + [0]
    
              [X1]    [1 0][X1]   [2]
    [half(0)]([X0]) = [0 1][X0] + [0]
    
          [2]
    [0] = [2]
    
    
    Qed