YES
TRS:
 {           +(x, 0()) -> x,
         +(+(x, y), z) -> +(x, +(y, z)),
             +(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))),
         *(*(x, y), z) -> *(x, *(y, z)),
         app(nil(), l) -> l,
  app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
      sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
            sum(nil()) -> 0(),
       sum(cons(x, l)) -> +(x, sum(l)),
     prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
           prod(nil()) -> s(0()),
      prod(cons(x, l)) -> *(x, prod(l))}
 DP:
  Strict:
   {       +#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z),
           +#(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),
           *#(*(x, y), z) -> *#(x, *(y, z)),
           *#(*(x, y), z) -> *#(y, z),
    app#(cons(x, l1), l2) -> app#(l1, l2),
        sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)),
        sum#(app(l1, l2)) -> sum#(l1),
        sum#(app(l1, l2)) -> sum#(l2),
         sum#(cons(x, l)) -> +#(x, sum(l)),
         sum#(cons(x, l)) -> sum#(l),
       prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)),
       prod#(app(l1, l2)) -> prod#(l1),
       prod#(app(l1, l2)) -> prod#(l2),
        prod#(cons(x, l)) -> *#(x, prod(l)),
        prod#(cons(x, l)) -> prod#(l)}
  Weak:
  {           +(x, 0()) -> x,
          +(+(x, y), z) -> +(x, +(y, z)),
              +(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))),
          *(*(x, y), z) -> *(x, *(y, z)),
          app(nil(), l) -> l,
   app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
       sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
             sum(nil()) -> 0(),
        sum(cons(x, l)) -> +(x, sum(l)),
      prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
            prod(nil()) -> s(0()),
       prod(cons(x, l)) -> *(x, prod(l))}
  EDG:
   {(*#(s(x), s(y)) -> +#(x, y), +#(s(x), s(y)) -> +#(x, y))
    (*#(s(x), s(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (*#(s(x), s(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(s(x), s(y)) -> +#(x, y))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(+(x, y), z) -> +#(y, z))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(*(x, y), z) -> *#(y, z))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (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))
    (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)))
    (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> sum#(l2))
    (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> sum#(l1))
    (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)))
    (prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l))
    (prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> *#(x, prod(l)))
    (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> prod#(l2))
    (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> prod#(l1))
    (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)))
    (*#(s(x), s(y)) -> +#(*(x, y), +(x, y)), +#(s(x), s(y)) -> +#(x, y))
    (*#(s(x), s(y)) -> +#(*(x, y), +(x, y)), +#(+(x, y), z) -> +#(y, z))
    (*#(s(x), s(y)) -> +#(*(x, y), +(x, y)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(y, z), +#(s(x), s(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> +#(x, sum(l)))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l2))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l1))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l1))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l2))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> *#(x, prod(l)))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> prod#(l))
    (*#(*(x, y), z) -> *#(y, z), *#(s(x), s(y)) -> +#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(s(x), s(y)) -> +#(*(x, y), +(x, y)))
    (*#(*(x, y), z) -> *#(y, z), *#(s(x), s(y)) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s(x), s(y)) -> +#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s(x), s(y)) -> +#(*(x, y), +(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(s(x), s(y)) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s(x), s(y)) -> +#(x, y))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> prod#(l1))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> prod#(l2))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> *#(x, prod(l)))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l))
    (sum#(app(l1, l2)) -> sum#(l2), sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)))
    (sum#(app(l1, l2)) -> sum#(l2), sum#(app(l1, l2)) -> sum#(l1))
    (sum#(app(l1, l2)) -> sum#(l2), sum#(app(l1, l2)) -> sum#(l2))
    (sum#(app(l1, l2)) -> sum#(l2), sum#(cons(x, l)) -> +#(x, sum(l)))
    (sum#(app(l1, l2)) -> sum#(l2), sum#(cons(x, l)) -> sum#(l))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(s(x), s(y)) -> +#(x, y))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(s(x), s(y)) -> +#(*(x, y), +(x, y)))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(s(x), s(y)) -> *#(x, y))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(*(x, y), z) -> *#(x, *(y, z)))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(*(x, y), z) -> *#(y, z))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(+(x, y), z) -> +#(y, z))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(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), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(s(x), s(y)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (+#(s(x), s(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(s(x), s(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(s(x), s(y)) -> +#(x, y), +#(s(x), s(y)) -> +#(x, y))}
   SCCS:
    Scc:
     {prod#(app(l1, l2)) -> prod#(l1),
      prod#(app(l1, l2)) -> prod#(l2),
       prod#(cons(x, l)) -> prod#(l)}
    Scc:
     {sum#(app(l1, l2)) -> sum#(l1),
      sum#(app(l1, l2)) -> sum#(l2),
       sum#(cons(x, l)) -> sum#(l)}
    Scc:
     {app#(cons(x, l1), l2) -> app#(l1, l2)}
    Scc:
     {*#(s(x), s(y)) -> *#(x, y),
      *#(*(x, y), z) -> *#(x, *(y, z)),
      *#(*(x, y), z) -> *#(y, z)}
    Scc:
     {+#(+(x, y), z) -> +#(x, +(y, z)),
      +#(+(x, y), z) -> +#(y, z),
      +#(s(x), s(y)) -> +#(x, y)}
    SCC:
     Strict:
      {prod#(app(l1, l2)) -> prod#(l1),
       prod#(app(l1, l2)) -> prod#(l2),
        prod#(cons(x, l)) -> prod#(l)}
     Weak:
     {           +(x, 0()) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
                 +(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))),
             *(*(x, y), z) -> *(x, *(y, z)),
             app(nil(), l) -> l,
      app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
          sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                sum(nil()) -> 0(),
           sum(cons(x, l)) -> +(x, sum(l)),
         prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
               prod(nil()) -> s(0()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(prod#) = 0
      Strict:
       {prod#(app(l1, l2)) -> prod#(l1),
         prod#(cons(x, l)) -> prod#(l)}
      EDG:
       {(prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l))
        (prod#(cons(x, l)) -> prod#(l), prod#(app(l1, l2)) -> prod#(l1))
        (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> prod#(l1))
        (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> prod#(l))}
       SCCS:
        Scc:
         {prod#(app(l1, l2)) -> prod#(l1),
           prod#(cons(x, l)) -> prod#(l)}
        SCC:
         Strict:
          {prod#(app(l1, l2)) -> prod#(l1),
            prod#(cons(x, l)) -> prod#(l)}
         Weak:
         {           +(x, 0()) -> x,
                 +(+(x, y), z) -> +(x, +(y, z)),
                     +(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))),
                 *(*(x, y), z) -> *(x, *(y, z)),
                 app(nil(), l) -> l,
          app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                    sum(nil()) -> 0(),
               sum(cons(x, l)) -> +(x, sum(l)),
             prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                   prod(nil()) -> s(0()),
              prod(cons(x, l)) -> *(x, prod(l))}
         SPSC:
          Simple Projection:
           pi(prod#) = 0
          Strict:
           {prod#(cons(x, l)) -> prod#(l)}
          EDG:
           {(prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l))}
           SCCS:
            Scc:
             {prod#(cons(x, l)) -> prod#(l)}
            SCC:
             Strict:
              {prod#(cons(x, l)) -> prod#(l)}
             Weak:
             {           +(x, 0()) -> x,
                     +(+(x, y), z) -> +(x, +(y, z)),
                         +(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))),
                     *(*(x, y), z) -> *(x, *(y, z)),
                     app(nil(), l) -> l,
              app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
                  sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                        sum(nil()) -> 0(),
                   sum(cons(x, l)) -> +(x, sum(l)),
                 prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                       prod(nil()) -> s(0()),
                  prod(cons(x, l)) -> *(x, prod(l))}
             SPSC:
              Simple Projection:
               pi(prod#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {sum#(app(l1, l2)) -> sum#(l1),
       sum#(app(l1, l2)) -> sum#(l2),
        sum#(cons(x, l)) -> sum#(l)}
     Weak:
     {           +(x, 0()) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
                 +(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))),
             *(*(x, y), z) -> *(x, *(y, z)),
             app(nil(), l) -> l,
      app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
          sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                sum(nil()) -> 0(),
           sum(cons(x, l)) -> +(x, sum(l)),
         prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
               prod(nil()) -> s(0()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(sum#) = 0
      Strict:
       {sum#(app(l1, l2)) -> sum#(l1),
         sum#(cons(x, l)) -> sum#(l)}
      EDG:
       {(sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> sum#(l))
        (sum#(cons(x, l)) -> sum#(l), sum#(app(l1, l2)) -> sum#(l1))
        (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> sum#(l1))
        (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l))}
       SCCS:
        Scc:
         {sum#(app(l1, l2)) -> sum#(l1),
           sum#(cons(x, l)) -> sum#(l)}
        SCC:
         Strict:
          {sum#(app(l1, l2)) -> sum#(l1),
            sum#(cons(x, l)) -> sum#(l)}
         Weak:
         {           +(x, 0()) -> x,
                 +(+(x, y), z) -> +(x, +(y, z)),
                     +(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))),
                 *(*(x, y), z) -> *(x, *(y, z)),
                 app(nil(), l) -> l,
          app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                    sum(nil()) -> 0(),
               sum(cons(x, l)) -> +(x, sum(l)),
             prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                   prod(nil()) -> s(0()),
              prod(cons(x, l)) -> *(x, prod(l))}
         SPSC:
          Simple Projection:
           pi(sum#) = 0
          Strict:
           {sum#(cons(x, l)) -> sum#(l)}
          EDG:
           {(sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> sum#(l))}
           SCCS:
            Scc:
             {sum#(cons(x, l)) -> sum#(l)}
            SCC:
             Strict:
              {sum#(cons(x, l)) -> sum#(l)}
             Weak:
             {           +(x, 0()) -> x,
                     +(+(x, y), z) -> +(x, +(y, z)),
                         +(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))),
                     *(*(x, y), z) -> *(x, *(y, z)),
                     app(nil(), l) -> l,
              app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
                  sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                        sum(nil()) -> 0(),
                   sum(cons(x, l)) -> +(x, sum(l)),
                 prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                       prod(nil()) -> s(0()),
                  prod(cons(x, l)) -> *(x, prod(l))}
             SPSC:
              Simple Projection:
               pi(sum#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {app#(cons(x, l1), l2) -> app#(l1, l2)}
     Weak:
     {           +(x, 0()) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
                 +(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))),
             *(*(x, y), z) -> *(x, *(y, z)),
             app(nil(), l) -> l,
      app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
          sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                sum(nil()) -> 0(),
           sum(cons(x, l)) -> +(x, sum(l)),
         prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
               prod(nil()) -> s(0()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(s(x), s(y)) -> *#(x, y),
       *#(*(x, y), z) -> *#(x, *(y, z)),
       *#(*(x, y), z) -> *#(y, z)}
     Weak:
     {           +(x, 0()) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
                 +(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))),
             *(*(x, y), z) -> *(x, *(y, z)),
             app(nil(), l) -> l,
      app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
          sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                sum(nil()) -> 0(),
           sum(cons(x, l)) -> +(x, sum(l)),
         prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
               prod(nil()) -> s(0()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {*#(s(x), s(y)) -> *#(x, y),
        *#(*(x, y), z) -> *#(y, z)}
      EDG:
       {(*#(s(x), s(y)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
        (*#(s(x), s(y)) -> *#(x, y), *#(s(x), s(y)) -> *#(x, y))
        (*#(*(x, y), z) -> *#(y, z), *#(s(x), s(y)) -> *#(x, y))
        (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))}
       SCCS:
        Scc:
         {*#(s(x), s(y)) -> *#(x, y),
          *#(*(x, y), z) -> *#(y, z)}
        SCC:
         Strict:
          {*#(s(x), s(y)) -> *#(x, y),
           *#(*(x, y), z) -> *#(y, z)}
         Weak:
         {           +(x, 0()) -> x,
                 +(+(x, y), z) -> +(x, +(y, z)),
                     +(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))),
                 *(*(x, y), z) -> *(x, *(y, z)),
                 app(nil(), l) -> l,
          app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                    sum(nil()) -> 0(),
               sum(cons(x, l)) -> +(x, sum(l)),
             prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                   prod(nil()) -> s(0()),
              prod(cons(x, l)) -> *(x, prod(l))}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {*#(s(x), s(y)) -> *#(x, y)}
          EDG:
           {(*#(s(x), s(y)) -> *#(x, y), *#(s(x), s(y)) -> *#(x, y))}
           SCCS:
            Scc:
             {*#(s(x), s(y)) -> *#(x, y)}
            SCC:
             Strict:
              {*#(s(x), s(y)) -> *#(x, y)}
             Weak:
             {           +(x, 0()) -> x,
                     +(+(x, y), z) -> +(x, +(y, z)),
                         +(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))),
                     *(*(x, y), z) -> *(x, *(y, z)),
                     app(nil(), l) -> l,
              app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
                  sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                        sum(nil()) -> 0(),
                   sum(cons(x, l)) -> +(x, sum(l)),
                 prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                       prod(nil()) -> s(0()),
                  prod(cons(x, l)) -> *(x, prod(l))}
             SPSC:
              Simple Projection:
               pi(*#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {+#(+(x, y), z) -> +#(x, +(y, z)),
       +#(+(x, y), z) -> +#(y, z),
       +#(s(x), s(y)) -> +#(x, y)}
     Weak:
     {           +(x, 0()) -> x,
             +(+(x, y), z) -> +(x, +(y, z)),
                 +(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))),
             *(*(x, y), z) -> *(x, *(y, z)),
             app(nil(), l) -> l,
      app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
          sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                sum(nil()) -> 0(),
           sum(cons(x, l)) -> +(x, sum(l)),
         prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
               prod(nil()) -> s(0()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {+#(+(x, y), z) -> +#(x, +(y, z)),
        +#(s(x), s(y)) -> +#(x, y)}
      EDG:
       {(+#(s(x), s(y)) -> +#(x, y), +#(s(x), s(y)) -> +#(x, y))
        (+#(s(x), s(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
        (+#(+(x, y), z) -> +#(x, +(y, z)), +#(s(x), s(y)) -> +#(x, y))}
       SCCS:
        Scc:
         {+#(+(x, y), z) -> +#(x, +(y, z)),
          +#(s(x), s(y)) -> +#(x, y)}
        SCC:
         Strict:
          {+#(+(x, y), z) -> +#(x, +(y, z)),
           +#(s(x), s(y)) -> +#(x, y)}
         Weak:
         {           +(x, 0()) -> x,
                 +(+(x, y), z) -> +(x, +(y, z)),
                     +(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))),
                 *(*(x, y), z) -> *(x, *(y, z)),
                 app(nil(), l) -> l,
          app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
              sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                    sum(nil()) -> 0(),
               sum(cons(x, l)) -> +(x, sum(l)),
             prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                   prod(nil()) -> s(0()),
              prod(cons(x, l)) -> *(x, prod(l))}
         SPSC:
          Simple Projection:
           pi(+#) = 0
          Strict:
           {+#(s(x), s(y)) -> +#(x, y)}
          EDG:
           {(+#(s(x), s(y)) -> +#(x, y), +#(s(x), s(y)) -> +#(x, y))}
           SCCS:
            Scc:
             {+#(s(x), s(y)) -> +#(x, y)}
            SCC:
             Strict:
              {+#(s(x), s(y)) -> +#(x, y)}
             Weak:
             {           +(x, 0()) -> x,
                     +(+(x, y), z) -> +(x, +(y, z)),
                         +(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))),
                     *(*(x, y), z) -> *(x, *(y, z)),
                     app(nil(), l) -> l,
              app(cons(x, l1), l2) -> cons(x, app(l1, l2)),
                  sum(app(l1, l2)) -> +(sum(l1), sum(l2)),
                        sum(nil()) -> 0(),
                   sum(cons(x, l)) -> +(x, sum(l)),
                 prod(app(l1, l2)) -> *(prod(l1), prod(l2)),
                       prod(nil()) -> s(0()),
                  prod(cons(x, l)) -> *(x, prod(l))}
             SPSC:
              Simple Projection:
               pi(+#) = 0
              Strict:
               {}
              Qed