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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 36
   0() <-0|[]- +(0(),0()) -2|[]-> 0()
   s(x) <-0|[]- +(s(x),0()) -3|[]-> s(+(x,0()))
   +(x,y) <-0|[]- +(+(x,y),0()) -8|[]-> +(x,+(y,0()))
   +(x,z) <-0|0[]- +(+(x,0()),z) -8|[]-> +(x,+(0(),z))
   x <-0|[]- +(x,0()) -9|[]-> +(0(),x)
   s(+(0(),x332)) <-1|[]- +(0(),s(x332)) -2|[]-> s(x332)
   s(+(s(x),x334)) <-1|[]- +(s(x),s(x334)) -3|[]-> s(+(x,s(x334)))
   s(+(+(x,y),x336)) <-1|[]- +(+(x,y),s(x336)) -8|[]-> +(x,+(y,s(x336)))
   +(s(+(x,x338)),z) <-1|0[]- +(+(x,s(x338)),z) -8|[]-> +(x,+(s(x338),z))
   s(+(x,x340)) <-1|[]- +(x,s(x340)) -9|[]-> +(s(x340),x)
   0() <-2|[]- +(0(),0()) -0|[]-> 0()
   s(y) <-2|[]- +(0(),s(y)) -1|[]-> s(+(0(),y))
   +(y,z) <-2|0[]- +(+(0(),y),z) -8|[]-> +(0(),+(y,z))
   y <-2|[]- +(0(),y) -9|[]-> +(y,0())
   s(+(x345,0())) <-3|[]- +(s(x345),0()) -0|[]-> s(x345)
   s(+(x347,s(y))) <-3|[]- +(s(x347),s(y)) -1|[]-> s(+(s(x347),y))
   +(s(+(x349,y)),z) <-3|0[]- +(+(s(x349),y),z) -8|[]-> +(s(x349),+(y,z))
   s(+(x351,y)) <-3|[]- +(s(x351),y) -9|[]-> +(y,s(x351))
   0() <-4|[]- *(0(),0()) -6|[]-> 0()
   0() <-4|[]- *(s(x),0()) -7|[]-> +(*(x,0()),0())
   +(*(0(),x356),0()) <-5|[]- *(0(),s(x356)) -6|[]-> 0()
   +(*(s(x),x358),s(x)) <-5|[]- *(s(x),s(x358)) -7|[]-> +(*(x,s(x358)),s(x358))
   0() <-6|[]- *(0(),0()) -4|[]-> 0()
   0() <-6|[]- *(0(),s(y)) -5|[]-> +(*(0(),y),0())
   +(*(x361,0()),0()) <-7|[]- *(s(x361),0()) -4|[]-> 0()
   +(*(x363,s(y)),s(y)) <-7|[]- *(s(x363),s(y)) -5|[]-> +(*(s(x363),y),s(x363))
   +(x365,+(x366,0())) <-8|[]- +(+(x365,x366),0()) -0|[]-> +(x365,x366)
   +(x368,+(x369,s(y))) <-8|[]- +(+(x368,x369),s(y)) -1|[]-> s(+(+(x368,x369),y))
   +(+(x371,+(x372,y)),z) <-8|0[]- +(+(+(x371,x372),y),z) -8|[]-> +(+(x371,x372),+(y,z))
   +(x374,+(x375,y)) <-8|[]- +(+(x374,x375),y) -9|[]-> +(y,+(x374,x375))
   +(0(),x) <-9|[]- +(x,0()) -0|[]-> x
   +(s(y),x) <-9|[]- +(x,s(y)) -1|[]-> s(+(x,y))
   +(y,0()) <-9|[]- +(0(),y) -2|[]-> y
   +(y,s(x)) <-9|[]- +(s(x),y) -3|[]-> s(+(x,y))
   +(z,+(x,y)) <-9|[]- +(+(x,y),z) -8|[]-> +(x,+(y,z))
   +(+(y,x),z) <-9|0[]- +(+(x,y),z) -8|[]-> +(x,+(y,z))
  Redundant Rules Transformation:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   *(x,0()) -> 0()
   *(x,s(y)) -> +(*(x,y),x)
   *(0(),y) -> 0()
   *(s(x),y) -> +(*(x,y),y)
   +(+(x,y),z) -> +(x,+(y,z))
   +(x,y) -> +(y,x)
   Church Rosser Transformation Processor (ac):
    f5_AC(0(),y) -> y
    f5_AC(s(x),y) -> s(f5_AC(x,y))
    *(x,0()) -> 0()
    *(x,s(y)) -> f5_AC(*(x,y),x)
    *(0(),y) -> 0()
    *(s(x),y) -> f5_AC(*(x,y),y)
    AC critical peaks: joinable
    AC-RPO Processor:
     precedence:
      * > 0 > f5_AC > s
     status:
      *:mul  
     problem:
      
     Qed