YES(?,O(n^2))
TRS:
 {
    half 0() -> 0(),
  half s 0() -> 0(),
  half s s x -> s half x,
    bits 0() -> 0(),
    bits s x -> s bits 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,
      bits 0() -> 0(),
      bits s x -> s bits 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(bits) x -> half(s) s(half) half(bits) x,
     half(bits) bits(0) 0() -> half(0) 0(),
       half(bits) bits(s) s(0) x -> half(s) s(bits) bits(half) half(s) s(0) x,
       half(bits) bits(s) s(half) x ->
     half(s) s(bits) bits(half) half(s) s(half) x,
       half(bits) bits(s) s(s) x -> half(s) s(bits) bits(half) half(s) s(s) x,
       half(bits) bits(s) s(bits) x ->
     half(s) s(bits) bits(half) half(s) s(bits) 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(bits) x -> s(s) s(half) half(bits) x,
     s(bits) bits(0) 0() -> s(0) 0(),
       s(bits) bits(s) s(0) x -> s(s) s(bits) bits(half) half(s) s(0) x,
       s(bits) bits(s) s(half) x -> s(s) s(bits) bits(half) half(s) s(half) x,
       s(bits) bits(s) s(s) x -> s(s) s(bits) bits(half) half(s) s(s) x,
       s(bits) bits(s) s(bits) x -> s(s) s(bits) bits(half) half(s) s(bits) x,
     bits(half) half(0) 0() -> bits(0) 0(),
     bits(half) half(s) s(0) 0() -> bits(0) 0(),
       bits(half) half(s) s(s) s(0) x -> bits(s) s(half) half(0) x,
       bits(half) half(s) s(s) s(half) x -> bits(s) s(half) half(half) x,
       bits(half) half(s) s(s) s(s) x -> bits(s) s(half) half(s) x,
       bits(half) half(s) s(s) s(bits) x -> bits(s) s(half) half(bits) x,
     bits(bits) bits(0) 0() -> bits(0) 0(),
       bits(bits) bits(s) s(0) x -> bits(s) s(bits) bits(half) half(s) s(0) x,
       bits(bits) bits(s) s(half) x ->
     bits(s) s(bits) bits(half) half(s) s(half) x,
       bits(bits) bits(s) s(s) x -> bits(s) s(bits) bits(half) half(s) s(s) x,
       bits(bits) bits(s) s(bits) x ->
     bits(s) s(bits) bits(half) half(s) s(bits) x
    }
   Weak:
    {}
   Matrix Interpretation:
    Interpretation class: triangular
              [X1]    [1 2][X1]   [3]
    [bits(3)]([X0]) = [0 1][X0] + [2]
    
              [X1]    [1 3][X1]   [1]
    [bits(2)]([X0]) = [0 1][X0] + [2]
    
              [X1]    [1 1][X1]   [0]
    [bits(1)]([X0]) = [0 1][X0] + [0]
    
              [X1]    [1 0][X1]   [3]
    [bits(0)]([X0]) = [0 0][X0] + [2]
    
           [X1]    [1 0][X1]   [0]
    [s(3)]([X0]) = [0 1][X0] + [0]
    
           [X1]    [1 1][X1]   [0]
    [s(2)]([X0]) = [0 1][X0] + [2]
    
           [X1]    [1 0][X1]   [0]
    [s(1)]([X0]) = [0 1][X0] + [0]
    
           [X1]    [1 0][X1]   [0]
    [s(0)]([X0]) = [0 0][X0] + [2]
    
              [X1]    [1 0][X1]   [0]
    [half(3)]([X0]) = [0 1][X0] + [0]
    
              [X1]    [1 1][X1]   [0]
    [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 0][X0] + [2]
    
          [0]
    [0] = [0]
    
    
    Qed