YES
O(n)
TRS:
 {-(-(neg(x), neg(x)), -(neg(y), neg(y))) -> -(-(x, y), -(x, y))}
 Natural interpretation:
  Strict:
   {-(-(neg(x), neg(x)), -(neg(y), neg(y))) -> -(-(x, y), -(x, y))}
  Weak:
   {}
  Interpretation class: stronglylinear
  [neg](X0) = + 1*X0 + 1
  [-](X1, X0) = + 1*X0 + 1*X1 + 0
  
  Qed