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

Proof:
 AT confluence processor
  Complete TRS T' of input TRS:
  +(x,0()) -> x
  +(x,s(y)) -> s(+(x,y))
  +(0(),y) -> y
  +(s(x),y) -> s(+(x,y))
  *(k(),0()) -> 0()
  *(k(),s(y)) -> +(k(),*(k(),y))
  *(k(),+(x,y)) -> +(*(k(),x),*(k(),y))
  +(x,y) -> +(y,x)
  +(+(x,y),z) -> +(x,+(y,z))
  +(z,+(x,y)) -> +(+(y,z),x)
  +(z,+(x,y)) -> +(x,+(z,y))
  
   T' = (P union S) with
  
   TRS P:+(x,y) -> +(y,x)
         +(+(x,y),z) -> +(x,+(y,z))
         +(z,+(x,y)) -> +(+(y,z),x)
         +(z,+(x,y)) -> +(x,+(z,y))
  
   TRS S:+(x,0()) -> x
         +(x,s(y)) -> s(+(x,y))
         +(0(),y) -> y
         +(s(x),y) -> s(+(x,y))
         *(k(),0()) -> 0()
         *(k(),s(y)) -> +(k(),*(k(),y))
         *(k(),+(x,y)) -> +(*(k(),x),*(k(),y))
  
  S is linear and P is reversible.
  
   CP(S,S) = 
  0() = 0(), s(x) = s(+(x,0())), *(k(),x) = +(*(k(),x),*(k(),0())), s(+(0(),x1538)) = 
  s(x1538), s(+(s(x),x1540)) = s(+(x,s(x1540))), *(k(),s(+(x,x1542))) = 
  +(*(k(),x),*(k(),s(x1542))), s(y) = s(+(0(),y)), *(k(),y) = +(*(k(),0()),*(k(),y)), 
  s(+(x1546,0())) = s(x1546), s(+(x1548,s(y))) = s(+(s(x1548),y)), *(k(),s(+(x1550,y))) = 
  +(*(k(),s(x1550)),*(k(),y))
  
   CP(S,P union P^-1) = 
  x = +(0(),x), +(x,y) = +(x,+(y,0())), +(x,z) = +(x,+(0(),z)), +(z,x) = 
  +(+(0(),z),x), +(z,x) = +(x,+(z,0())), y = +(0(),y), +(x,y) = +(+(x,y),0()), 
  +(y,z) = +(z,+(0(),y)), +(y,x) = +(0(),+(x,y)), +(x,z) = +(z,+(x,0())), 
  s(+(x,x1689)) = +(s(x1689),x), s(+(+(x,y),x1691)) = +(x,+(y,s(x1691))), 
  +(s(+(x,x1693)),z) = +(x,+(s(x1693),z)), +(z,s(+(x,x1695))) = +(+(s(x1695),z),x), 
  +(z,s(+(x,x1697))) = +(x,+(z,s(x1697))), s(+(y,x1699)) = +(s(x1699),y), 
  +(x,s(+(y,x1701))) = +(+(x,y),s(x1701)), s(+(+(y,z),x1703)) = +(z,+(s(x1703),y)), 
  +(s(+(y,x1705)),x) = +(s(x1705),+(x,y)), +(x,s(+(z,x1707))) = +(z,+(x,s(x1707))), 
  y = +(y,0()), +(y,z) = +(0(),+(y,z)), +(x,y) = +(+(y,0()),x), +(z,y) = 
  +(+(y,z),0()), +(x,y) = +(x,+(0(),y)), +(z,y) = +(0(),+(z,y)), x = 
  +(x,0()), +(y,z) = +(+(0(),y),z), +(x,z) = +(+(x,0()),z), +(z,x) = 
  +(z,+(x,0())), +(z,y) = +(z,+(0(),y)), +(x,y) = +(0(),+(x,y)), s(+(x1720,y)) = 
  +(y,s(x1720)), +(s(+(x1722,y)),z) = +(s(x1722),+(y,z)), s(+(x1724,+(x,y))) = 
  +(+(y,s(x1724)),x), +(z,s(+(x1726,y))) = +(+(y,z),s(x1726)), s(+(x1728,+(x,y))) = 
  +(x,+(s(x1728),y)), +(z,s(+(x1730,y))) = +(s(x1730),+(z,y)), s(+(x1732,x)) = 
  +(x,s(x1732)), s(+(x1734,+(y,z))) = +(+(s(x1734),y),z), +(x,s(+(x1736,z))) = 
  +(+(x,s(x1736)),z), +(s(+(x1738,z)),x) = +(z,+(x,s(x1738))), s(+(x1740,+(z,y))) = 
  +(z,+(s(x1740),y)), +(x,s(+(x1742,y))) = +(s(x1742),+(x,y))
  
   CP(P union P^-1,S) = 
  +(0(),x) = x, +(s(y),x) = s(+(x,y)), +(y,0()) = y, +(y,s(x)) = s(+(x,y)), 
  *(k(),+(y,x)) = +(*(k(),x),*(k(),y)), +(x2128,+(x2129,0())) = +(x2128,x2129), 
  +(x2131,+(x2132,s(y))) = s(+(+(x2131,x2132),y)), *(k(),+(x2134,+(x2135,y))) = 
  +(*(k(),+(x2134,x2135)),*(k(),y)), +(+(x2139,0()),x2138) = +(x2138,x2139), 
  +(+(x2142,s(x)),x2141) = s(+(x,+(x2141,x2142))), *(k(),+(+(x2145,x),x2144)) = 
  +(*(k(),x),*(k(),+(x2144,x2145))), +(x2147,+(0(),x2148)) = +(x2147,x2148), 
  +(x2150,+(s(x),x2151)) = s(+(x,+(x2150,x2151))), *(k(),+(x2153,+(x,x2154))) = 
  +(*(k(),x),*(k(),+(x2153,x2154))), +(+(0(),x2166),x2167) = +(x2166,x2167), 
  +(+(s(x),x2169),x2170) = s(+(x,+(x2169,x2170))), *(k(),+(+(x,x2172),x2173)) = 
  +(*(k(),x),*(k(),+(x2172,x2173))), +(x2175,+(0(),x2174)) = +(x2174,x2175), 
  +(x2178,+(s(y),x2177)) = s(+(+(x2177,x2178),y)), *(k(),+(x2181,+(y,x2180))) = 
  +(*(k(),+(x2180,x2181)),*(k(),y)), +(x2184,+(0(),x2185)) = +(x2184,x2185), 
  +(x2187,+(s(x),x2188)) = s(+(x,+(x2187,x2188))), *(k(),+(x2190,+(x,x2191))) = 
  +(*(k(),x),*(k(),+(x2190,x2191)))
  
  
  We have to check termination of S:
  
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [*](x0, x1) = 4x0 + x1,
    
    [+](x0, x1) = x0 + x1 + 5,
    
    [k] = 0,
    
    [0] = 0,
    
    [s](x0) = x0 + 5
   orientation:
    +(x,0()) = x + 5 >= x = x
    
    +(x,s(y)) = x + y + 10 >= x + y + 10 = s(+(x,y))
    
    +(0(),y) = y + 5 >= y = y
    
    +(s(x),y) = x + y + 10 >= x + y + 10 = s(+(x,y))
    
    *(k(),0()) = 0 >= 0 = 0()
    
    *(k(),s(y)) = y + 5 >= y + 5 = +(k(),*(k(),y))
    
    *(k(),+(x,y)) = x + y + 5 >= x + y + 5 = +(*(k(),x),*(k(),y))
   problem:
    +(x,s(y)) -> s(+(x,y))
    +(s(x),y) -> s(+(x,y))
    *(k(),0()) -> 0()
    *(k(),s(y)) -> +(k(),*(k(),y))
    *(k(),+(x,y)) -> +(*(k(),x),*(k(),y))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [*](x0, x1) = x0 + 3x1,
     
     [+](x0, x1) = x0 + x1,
     
     [k] = 0,
     
     [0] = 1,
     
     [s](x0) = x0 + 6
    orientation:
     +(x,s(y)) = x + y + 6 >= x + y + 6 = s(+(x,y))
     
     +(s(x),y) = x + y + 6 >= x + y + 6 = s(+(x,y))
     
     *(k(),0()) = 3 >= 1 = 0()
     
     *(k(),s(y)) = 3y + 18 >= 3y = +(k(),*(k(),y))
     
     *(k(),+(x,y)) = 3x + 3y >= 3x + 3y = +(*(k(),x),*(k(),y))
    problem:
     +(x,s(y)) -> s(+(x,y))
     +(s(x),y) -> s(+(x,y))
     *(k(),+(x,y)) -> +(*(k(),x),*(k(),y))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [*](x0, x1) = x0 + 4x1 + 3,
      
      [+](x0, x1) = x0 + x1 + 6,
      
      [k] = 2,
      
      [s](x0) = x0
     orientation:
      +(x,s(y)) = x + y + 6 >= x + y + 6 = s(+(x,y))
      
      +(s(x),y) = x + y + 6 >= x + y + 6 = s(+(x,y))
      
      *(k(),+(x,y)) = 4x + 4y + 29 >= 4x + 4y + 16 = +(*(k(),x),*(k(),y))
     problem:
      +(x,s(y)) -> s(+(x,y))
      +(s(x),y) -> s(+(x,y))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [+](x0, x1) = 2x0 + x1 + 1,
       
       [s](x0) = x0 + 1
      orientation:
       +(x,s(y)) = 2x + y + 2 >= 2x + y + 2 = s(+(x,y))
       
       +(s(x),y) = 2x + y + 3 >= 2x + y + 2 = s(+(x,y))
      problem:
       +(x,s(y)) -> s(+(x,y))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [+](x0, x1) = x0 + 4x1,
        
        [s](x0) = x0 + 5
       orientation:
        +(x,s(y)) = x + 4y + 20 >= x + 4y + 5 = s(+(x,y))
       problem:
        
       Qed