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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  +(0(),y) -> y
  +(x,0()) -> x
  +(s(x),y) -> s(+(x,y))
  +(x,s(y)) -> s(+(x,y))
  +(x,+(y,z)) -> +(+(x,y),z)
  +(x,y) -> +(y,x)
  
   T' = (P union S) with
  
   TRS P:+(x,+(y,z)) -> +(+(x,y),z)
         +(x,y) -> +(y,x)
  
   TRS S:+(0(),y) -> y
         +(x,0()) -> x
         +(s(x),y) -> s(+(x,y))
         +(x,s(y)) -> s(+(x,y))
  
  S is linear and P is reversible.
  
   CP(S,S) = 
  0() = 0(), s(y) = s(+(0(),y)), s(x) = s(+(x,0())), s(+(x289,0())) = 
  s(x289), s(+(x291,s(y))) = s(+(s(x291),y)), s(+(0(),x294)) = s(x294), 
  s(+(s(x),x296)) = s(+(x,s(x296)))
  
   CP(S,P union P^-1) = 
  +(y,z) = +(+(0(),y),z), +(x,z) = +(+(x,0()),z), y = +(y,0()), +(y,z) = 
  +(0(),+(y,z)), x = +(x,0()), +(x,y) = +(+(x,y),0()), x = +(0(),x), 
  +(x,y) = +(x,+(y,0())), +(x,z) = +(x,+(0(),z)), y = +(0(),y), s(+(x343,+(y,z))) = 
  +(+(s(x343),y),z), +(x,s(+(x345,z))) = +(+(x,s(x345)),z), s(+(x347,y)) = 
  +(y,s(x347)), +(s(+(x349,y)),z) = +(s(x349),+(y,z)), s(+(x351,x)) = 
  +(x,s(x351)), +(x,s(+(y,x354))) = +(+(x,y),s(x354)), s(+(x,x356)) = 
  +(s(x356),x), s(+(+(x,y),x358)) = +(x,+(y,s(x358))), +(s(+(x,x360)),z) = 
  +(x,+(s(x360),z)), s(+(y,x362)) = +(s(x362),y)
  
   CP(P union P^-1,S) = 
  +(+(0(),x444),x445) = +(x444,x445), +(+(s(x),x447),x448) = s(+(x,+(x447,x448))), 
  +(y,0()) = y, +(0(),x) = x, +(y,s(x)) = s(+(x,y)), +(s(y),x) = s(+(x,y)), 
  +(x457,+(x458,0())) = +(x457,x458), +(x460,+(x461,s(y))) = s(+(+(x460,x461),y))
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [s](x0) = x0,
    
    [+](x0, x1) = x0 + 4x1 + 4,
    
    [0] = 2
   orientation:
    +(0(),y) = 4y + 6 >= y = y
    
    +(x,0()) = x + 12 >= x = x
    
    +(s(x),y) = x + 4y + 4 >= x + 4y + 4 = s(+(x,y))
    
    +(x,s(y)) = x + 4y + 4 >= x + 4y + 4 = s(+(x,y))
   problem:
    +(s(x),y) -> s(+(x,y))
    +(x,s(y)) -> s(+(x,y))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [s](x0) = x0 + 1,
     
     [+](x0, x1) = x0 + 2x1 + 5
    orientation:
     +(s(x),y) = x + 2y + 6 >= x + 2y + 6 = s(+(x,y))
     
     +(x,s(y)) = x + 2y + 7 >= x + 2y + 6 = s(+(x,y))
    problem:
     +(s(x),y) -> s(+(x,y))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [s](x0) = x0 + 1,
      
      [+](x0, x1) = 2x0 + 4x1 + 5
     orientation:
      +(s(x),y) = 2x + 4y + 7 >= 2x + 4y + 6 = s(+(x,y))
     problem:
      
     Qed