YES
Time: 0.001445
TRS:
 { sum 0() -> 0(),
   sum s x -> +(sum x, s x),
  sum1 0() -> 0(),
  sum1 s x -> s +(sum1 x, +(x, x))}
 DP:
  DP:
   { sum# s x -> sum# x,
    sum1# s x -> sum1# x}
  TRS:
  { 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 (2):
    Scc:
     {sum1# s x -> sum1# x}
    Scc:
     {sum# s x -> sum# x}
    SCC (1):
     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 (1):
     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