YES 1 decompositions #0 ----------- 1: E(+(x,y)) -> *(E(x),E(y)) 2: E(0()) -> 1() 3: +(x,0()) -> x 4: +(0(),x) -> x 5: *(x,1()) -> x 6: *(1(),x) -> x 7: +(+(x,y),z) -> +(x,+(y,z)) 8: +(x,+(y,z)) -> +(+(x,y),z) 9: +(x,y) -> +(y,x) 10: *(*(x,y),z) -> *(x,*(y,z)) 11: *(x,*(y,z)) -> *(*(x,y),z) 12: *(x,y) -> *(y,x) @Jouannaud and Kirchner's criterion --- R 1: E(+(x,y)) -> *(E(x),E(y)) 2: E(0()) -> 1() 3: +(x,0()) -> x 4: +(0(),x) -> x 5: *(x,1()) -> x 6: *(1(),x) -> x 7: +(+(x,y),z) -> +(x,+(y,z)) 8: +(x,+(y,z)) -> +(+(x,y),z) 9: +(x,y) -> +(y,x) 10: *(*(x,y),z) -> *(x,*(y,z)) 11: *(x,*(y,z)) -> *(*(x,y),z) 12: *(x,y) -> *(y,x) --- S 1: E(+(x,y)) -> *(E(x),E(y)) 2: E(0()) -> 1() 3: +(x,0()) -> x 4: +(0(),x) -> x 5: *(x,1()) -> x 6: *(1(),x) -> x 7: +(+(x,y),z) -> +(x,+(y,z)) 8: +(x,+(y,z)) -> +(+(x,y),z) 9: +(x,y) -> +(y,x) 10: *(*(x,y),z) -> *(x,*(y,z)) 11: *(x,*(y,z)) -> *(*(x,y),z) 12: *(x,y) -> *(y,x)