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

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