YES

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

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

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


NOTE: input TRS is reduced

original is
   1: +(0(),x1) -> x1
   2: +(x2,0()) -> x2
   3: +(s(x2),x1) -> s(+(x2,x1))
   4: +(x2,s(x1)) -> +(s(x1),x2)
   5: +(x2,+(x1,x3)) -> +(+(x2,x1),x3)
   6: +(x2,x1) -> +(x1,x2)
   7: dbl(x2) -> +(x2,x2)

reduced to
   2: +(x2,0()) -> x2
   3: +(s(x2),x1) -> s(+(x2,x1))
   5: +(x2,+(x1,x3)) -> +(+(x2,x1),x3)
   6: +(x2,x1) -> +(x1,x2)
   7: dbl(x2) -> +(x2,x2)