Problem:
 *(e(),x) -> x
 *(i(x),x) -> e()
 i(e()) -> e()
 i(i(x)) -> x
 i(*(x,y)) -> *(i(x),i(y))
 f(*(x,y)) -> *(f(x),f(y))
 f(e()) -> e()
 f(i(x)) -> i(f(x))
 *(*(x,y),z) -> *(x,*(y,z))
 *(x,*(y,z)) -> *(*(x,y),z)
 *(x,y) -> *(y,x)

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 43
   i(y) <-0|0[]- i(*(e(),y)) -4|[]-> *(i(e()),i(y))
   f(y) <-0|0[]- f(*(e(),y)) -5|[]-> *(f(e()),f(y))
   *(y,z) <-0|0[]- *(*(e(),y),z) -8|[]-> *(e(),*(y,z))
   *(y,z) <-0|[]- *(e(),*(y,z)) -9|[]-> *(*(e(),y),z)
   *(x,z) <-0|1[]- *(x,*(e(),z)) -9|[]-> *(*(x,e()),z)
   y <-0|[]- *(e(),y) -10|[]-> *(y,e())
   i(e()) <-1|0[]- i(*(i(y),y)) -4|[]-> *(i(i(y)),i(y))
   f(e()) <-1|0[]- f(*(i(y),y)) -5|[]-> *(f(i(y)),f(y))
   *(e(),z) <-1|0[]- *(*(i(y),y),z) -8|[]-> *(i(y),*(y,z))
   e() <-1|[]- *(i(*(y,z)),*(y,z)) -9|[]-> *(*(i(*(y,z)),y),z)
   *(x,e()) <-1|1[]- *(x,*(i(z),z)) -9|[]-> *(*(x,i(z)),z)
   e() <-1|[]- *(i(y),y) -10|[]-> *(y,i(y))
   *(e(),e()) <-2|0[]- *(i(e()),e()) -1|[]-> e()
   i(e()) <-2|0[]- i(i(e())) -3|[]-> e()
   f(e()) <-2|0[]- f(i(e())) -7|[]-> i(f(e()))
   *(x351,i(x351)) <-3|0[]- *(i(i(x351)),i(x351)) -1|[]-> e()
   i(x352) <-3|0[]- i(i(i(x352))) -3|[]-> i(x352)
   f(x353) <-3|0[]- f(i(i(x353))) -7|[]-> i(f(i(x353)))
   *(*(i(x354),i(x355)),*(x354,x355)) <-4|0[]- *(i(*(x354,x355)),*(x354,x355)) -1|[]-> e()
   i(*(i(x356),i(x357))) <-4|0[]- i(i(*(x356,x357))) -3|[]-> *(x356,x357)
   f(*(i(x358),i(x359))) <-4|0[]- f(i(*(x358,x359))) -7|[]-> i(f(*(x358,x359)))
   i(*(x360,*(x361,y))) <-8|0[]- i(*(*(x360,x361),y)) -4|[]-> *(i(*(x360,x361)),i(y))
   f(*(x363,*(x364,y))) <-8|0[]- f(*(*(x363,x364),y)) -5|[]-> *(f(*(x363,x364)),f(y))
   *(*(x366,*(x367,y)),z) <-8|0[]- *(*(*(x366,x367),y),z) -8|[]-> *(*(x366,x367),*(y,z))
   *(x369,*(x370,*(y,z))) <-8|[]- *(*(x369,x370),*(y,z)) -9|[]-> *(*(*(x369,x370),y),z)
   *(x,*(x372,*(x373,z))) <-8|1[]- *(x,*(*(x372,x373),z)) -9|[]-> *(*(x,*(x372,x373)),z)
   *(x375,*(x376,y)) <-8|[]- *(*(x375,x376),y) -10|[]-> *(y,*(x375,x376))
   *(*(e(),x379),x380) <-9|[]- *(e(),*(x379,x380)) -0|[]-> *(x379,x380)
   *(*(i(*(x382,x383)),x382),x383) <-9|[]- *(i(*(x382,x383)),*(x382,x383)) -1|[]-> e()
   i(*(*(x,x385),x386)) <-9|0[]- i(*(x,*(x385,x386))) -4|[]-> *(i(x),i(*(x385,x386)))
   f(*(*(x,x388),x389)) <-9|0[]- f(*(x,*(x388,x389))) -5|[]-> *(f(x),f(*(x388,x389)))
   *(*(*(x,y),x391),x392) <-9|[]- *(*(x,y),*(x391,x392)) -8|[]-> *(x,*(y,*(x391,x392)))
   *(*(*(x,x394),x395),z) <-9|0[]- *(*(x,*(x394,x395)),z) -8|[]-> *(x,*(*(x394,x395),z))
   *(x,*(*(y,x397),x398)) <-9|1[]- *(x,*(y,*(x397,x398))) -9|[]-> *(*(x,y),*(x397,x398))
   *(*(x,x400),x401) <-9|[]- *(x,*(x400,x401)) -10|[]-> *(*(x400,x401),x)
   *(x,e()) <-10|[]- *(e(),x) -0|[]-> x
   *(x,i(x)) <-10|[]- *(i(x),x) -1|[]-> e()
   i(*(y,x)) <-10|0[]- i(*(x,y)) -4|[]-> *(i(x),i(y))
   f(*(y,x)) <-10|0[]- f(*(x,y)) -5|[]-> *(f(x),f(y))
   *(z,*(x,y)) <-10|[]- *(*(x,y),z) -8|[]-> *(x,*(y,z))
   *(*(y,x),z) <-10|0[]- *(*(x,y),z) -8|[]-> *(x,*(y,z))
   *(*(y,z),x) <-10|[]- *(x,*(y,z)) -9|[]-> *(*(x,y),z)
   *(x,*(z,y)) <-10|1[]- *(x,*(y,z)) -9|[]-> *(*(x,y),z)
  Redundant Rules Transformation:
   *(e(),x) -> x
   *(i(x),x) -> e()
   i(e()) -> e()
   i(i(x)) -> x
   i(*(x,y)) -> *(i(x),i(y))
   f(*(x,y)) -> *(f(x),f(y))
   f(e()) -> e()
   f(i(x)) -> i(f(x))
   *(x,*(y,z)) -> *(*(x,y),z)
   *(x,y) -> *(y,x)
   Church Rosser Transformation Processor (ac):
    f5_AC(e(),x) -> x
    f5_AC(i(x),x) -> e()
    i(e()) -> e()
    i(i(x)) -> x
    i(f5_AC(x,y)) -> f5_AC(i(x),i(y))
    f(f5_AC(x,y)) -> f5_AC(f(x),f(y))
    f(e()) -> e()
    f(i(x)) -> i(f(x))
    AC critical peaks: joinable
    AC-RPO Processor:
     precedence:
      f > i > e > f5_AC
     status:
      
     problem:
      
     Qed