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