YES

1 decompositions
 #1 -----------
   1: e(x1) -> ++(x1,e(+(x1,x1)))
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))
   3: ++(x1,++(x2,x3)) -> ++(++(x1,x2),x3)
   4: ++(0(),x1) -> x1
   5: +(x1,x2) -> +(x2,x1)
   6: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   7: +(0(),x1) -> x1
   8: +(s(x1),x2) -> s(+(x1,x2))

@Commutation Lemma

@Development Closedness
--- R
   1: e(x1) -> ++(x1,e(+(x1,x1)))

--- S
   1: e(x1) -> ++(x1,e(+(x1,x1)))
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))
   3: ++(x1,++(x2,x3)) -> ++(++(x1,x2),x3)
   4: ++(0(),x1) -> x1
   5: +(x1,x2) -> +(x2,x1)
   6: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   7: +(0(),x1) -> x1
   8: +(s(x1),x2) -> s(+(x1,x2))

@Commutation Lemma

@Development Closedness
--- R
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))
   3: ++(x1,++(x2,x3)) -> ++(++(x1,x2),x3)
   4: ++(0(),x1) -> x1
   5: +(x1,x2) -> +(x2,x1)
   6: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   7: +(0(),x1) -> x1
   8: +(s(x1),x2) -> s(+(x1,x2))

--- S
   1: e(x1) -> ++(x1,e(+(x1,x1)))

@Commutation Lemma

@Rule Labeling
--- R
   3: ++(x1,++(x2,x3)) -> ++(++(x1,x2),x3)

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

@Commutation Lemma

@Commutation Lemma

@Jouannaud and Kirchner's criterion
--- R
   4: ++(0(),x1) -> x1

--- S
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))

@Commutation Lemma

@Jouannaud and Kirchner's criterion
--- R
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))

--- S
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))

@Development Closedness
--- R
   5: +(x1,x2) -> +(x2,x1)
   6: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   7: +(0(),x1) -> x1
   8: +(s(x1),x2) -> s(+(x1,x2))

--- S
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))

@Commutation Lemma

@Rule Labeling
--- R
   2: ++(++(x1,x2),x3) -> ++(x1,++(x2,x3))
   4: ++(0(),x1) -> x1
   5: +(x1,x2) -> +(x2,x1)
   6: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   7: +(0(),x1) -> x1
   8: +(s(x1),x2) -> s(+(x1,x2))

--- S
   3: ++(x1,++(x2,x3)) -> ++(++(x1,x2),x3)

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

--- S
   4: ++(0(),x1) -> x1
   5: +(x1,x2) -> +(x2,x1)
   6: +(+(x1,x2),x3) -> +(x1,+(x2,x3))
   7: +(0(),x1) -> x1
   8: +(s(x1),x2) -> s(+(x1,x2))