YES
TRS:
 {-(-(neg(x), neg(x)), -(neg(y), neg(y))) -> -(-(x, y), -(x, y))}
 RUF:
  Strict:
   {}
  Weak:
   {}
  Qed