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