YES 1 decompositions #1 ----------- 1: +(x1,0()) -> x1 2: +(x1,s(x2)) -> s(+(x1,x2)) 3: *(x1,0()) -> 0() 4: *(x1,s(x2)) -> +(*(x1,x2),x1) 5: +(+(x1,x2),x3) -> +(x1,+(x2,x3)) 6: +(x1,x2) -> +(x2,x1) 7: *(*(x1,x2),x3) -> *(x1,*(x2,x3)) 8: *(x1,x2) -> *(x2,x1) 9: *(x1,+(x2,x3)) -> +(*(x1,x2),*(x1,x3)) @Jouannaud and Kirchner's criterion --- R 1: +(x1,0()) -> x1 2: +(x1,s(x2)) -> s(+(x1,x2)) 3: *(x1,0()) -> 0() 4: *(x1,s(x2)) -> +(*(x1,x2),x1) 5: +(+(x1,x2),x3) -> +(x1,+(x2,x3)) 6: +(x1,x2) -> +(x2,x1) 7: *(*(x1,x2),x3) -> *(x1,*(x2,x3)) 8: *(x1,x2) -> *(x2,x1) 9: *(x1,+(x2,x3)) -> +(*(x1,x2),*(x1,x3)) --- S 1: +(x1,0()) -> x1 2: +(x1,s(x2)) -> s(+(x1,x2)) 3: *(x1,0()) -> 0() 4: *(x1,s(x2)) -> +(*(x1,x2),x1) 5: +(+(x1,x2),x3) -> +(x1,+(x2,x3)) 6: +(x1,x2) -> +(x2,x1) 7: *(*(x1,x2),x3) -> *(x1,*(x2,x3)) 8: *(x1,x2) -> *(x2,x1) 9: *(x1,+(x2,x3)) -> +(*(x1,x2),*(x1,x3))