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

Proof:
 Church Rosser Transformation Processor (dup):
  
  strict:
   
  weak:
   -(+(x,y)) -> +(-(x),-(y))
   +(-(x),-(y)) -> -(+(x,y))
  critical peaks: 3
  +(+(-(x22),-(x23)),-(y)) <-0|0[]- +(-(+(x22,x23)),-(y)) -1|[]-> -(+(+(x22,x23),y))
  +(-(x),+(-(x24),-(x25))) <-0|1[]- +(-(x),-(+(x24,x25))) -1|[]-> -(+(x,+(x24,x25)))
  -(-(+(x26,x27))) <-1|0[]- -(+(-(x26),-(x27))) -0|[]-> +(-(-(x26)),-(-(x27)))
  Shift Processor (no label):
   
   strict:
    
   weak:
    
   Shift Processor lab=left (dd):
    
    strict:
     +(-(+(x22,x23)),-(y)) -> +(+(-(x22),-(x23)),-(y))
     +(-(+(x22,x23)),-(y)) -> -(+(+(x22,x23),y))
     +(+(-(x22),-(x23)),-(y)) -> +(-(+(x22,x23)),-(y))
     -(+(+(x22,x23),y)) -> +(-(+(x22,x23)),-(y))
     +(-(x),-(+(x24,x25))) -> +(-(x),+(-(x24),-(x25)))
     +(-(x),-(+(x24,x25))) -> -(+(x,+(x24,x25)))
     +(-(x),+(-(x24),-(x25))) -> +(-(x),-(+(x24,x25)))
     -(+(x,+(x24,x25))) -> +(-(x),-(+(x24,x25)))
     -(+(-(x26),-(x27))) -> -(-(+(x26,x27)))
     -(+(-(x26),-(x27))) -> +(-(-(x26)),-(-(x27)))
     -(-(+(x26,x27))) -> -(+(-(x26),-(x27)))
     +(-(-(x26)),-(-(x27))) -> -(+(-(x26),-(x27)))
    weak:
     -(+(x,y)) -> +(-(x),-(y))
     +(-(x),-(y)) -> -(+(x,y))
    Shift Processor (ldh) lab=left (force):
     
     strict:
      
     weak:
      
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       +(+(-(x22),-(x23)),-(y)) <-0|0[1]- +(-(+(x22,x23)),-(y)) -1|[1]-> -(+(+(x22,x23),y))
      joins:
       +(+(-(x22),-(x23)),-(y)) -1|0[1]-> +(-(+(x22,x23)),-(y))
       -(+(+(x22,x23),y)) -0|[1]-> +(-(+(x22,x23)),-(y))
      peak:
       +(-(x),+(-(x24),-(x25))) <-0|1[1]- +(-(x),-(+(x24,x25))) -1|[1]-> -(+(x,+(x24,x25)))
      joins:
       +(-(x),+(-(x24),-(x25))) -1|1[1]-> +(-(x),-(+(x24,x25)))
       -(+(x,+(x24,x25))) -0|[1]-> +(-(x),-(+(x24,x25)))
      peak:
       -(-(+(x26,x27))) <-1|0[1]- -(+(-(x26),-(x27))) -0|[1]-> +(-(-(x26)),-(-(x27)))
      joins:
       -(-(+(x26,x27))) -0|0[1]-> -(+(-(x26),-(x27)))
       +(-(-(x26)),-(-(x27))) -1|[1]-> -(+(-(x26),-(x27)))
      Qed