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: hd(c(x1)) -> x1
   7: hd(++(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: hd(c(x1)) -> x1
   7: hd(++(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: hd(c(x1)) -> x1
   7: hd(++(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))