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

Proof:
 Church Rosser Transformation Processor (dup):
  
  strict:
   
  weak:
   +(+(x,y),z) -> +(x,+(y,z))
   +(x,+(y,z)) -> +(+(x,y),z)
  critical peaks: 6
  +(+(x27,+(x28,y)),z) <-0|0[]- +(+(+(x27,x28),y),z) -0|[]-> +(+(x27,x28),+(y,z))
  +(x30,+(x31,+(y,z))) <-0|[]- +(+(x30,x31),+(y,z)) -1|[]-> +(+(+(x30,x31),y),z)
  +(x,+(x33,+(x34,z))) <-0|1[]- +(x,+(+(x33,x34),z)) -1|[]-> +(+(x,+(x33,x34)),z)
  +(+(+(x,y),x37),x38) <-1|[]- +(+(x,y),+(x37,x38)) -0|[]-> +(x,+(y,+(x37,x38)))
  +(+(+(x,x40),x41),z) <-1|0[]- +(+(x,+(x40,x41)),z) -0|[]-> +(x,+(+(x40,x41),z))
  +(x,+(+(y,x43),x44)) <-1|1[]- +(x,+(y,+(x43,x44))) -1|[]-> +(+(x,y),+(x43,x44))
  Shift Processor (no label):
   
   strict:
    
   weak:
    
   Shift Processor lab=left (dd):
    
    strict:
     +(+(+(x27,x28),y),z) -> +(+(x27,+(x28,y)),z)
     +(+(+(x27,x28),y),z) -> +(+(x27,x28),+(y,z))
     +(+(x27,+(x28,y)),z) -> +(+(+(x27,x28),y),z)
     +(+(x27,x28),+(y,z)) -> +(+(+(x27,x28),y),z)
     +(+(x30,x31),+(y,z)) -> +(x30,+(x31,+(y,z)))
     +(+(x30,x31),+(y,z)) -> +(+(+(x30,x31),y),z)
     +(x30,+(x31,+(y,z))) -> +(+(x30,x31),+(y,z))
     +(+(+(x30,x31),y),z) -> +(+(x30,x31),+(y,z))
     +(x,+(+(x33,x34),z)) -> +(x,+(x33,+(x34,z)))
     +(x,+(+(x33,x34),z)) -> +(+(x,+(x33,x34)),z)
     +(x,+(x33,+(x34,z))) -> +(x,+(+(x33,x34),z))
     +(+(x,+(x33,x34)),z) -> +(x,+(+(x33,x34),z))
     +(+(x,y),+(x37,x38)) -> +(+(+(x,y),x37),x38)
     +(+(x,y),+(x37,x38)) -> +(x,+(y,+(x37,x38)))
     +(+(+(x,y),x37),x38) -> +(+(x,y),+(x37,x38))
     +(x,+(y,+(x37,x38))) -> +(+(x,y),+(x37,x38))
     +(+(x,+(x40,x41)),z) -> +(+(+(x,x40),x41),z)
     +(+(x,+(x40,x41)),z) -> +(x,+(+(x40,x41),z))
     +(+(+(x,x40),x41),z) -> +(+(x,+(x40,x41)),z)
     +(x,+(+(x40,x41),z)) -> +(+(x,+(x40,x41)),z)
     +(x,+(y,+(x43,x44))) -> +(x,+(+(y,x43),x44))
     +(x,+(y,+(x43,x44))) -> +(+(x,y),+(x43,x44))
     +(x,+(+(y,x43),x44)) -> +(x,+(y,+(x43,x44)))
     +(+(x,y),+(x43,x44)) -> +(x,+(y,+(x43,x44)))
    weak:
     +(+(x,y),z) -> +(x,+(y,z))
     +(x,+(y,z)) -> +(+(x,y),z)
    Shift Processor (ldh) lab=left (force):
     
     strict:
      
     weak:
      
     Decreasing Processor:
      The following diagrams are decreasing:
      peak:
       +(+(x27,+(x28,y)),z) <-0|0[1]- +(+(+(x27,x28),y),z) -0|[1]-> +(+(x27,x28),+(y,z))
      joins:
       +(+(x27,+(x28,y)),z) -1|0[1]-> +(+(+(x27,x28),y),z)
       +(+(x27,x28),+(y,z)) -1|[1]-> +(+(+(x27,x28),y),z)
      peak:
       +(x30,+(x31,+(y,z))) <-0|[1]- +(+(x30,x31),+(y,z)) -1|[1]-> +(+(+(x30,x31),y),z)
      joins:
       +(x30,+(x31,+(y,z))) -1|[1]-> +(+(x30,x31),+(y,z))
       +(+(+(x30,x31),y),z) -0|[1]-> +(+(x30,x31),+(y,z))
      peak:
       +(x,+(x33,+(x34,z))) <-0|1[1]- +(x,+(+(x33,x34),z)) -1|[1]-> +(+(x,+(x33,x34)),z)
      joins:
       +(x,+(x33,+(x34,z))) -1|1[1]-> +(x,+(+(x33,x34),z))
       +(+(x,+(x33,x34)),z) -0|[1]-> +(x,+(+(x33,x34),z))
      peak:
       +(+(+(x,y),x37),x38) <-1|[1]- +(+(x,y),+(x37,x38)) -0|[1]-> +(x,+(y,+(x37,x38)))
      joins:
       +(+(+(x,y),x37),x38) -0|[1]-> +(+(x,y),+(x37,x38))
       +(x,+(y,+(x37,x38))) -1|[1]-> +(+(x,y),+(x37,x38))
      peak:
       +(+(+(x,x40),x41),z) <-1|0[1]- +(+(x,+(x40,x41)),z) -0|[1]-> +(x,+(+(x40,x41),z))
      joins:
       +(+(+(x,x40),x41),z) -0|0[1]-> +(+(x,+(x40,x41)),z)
       +(x,+(+(x40,x41),z)) -1|[1]-> +(+(x,+(x40,x41)),z)
      peak:
       +(x,+(+(y,x43),x44)) <-1|1[1]- +(x,+(y,+(x43,x44))) -1|[1]-> +(+(x,y),+(x43,x44))
      joins:
       +(x,+(+(y,x43),x44)) -0|1[1]-> +(x,+(y,+(x43,x44)))
       +(+(x,y),+(x43,x44)) -0|[1]-> +(x,+(y,+(x43,x44)))
      Qed