YES

Problem:
 +(-(x,y),z) -> -(+(x,z),y)
 -(+(x,y),y) -> x

Proof:
 Bounds Processor:
  bound: 0
  enrichment: top
  automaton:
   final states: {7,6,2,1}
   transitions:
    f20() -> 6*,1,3,2
    -0(6,2) -> 7*
    -0(6,6) -> 7*
    -0(3,2) -> 7*,3,1
    -0(3,6) -> 7*
    -0(7,2) -> 7*
    -0(7,6) -> 7*
    +0(6,2) -> 3*
    +0(6,6) -> 3*
    +0(2,2) -> 3*
    +0(2,6) -> 3*
    1 -> 3*
    2 -> 7,1
    6 -> 7*
  problem:
   
  Qed