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

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   +(0)(x) -> +(1)(x)
   +(1)(y) -> +(0)(y)
   -(0)(+(0)(x)) -> +(0)(-(0)(x))
   -(0)(+(1)(y)) -> +(1)(-(0)(y))
  critical peaks: 1
  -(+(y,x)) <-1|0[]- -(+(x,y)) -0|[]-> +(-(x),-(y))
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [-(0)](x0) = 2x0,
    
    [+(1)](x0) = x0 + 1,
    
    [+(0)](x0) = x0 + 1
   orientation:
    +(0)(x) = x + 1 >= x + 1 = +(1)(x)
    
    +(1)(y) = y + 1 >= y + 1 = +(0)(y)
    
    -(0)(+(0)(x)) = 2x + 2 >= 2x + 1 = +(0)(-(0)(x))
    
    -(0)(+(1)(y)) = 2y + 2 >= 2y + 1 = +(1)(-(0)(y))
   problem:
    
    strict:
     
    weak:
     +(0)(x) -> +(1)(x)
     +(1)(y) -> +(0)(y)
   Shift Processor lab=left (dd):
    
    strict:
     -(+(x,y)) -> -(+(y,x))
     -(+(x,y)) -> +(-(x),-(y))
     -(+(y,x)) -> +(-(y),-(x))
     +(-(x),-(y)) -> +(-(y),-(x))
    weak:
     -(+(x,y)) -> +(-(x),-(y))
     +(x,y) -> +(y,x)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [-](x0) = 4x0 + 2,
      
      [+](x0, x1) = x0 + x1 + 2
     orientation:
      -(+(x,y)) = 4x + 4y + 10 >= 4x + 4y + 10 = -(+(y,x))
      
      -(+(x,y)) = 4x + 4y + 10 >= 4x + 4y + 6 = +(-(x),-(y))
      
      -(+(y,x)) = 4x + 4y + 10 >= 4x + 4y + 6 = +(-(y),-(x))
      
      +(-(x),-(y)) = 4x + 4y + 6 >= 4x + 4y + 6 = +(-(y),-(x))
      
      +(x,y) = x + y + 2 >= x + y + 2 = +(y,x)
     problem:
      
      strict:
       -(+(x,y)) -> -(+(y,x))
       +(-(x),-(y)) -> +(-(y),-(x))
      weak:
       +(x,y) -> +(y,x)
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        -(+(y,x)) <-1|0[1,0]- -(+(x,y)) -0|[1,0]-> +(-(x),-(y))
       joins:
        -(+(y,x)) -0|[1,0]-> +(-(y),-(x))
        +(-(x),-(y)) -1|[0,0]-> +(-(y),-(x))
       Qed