YES

3 decompositions
 #1 -----------
   1: from(x1) -> :(x1,from(s(x1)))

 #2 -----------
   2: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   3: +(x1,+(x2,x3)) -> +(+(x1,x2),x3)
   4: +(0(),x1) -> x1
   5: +(x1,0()) -> x1
   6: f(c(x1)) -> x1
   7: f(+(c(x1),x2)) -> x1

 #3 -----------
   2: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   3: +(x1,+(x2,x3)) -> +(+(x1,x2),x3)
   4: +(0(),x1) -> x1
   5: +(x1,0()) -> x1
   8: *(0(),x2) -> 0()
   9: *(s(x1),x2) -> +(x2,*(x1,x2))

@Development Closedness
--- R
   1: from(x1) -> :(x1,from(s(x1)))

--- S
   1: from(x1) -> :(x1,from(s(x1)))


@Jouannaud and Kirchner's criterion
--- R
   2: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   3: +(x1,+(x2,x3)) -> +(+(x1,x2),x3)
   4: +(0(),x1) -> x1
   5: +(x1,0()) -> x1
   6: f(c(x1)) -> x1
   7: f(+(c(x1),x2)) -> x1

--- S
   2: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   3: +(x1,+(x2,x3)) -> +(+(x1,x2),x3)
   4: +(0(),x1) -> x1
   5: +(x1,0()) -> x1
   6: f(c(x1)) -> x1
   7: f(+(c(x1),x2)) -> x1


@Jouannaud and Kirchner's criterion
--- R
   2: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   3: +(x1,+(x2,x3)) -> +(+(x1,x2),x3)
   4: +(0(),x1) -> x1
   5: +(x1,0()) -> x1
   8: *(0(),x2) -> 0()
   9: *(s(x1),x2) -> +(x2,*(x1,x2))

--- S
   2: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   3: +(x1,+(x2,x3)) -> +(+(x1,x2),x3)
   4: +(0(),x1) -> x1
   5: +(x1,0()) -> x1
   8: *(0(),x2) -> 0()
   9: *(s(x1),x2) -> +(x2,*(x1,x2))