YES

TRS:

  ++(nil(),y) -> y
  ++(x,nil()) -> x
  ++(.(x,y),z) -> .(x,++(y,z))
  ++(++(x,y),z) -> ++(x,++(y,z))

linear polynomial interpretations on N:

  ++_A(x1,x2) = x1 + x2 + 1
  ++#_A(x1,x2) = x1 + x2 + 1
  nil_A = 0
  nil#_A = 0
  ._A(x1,x2) = x1 + x2 + 1
  .#_A(x1,x2) = x1 + x2 + 1

precedence:

  ++ = nil > .