YES
TRS:
 {  sum(0()) -> 0(),
   sum(s(x)) -> +(sum(x), s(x)),
   sum1(0()) -> 0(),
  sum1(s(x)) -> s(+(sum1(x), +(x, x)))}
 DP:
  Strict:
   { sum#(s(x)) -> sum#(x),
    sum1#(s(x)) -> sum1#(x)}
  Weak:
  {  sum(0()) -> 0(),
    sum(s(x)) -> +(sum(x), s(x)),
    sum1(0()) -> 0(),
   sum1(s(x)) -> s(+(sum1(x), +(x, x)))}
  EDG:
   {(sum1#(s(x)) -> sum1#(x), sum1#(s(x)) -> sum1#(x))
    (sum#(s(x)) -> sum#(x), sum#(s(x)) -> sum#(x))}
   SCCS:
    Scc:
     {sum1#(s(x)) -> sum1#(x)}
    Scc:
     {sum#(s(x)) -> sum#(x)}
    SCC:
     Strict:
      {sum1#(s(x)) -> sum1#(x)}
     Weak:
     {  sum(0()) -> 0(),
       sum(s(x)) -> +(sum(x), s(x)),
       sum1(0()) -> 0(),
      sum1(s(x)) -> s(+(sum1(x), +(x, x)))}
     SPSC:
      Simple Projection:
       pi(sum1#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {sum#(s(x)) -> sum#(x)}
     Weak:
     {  sum(0()) -> 0(),
       sum(s(x)) -> +(sum(x), s(x)),
       sum1(0()) -> 0(),
      sum1(s(x)) -> s(+(sum1(x), +(x, x)))}
     SPSC:
      Simple Projection:
       pi(sum#) = 0
      Strict:
       {}
      Qed