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

Proof:
 Commute Transformation Processor:
  +(+(x,y),z) -> +(x,+(y,z))
  +(x,+(y,z)) -> +(+(x,y),z)
  +(x,y) -> +(y,x)
  Church Rosser Transformation Processor (dup):
   
   strict:
    
   weak:
    +(+(x,y),z) -> +(x,+(y,z))
    +(x,+(y,z)) -> +(+(x,y),z)
    +(x,y) -> +(y,x)
   critical peaks: 12
   +(+(x43,+(x44,y)),z) <-0|0[]- +(+(+(x43,x44),y),z) -0|[]-> +(+(x43,x44),+(y,z))
   +(x46,+(x47,+(y,z))) <-0|[]- +(+(x46,x47),+(y,z)) -1|[]-> +(+(+(x46,x47),y),z)
   +(x,+(x49,+(x50,z))) <-0|1[]- +(x,+(+(x49,x50),z)) -1|[]-> +(+(x,+(x49,x50)),z)
   +(x52,+(x53,y)) <-0|[]- +(+(x52,x53),y) -2|[]-> +(y,+(x52,x53))
   +(+(+(x,y),x56),x57) <-1|[]- +(+(x,y),+(x56,x57)) -0|[]-> +(x,+(y,+(x56,x57)))
   +(+(+(x,x59),x60),z) <-1|0[]- +(+(x,+(x59,x60)),z) -0|[]-> +(x,+(+(x59,x60),z))
   +(x,+(+(y,x62),x63)) <-1|1[]- +(x,+(y,+(x62,x63))) -1|[]-> +(+(x,y),+(x62,x63))
   +(+(x,x65),x66) <-1|[]- +(x,+(x65,x66)) -2|[]-> +(+(x65,x66),x)
   +(z,+(x,y)) <-2|[]- +(+(x,y),z) -0|[]-> +(x,+(y,z))
   +(+(y,x),z) <-2|0[]- +(+(x,y),z) -0|[]-> +(x,+(y,z))
   +(+(y,z),x) <-2|[]- +(x,+(y,z)) -1|[]-> +(+(x,y),z)
   +(x,+(z,y)) <-2|1[]- +(x,+(y,z)) -1|[]-> +(+(x,y),z)
   Shift Processor (no label):
    
    strict:
     
    weak:
     
    Shift Processor lab=left (dd):
     
     strict:
      +(+(+(x43,x44),y),z) -> +(+(x43,+(x44,y)),z)
      +(+(+(x43,x44),y),z) -> +(+(x43,x44),+(y,z))
      +(+(x43,+(x44,y)),z) -> +(+(+(x43,x44),y),z)
      +(+(x43,x44),+(y,z)) -> +(+(+(x43,x44),y),z)
      +(+(x46,x47),+(y,z)) -> +(x46,+(x47,+(y,z)))
      +(+(x46,x47),+(y,z)) -> +(+(+(x46,x47),y),z)
      +(x46,+(x47,+(y,z))) -> +(+(x46,x47),+(y,z))
      +(+(+(x46,x47),y),z) -> +(+(x46,x47),+(y,z))
      +(x,+(+(x49,x50),z)) -> +(x,+(x49,+(x50,z)))
      +(x,+(+(x49,x50),z)) -> +(+(x,+(x49,x50)),z)
      +(x,+(x49,+(x50,z))) -> +(x,+(+(x49,x50),z))
      +(+(x,+(x49,x50)),z) -> +(x,+(+(x49,x50),z))
      +(+(x52,x53),y) -> +(x52,+(x53,y))
      +(+(x52,x53),y) -> +(y,+(x52,x53))
      +(x52,+(x53,y)) -> +(+(x52,x53),y)
      +(y,+(x52,x53)) -> +(+(x52,x53),y)
      +(+(x,y),+(x56,x57)) -> +(+(+(x,y),x56),x57)
      +(+(x,y),+(x56,x57)) -> +(x,+(y,+(x56,x57)))
      +(+(+(x,y),x56),x57) -> +(+(x,y),+(x56,x57))
      +(x,+(y,+(x56,x57))) -> +(+(x,y),+(x56,x57))
      +(+(x,+(x59,x60)),z) -> +(+(+(x,x59),x60),z)
      +(+(x,+(x59,x60)),z) -> +(x,+(+(x59,x60),z))
      +(+(+(x,x59),x60),z) -> +(+(x,+(x59,x60)),z)
      +(x,+(+(x59,x60),z)) -> +(+(x,+(x59,x60)),z)
      +(x,+(y,+(x62,x63))) -> +(x,+(+(y,x62),x63))
      +(x,+(y,+(x62,x63))) -> +(+(x,y),+(x62,x63))
      +(x,+(+(y,x62),x63)) -> +(x,+(y,+(x62,x63)))
      +(+(x,y),+(x62,x63)) -> +(x,+(y,+(x62,x63)))
      +(x,+(x65,x66)) -> +(+(x,x65),x66)
      +(x,+(x65,x66)) -> +(+(x65,x66),x)
      +(+(x,x65),x66) -> +(x,+(x65,x66))
      +(+(x65,x66),x) -> +(x,+(x65,x66))
      +(+(x,y),z) -> +(z,+(x,y))
      +(+(x,y),z) -> +(x,+(y,z))
      +(z,+(x,y)) -> +(+(x,y),z)
      +(x,+(y,z)) -> +(+(x,y),z)
      +(+(x,y),z) -> +(+(y,x),z)
      +(+(x,y),z) -> +(x,+(y,z))
      +(+(y,x),z) -> +(+(x,y),z)
      +(x,+(y,z)) -> +(+(x,y),z)
      +(x,+(y,z)) -> +(+(y,z),x)
      +(x,+(y,z)) -> +(+(x,y),z)
      +(+(y,z),x) -> +(x,+(y,z))
      +(+(x,y),z) -> +(x,+(y,z))
      +(x,+(y,z)) -> +(x,+(z,y))
      +(x,+(y,z)) -> +(+(x,y),z)
      +(x,+(z,y)) -> +(x,+(y,z))
      +(+(x,y),z) -> +(x,+(y,z))
     weak:
      +(+(x,y),z) -> +(x,+(y,z))
      +(x,+(y,z)) -> +(+(x,y),z)
      +(x,y) -> +(y,x)
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        +(+(x43,+(x44,y)),z) <-0|0[1]- +(+(+(x43,x44),y),z) -0|[1]-> +(+(x43,x44),+(y,z))
       joins:
        +(+(x43,+(x44,y)),z) -1|0[1]-> +(+(+(x43,x44),y),z)
        +(+(x43,x44),+(y,z)) -1|[1]-> +(+(+(x43,x44),y),z)
       peak:
        +(x46,+(x47,+(y,z))) <-0|[1]- +(+(x46,x47),+(y,z)) -1|[1]-> +(+(+(x46,x47),y),z)
       joins:
        +(x46,+(x47,+(y,z))) -1|[1]-> +(+(x46,x47),+(y,z))
        +(+(+(x46,x47),y),z) -0|[1]-> +(+(x46,x47),+(y,z))
       peak:
        +(x,+(x49,+(x50,z))) <-0|1[1]- +(x,+(+(x49,x50),z)) -1|[1]-> +(+(x,+(x49,x50)),z)
       joins:
        +(x,+(x49,+(x50,z))) -1|1[1]-> +(x,+(+(x49,x50),z))
        +(+(x,+(x49,x50)),z) -0|[1]-> +(x,+(+(x49,x50),z))
       peak:
        +(x52,+(x53,y)) <-0|[1]- +(+(x52,x53),y) -2|[1]-> +(y,+(x52,x53))
       joins:
        +(x52,+(x53,y)) -1|[1]-> +(+(x52,x53),y)
        +(y,+(x52,x53)) -2|[1]-> +(+(x52,x53),y)
       peak:
        +(+(+(x,y),x56),x57) <-1|[1]- +(+(x,y),+(x56,x57)) -0|[1]-> +(x,+(y,+(x56,x57)))
       joins:
        +(+(+(x,y),x56),x57) -0|[1]-> +(+(x,y),+(x56,x57))
        +(x,+(y,+(x56,x57))) -1|[1]-> +(+(x,y),+(x56,x57))
       peak:
        +(+(+(x,x59),x60),z) <-1|0[1]- +(+(x,+(x59,x60)),z) -0|[1]-> +(x,+(+(x59,x60),z))
       joins:
        +(+(+(x,x59),x60),z) -0|0[1]-> +(+(x,+(x59,x60)),z)
        +(x,+(+(x59,x60),z)) -1|[1]-> +(+(x,+(x59,x60)),z)
       peak:
        +(x,+(+(y,x62),x63)) <-1|1[1]- +(x,+(y,+(x62,x63))) -1|[1]-> +(+(x,y),+(x62,x63))
       joins:
        +(x,+(+(y,x62),x63)) -0|1[1]-> +(x,+(y,+(x62,x63)))
        +(+(x,y),+(x62,x63)) -0|[1]-> +(x,+(y,+(x62,x63)))
       peak:
        +(+(x,x65),x66) <-1|[1]- +(x,+(x65,x66)) -2|[1]-> +(+(x65,x66),x)
       joins:
        +(+(x,x65),x66) -0|[1]-> +(x,+(x65,x66))
        +(+(x65,x66),x) -2|[1]-> +(x,+(x65,x66))
       peak:
        +(z,+(x,y)) <-2|[1]- +(+(x,y),z) -0|[1]-> +(x,+(y,z))
       joins:
        +(z,+(x,y)) -2|[1]-> +(+(x,y),z)
        +(x,+(y,z)) -1|[1]-> +(+(x,y),z)
       peak:
        +(+(y,x),z) <-2|0[1]- +(+(x,y),z) -0|[1]-> +(x,+(y,z))
       joins:
        +(+(y,x),z) -2|0[1]-> +(+(x,y),z)
        +(x,+(y,z)) -1|[1]-> +(+(x,y),z)
       peak:
        +(+(y,z),x) <-2|[1]- +(x,+(y,z)) -1|[1]-> +(+(x,y),z)
       joins:
        +(+(y,z),x) -2|[1]-> +(x,+(y,z))
        +(+(x,y),z) -0|[1]-> +(x,+(y,z))
       peak:
        +(x,+(z,y)) <-2|1[1]- +(x,+(y,z)) -1|[1]-> +(+(x,y),z)
       joins:
        +(x,+(z,y)) -2|1[1]-> +(x,+(y,z))
        +(+(x,y),z) -0|[1]-> +(x,+(y,z))
       Qed