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)
 *(*(x,y),z) -> *(x,*(y,z))
 *(x,y) -> *(y,x)
 *(x,+(y,z)) -> +(*(x,y),*(x,z))
 *(+(x,y),z) -> +(*(x,z),*(y,z))

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 86
   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)
   *(x,y) <-0|1[]- *(x,+(y,0())) -12|[]-> +(*(x,y),*(x,0()))
   *(x,z) <-0|0[]- *(+(x,0()),z) -13|[]-> +(*(x,z),*(0(),z))
   s(+(0(),x739)) <-1|[]- +(0(),s(x739)) -2|[]-> s(x739)
   s(+(s(x),x741)) <-1|[]- +(s(x),s(x741)) -3|[]-> s(+(x,s(x741)))
   s(+(+(x,y),x743)) <-1|[]- +(+(x,y),s(x743)) -8|[]-> +(x,+(y,s(x743)))
   +(s(+(x,x745)),z) <-1|0[]- +(+(x,s(x745)),z) -8|[]-> +(x,+(s(x745),z))
   s(+(x,x747)) <-1|[]- +(x,s(x747)) -9|[]-> +(s(x747),x)
   *(x,s(+(y,x749))) <-1|1[]- *(x,+(y,s(x749))) -12|[]-> +(*(x,y),*(x,s(x749)))
   *(s(+(x,x751)),z) <-1|0[]- *(+(x,s(x751)),z) -13|[]-> +(*(x,z),*(s(x751),z))
   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())
   *(x,z) <-2|1[]- *(x,+(0(),z)) -12|[]-> +(*(x,0()),*(x,z))
   *(y,z) <-2|0[]- *(+(0(),y),z) -13|[]-> +(*(0(),z),*(y,z))
   s(+(x758,0())) <-3|[]- +(s(x758),0()) -0|[]-> s(x758)
   s(+(x760,s(y))) <-3|[]- +(s(x760),s(y)) -1|[]-> s(+(s(x760),y))
   +(s(+(x762,y)),z) <-3|0[]- +(+(s(x762),y),z) -8|[]-> +(s(x762),+(y,z))
   s(+(x764,y)) <-3|[]- +(s(x764),y) -9|[]-> +(y,s(x764))
   *(x,s(+(x766,z))) <-3|1[]- *(x,+(s(x766),z)) -12|[]-> +(*(x,s(x766)),*(x,z))
   *(s(+(x768,y)),z) <-3|0[]- *(+(s(x768),y),z) -13|[]-> +(*(s(x768),z),*(y,z))
   0() <-4|[]- *(0(),0()) -6|[]-> 0()
   0() <-4|[]- *(s(x),0()) -7|[]-> +(*(x,0()),0())
   0() <-4|[]- *(*(x,y),0()) -10|[]-> *(x,*(y,0()))
   *(0(),z) <-4|0[]- *(*(x,0()),z) -10|[]-> *(x,*(0(),z))
   0() <-4|[]- *(x,0()) -11|[]-> *(0(),x)
   0() <-4|[]- *(+(x,y),0()) -13|[]-> +(*(x,0()),*(y,0()))
   +(*(0(),x777),0()) <-5|[]- *(0(),s(x777)) -6|[]-> 0()
   +(*(s(x),x779),s(x)) <-5|[]- *(s(x),s(x779)) -7|[]-> +(*(x,s(x779)),s(x779))
   +(*(*(x,y),x781),*(x,y)) <-5|[]- *(*(x,y),s(x781)) -10|[]-> *(x,*(y,s(x781)))
   *(+(*(x,x783),x),z) <-5|0[]- *(*(x,s(x783)),z) -10|[]-> *(x,*(s(x783),z))
   +(*(x,x785),x) <-5|[]- *(x,s(x785)) -11|[]-> *(s(x785),x)
   +(*(+(x,y),x787),+(x,y)) <-5|[]- *(+(x,y),s(x787)) -13|[]-> +(*(x,s(x787)),*(y,s(x787)))
   0() <-6|[]- *(0(),0()) -4|[]-> 0()
   0() <-6|[]- *(0(),s(y)) -5|[]-> +(*(0(),y),0())
   *(0(),z) <-6|0[]- *(*(0(),y),z) -10|[]-> *(0(),*(y,z))
   0() <-6|[]- *(0(),y) -11|[]-> *(y,0())
   0() <-6|[]- *(0(),+(y,z)) -12|[]-> +(*(0(),y),*(0(),z))
   +(*(x793,0()),0()) <-7|[]- *(s(x793),0()) -4|[]-> 0()
   +(*(x795,s(y)),s(y)) <-7|[]- *(s(x795),s(y)) -5|[]-> +(*(s(x795),y),s(x795))
   *(+(*(x797,y),y),z) <-7|0[]- *(*(s(x797),y),z) -10|[]-> *(s(x797),*(y,z))
   +(*(x799,y),y) <-7|[]- *(s(x799),y) -11|[]-> *(y,s(x799))
   +(*(x801,+(y,z)),+(y,z)) <-7|[]- *(s(x801),+(y,z)) -12|[]-> +(*(s(x801),y),*(s(x801),z))
   +(x803,+(x804,0())) <-8|[]- +(+(x803,x804),0()) -0|[]-> +(x803,x804)
   +(x806,+(x807,s(y))) <-8|[]- +(+(x806,x807),s(y)) -1|[]-> s(+(+(x806,x807),y))
   +(+(x809,+(x810,y)),z) <-8|0[]- +(+(+(x809,x810),y),z) -8|[]-> +(+(x809,x810),+(y,z))
   +(x812,+(x813,y)) <-8|[]- +(+(x812,x813),y) -9|[]-> +(y,+(x812,x813))
   *(x,+(x815,+(x816,z))) <-8|1[]- *(x,+(+(x815,x816),z)) -12|[]-> +(*(x,+(x815,x816)),*(x,z))
   *(+(x818,+(x819,y)),z) <-8|0[]- *(+(+(x818,x819),y),z) -13|[]-> +(*(+(x818,x819),z),*(y,z))
   +(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))
   *(x,+(z,y)) <-9|1[]- *(x,+(y,z)) -12|[]-> +(*(x,y),*(x,z))
   *(+(y,x),z) <-9|0[]- *(+(x,y),z) -13|[]-> +(*(x,z),*(y,z))
   *(x837,*(x838,0())) <-10|[]- *(*(x837,x838),0()) -4|[]-> 0()
   *(x840,*(x841,s(y))) <-10|[]- *(*(x840,x841),s(y)) -5|[]-> +(*(*(x840,x841),y),*(x840,x841))
   *(*(x843,*(x844,y)),z) <-10|0[]- *(*(*(x843,x844),y),z) -10|[]-> *(*(x843,x844),*(y,z))
   *(x846,*(x847,y)) <-10|[]- *(*(x846,x847),y) -11|[]-> *(y,*(x846,x847))
   *(x849,*(x850,+(y,z))) <-10|[]- *(*(x849,x850),+(y,z)) -12|[]-> +(
                                                                    *(*(x849,x850),y),
                                                                    *
                                                                    (*(x849,x850),z))
   *(0(),x) <-11|[]- *(x,0()) -4|[]-> 0()
   *(s(y),x) <-11|[]- *(x,s(y)) -5|[]-> +(*(x,y),x)
   *(y,0()) <-11|[]- *(0(),y) -6|[]-> 0()
   *(y,s(x)) <-11|[]- *(s(x),y) -7|[]-> +(*(x,y),y)
   *(z,*(x,y)) <-11|[]- *(*(x,y),z) -10|[]-> *(x,*(y,z))
   *(*(y,x),z) <-11|0[]- *(*(x,y),z) -10|[]-> *(x,*(y,z))
   *(+(y,z),x) <-11|[]- *(x,+(y,z)) -12|[]-> +(*(x,y),*(x,z))
   *(z,+(x,y)) <-11|[]- *(+(x,y),z) -13|[]-> +(*(x,z),*(y,z))
   +(*(0(),x869),*(0(),x870)) <-12|[]- *(0(),+(x869,x870)) -6|[]-> 0()
   +(*(s(x),x872),*(s(x),x873)) <-12|[]- *(s(x),+(x872,x873)) -7|[]-> 
                                         +(*(x,+(x872,x873)),+(x872,x873))
   +(*(*(x,y),x875),*(*(x,y),x876)) <-12|[]- *(*(x,y),+(x875,x876)) -10|[]-> *(x,*(y,+(x875,x876)))
   *(+(*(x,x878),*(x,x879)),z) <-12|0[]- *(*(x,+(x878,x879)),z) -10|[]-> *(x,*(+(x878,x879),z))
   +(*(x,x881),*(x,x882)) <-12|[]- *(x,+(x881,x882)) -11|[]-> *(+(x881,x882),x)
   +(*(+(x,y),x884),*(+(x,y),x885)) <-12|[]- *(+(x,y),+(x884,x885)) -13|
                                             []-> +(*(x,+(x884,x885)),*(y,+(x884,x885)))
   +(*(x886,0()),*(x887,0())) <-13|[]- *(+(x886,x887),0()) -4|[]-> 0()
   +(*(x889,s(y)),*(x890,s(y))) <-13|[]- *(+(x889,x890),s(y)) -5|[]-> 
                                         +(*(+(x889,x890),y),+(x889,x890))
   *(+(*(x892,y),*(x893,y)),z) <-13|0[]- *(*(+(x892,x893),y),z) -10|[]-> *(+(x892,x893),*(y,z))
   +(*(x895,y),*(x896,y)) <-13|[]- *(+(x895,x896),y) -11|[]-> *(y,+(x895,x896))
   +(*(x898,+(y,z)),*(x899,+(y,z))) <-13|[]- *(+(x898,x899),+(y,z)) -12|
                                             []-> +(*(+(x898,x899),y),*(+(x898,x899),z))
  Redundant Rules Transformation:
   +(0(),y) -> y
   +(s(x),y) -> s(+(x,y))
   *(0(),y) -> 0()
   *(s(x),y) -> +(*(x,y),y)
   +(+(x,y),z) -> +(x,+(y,z))
   +(x,y) -> +(y,x)
   *(*(x,y),z) -> *(x,*(y,z))
   *(x,y) -> *(y,x)
   *(+(x,y),z) -> +(*(x,z),*(y,z))
   Church Rosser Transformation Processor (ac):
    f5_AC(0(),y) -> y
    f5_AC(s(x),y) -> s(f5_AC(x,y))
    f7_AC(0(),y) -> 0()
    f7_AC(s(x),y) -> f5_AC(f7_AC(x,y),y)
    f7_AC(f5_AC(x,y),z) -> f5_AC(f7_AC(x,z),f7_AC(y,z))
    AC critical peaks: joinable
    AC-RPO Processor:
     precedence:
      f7_AC > 0 > f5_AC > s
     status:
      
     problem:
      
     Qed