YES
TRS:
 {              0(#()) -> #(),
             +(x, #()) -> x,
             +(#(), x) -> x,
         +(0(x), 0(y)) -> 0(+(x, y)),
         +(0(x), 1(y)) -> 1(+(x, y)),
         +(+(x, y), z) -> +(x, +(y, z)),
         +(1(x), 0(y)) -> 1(+(x, y)),
         +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
         *(x, +(y, z)) -> +(*(x, y), *(x, z)),
             *(#(), x) -> #(),
            *(0(x), y) -> 0(*(x, y)),
            *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
      prod(cons(x, l)) -> *(x, prod(l))}
 DP:
  Strict:
   {       +#(0(x), 0(y)) -> 0#(+(x, y)),
           +#(0(x), 0(y)) -> +#(x, y),
           +#(0(x), 1(y)) -> +#(x, y),
           +#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z),
           +#(1(x), 0(y)) -> +#(x, y),
           +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))),
           +#(1(x), 1(y)) -> +#(x, y),
           +#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
           *#(x, +(y, z)) -> +#(*(x, y), *(x, z)),
           *#(x, +(y, z)) -> *#(x, y),
           *#(x, +(y, z)) -> *#(x, z),
              *#(0(x), y) -> 0#(*(x, y)),
              *#(0(x), y) -> *#(x, y),
              *#(1(x), y) -> 0#(*(x, y)),
              *#(1(x), y) -> +#(0(*(x, y)), y),
              *#(1(x), 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#(nil()) -> 0#(#()),
         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:
  {              0(#()) -> #(),
              +(x, #()) -> x,
              +(#(), x) -> x,
          +(0(x), 0(y)) -> 0(+(x, y)),
          +(0(x), 1(y)) -> 1(+(x, y)),
          +(+(x, y), z) -> +(x, +(y, z)),
          +(1(x), 0(y)) -> 1(+(x, y)),
          +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
          *(x, +(y, z)) -> +(*(x, y), *(x, z)),
              *(#(), x) -> #(),
             *(0(x), y) -> 0(*(x, y)),
             *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
       prod(cons(x, l)) -> *(x, prod(l))}
  EDG:
   {
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> +#(x, y))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 0(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)))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 1(y)) -> +#(x, y))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 0(y)) -> +#(x, y))
    (sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (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)), *#(1(x), y) -> *#(x, y))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> +#(0(*(x, y)), y))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> 0#(*(x, y)))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(0(x), y) -> *#(x, y))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(0(x), y) -> 0#(*(x, y)))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(x, +(y, z)) -> *#(x, z))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(x, +(y, z)) -> *#(x, y))
    (prod#(cons(x, l)) -> *#(x, prod(l)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> prod#(l))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(cons(x, l)) -> *#(x, prod(l)))
    (prod#(app(l1, l2)) -> prod#(l2), prod#(app(l1, l2)) -> 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(l1), prod(l2)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 0(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(y, z))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 1(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> +#(x, y))
    (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(x, +(y, z)) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
    (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
    (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
    (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
    (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
    (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
    (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
    (*#(1(x), y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> prod#(l))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(cons(x, l)) -> *#(x, prod(l)))
    (prod#(app(l1, l2)) -> prod#(l1), prod#(app(l1, l2)) -> 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(l1), prod(l2)))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 1(y)) -> +#(x, y))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(1(x), 0(y)) -> +#(x, y))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(0(x), 1(y)) -> +#(x, y))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(0(x), 0(y)) -> +#(x, y))
    (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z))
    (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(x, +(y, z)) -> *#(x, z), *#(1(x), y) -> 0#(*(x, y)))
    (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> 0#(*(x, y)))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (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#(nil()) -> 0#(#()))
    (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#(app(l1, l2)) -> *#(prod(l1), 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#(l2))
    (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))
    (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z))
    (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(*(x, y), z) -> *#(y, z), *#(1(x), 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) -> +#(y, z), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(0(x), 1(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) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> *#(x, y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> 0#(*(x, y)))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), 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)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 1(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)), +#(1(x), 0(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(x, y))
    (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(app(l1, l2)) -> +#(sum(l1), 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#(l2))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(nil()) -> 0#(#()))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> +#(x, sum(l)))
    (sum#(app(l1, l2)) -> sum#(l1), sum#(cons(x, l)) -> sum#(l))
    (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
    (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
    (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
    (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
    (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
    (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
    (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
    (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
    (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
    (+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (app#(cons(x, l1), l2) -> app#(l1, l2), app#(cons(x, l1), l2) -> app#(l1, l2))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z)))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
    (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
    (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#(nil()) -> 0#(#()))
    (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)), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(x, +(y, z)) -> *#(x, y))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(x, +(y, z)) -> *#(x, z))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(0(x), y) -> 0#(*(x, y)))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(0(x), y) -> *#(x, y))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(1(x), y) -> 0#(*(x, y)))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(1(x), y) -> +#(0(*(x, y)), y))
    (prod#(app(l1, l2)) -> *#(prod(l1), prod(l2)), *#(1(x), 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)), +#(0(x), 0(y)) -> 0#(+(x, y)))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(0(x), 0(y)) -> +#(x, y))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(0(x), 1(y)) -> +#(x, y))
    (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)), +#(1(x), 0(y)) -> +#(x, y))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 1(y)) -> +#(x, y))
    (sum#(app(l1, l2)) -> +#(sum(l1), sum(l2)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
   }
   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:
     {*#(x, +(y, z)) -> *#(x, y),
      *#(x, +(y, z)) -> *#(x, z),
         *#(0(x), y) -> *#(x, y),
         *#(1(x), y) -> *#(x, y),
      *#(*(x, y), z) -> *#(x, *(y, z)),
      *#(*(x, y), z) -> *#(y, z)}
    Scc:
     {+#(0(x), 0(y)) -> +#(x, y),
      +#(0(x), 1(y)) -> +#(x, y),
      +#(+(x, y), z) -> +#(x, +(y, z)),
      +#(+(x, y), z) -> +#(y, z),
      +#(1(x), 0(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(x, y),
      +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
    SCC:
     Strict:
      {prod#(app(l1, l2)) -> prod#(l1),
       prod#(app(l1, l2)) -> prod#(l2),
        prod#(cons(x, l)) -> prod#(l)}
     Weak:
     {              0(#()) -> #(),
                 +(x, #()) -> x,
                 +(#(), x) -> x,
             +(0(x), 0(y)) -> 0(+(x, y)),
             +(0(x), 1(y)) -> 1(+(x, y)),
             +(+(x, y), z) -> +(x, +(y, z)),
             +(1(x), 0(y)) -> 1(+(x, y)),
             +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
             *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                 *(#(), x) -> #(),
                *(0(x), y) -> 0(*(x, y)),
                *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
          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:
         {              0(#()) -> #(),
                     +(x, #()) -> x,
                     +(#(), x) -> x,
                 +(0(x), 0(y)) -> 0(+(x, y)),
                 +(0(x), 1(y)) -> 1(+(x, y)),
                 +(+(x, y), z) -> +(x, +(y, z)),
                 +(1(x), 0(y)) -> 1(+(x, y)),
                 +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                 *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                     *(#(), x) -> #(),
                    *(0(x), y) -> 0(*(x, y)),
                    *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
              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:
             {              0(#()) -> #(),
                         +(x, #()) -> x,
                         +(#(), x) -> x,
                     +(0(x), 0(y)) -> 0(+(x, y)),
                     +(0(x), 1(y)) -> 1(+(x, y)),
                     +(+(x, y), z) -> +(x, +(y, z)),
                     +(1(x), 0(y)) -> 1(+(x, y)),
                     +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                     *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                         *(#(), x) -> #(),
                        *(0(x), y) -> 0(*(x, y)),
                        *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                  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:
     {              0(#()) -> #(),
                 +(x, #()) -> x,
                 +(#(), x) -> x,
             +(0(x), 0(y)) -> 0(+(x, y)),
             +(0(x), 1(y)) -> 1(+(x, y)),
             +(+(x, y), z) -> +(x, +(y, z)),
             +(1(x), 0(y)) -> 1(+(x, y)),
             +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
             *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                 *(#(), x) -> #(),
                *(0(x), y) -> 0(*(x, y)),
                *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
          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:
         {              0(#()) -> #(),
                     +(x, #()) -> x,
                     +(#(), x) -> x,
                 +(0(x), 0(y)) -> 0(+(x, y)),
                 +(0(x), 1(y)) -> 1(+(x, y)),
                 +(+(x, y), z) -> +(x, +(y, z)),
                 +(1(x), 0(y)) -> 1(+(x, y)),
                 +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                 *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                     *(#(), x) -> #(),
                    *(0(x), y) -> 0(*(x, y)),
                    *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
              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:
             {              0(#()) -> #(),
                         +(x, #()) -> x,
                         +(#(), x) -> x,
                     +(0(x), 0(y)) -> 0(+(x, y)),
                     +(0(x), 1(y)) -> 1(+(x, y)),
                     +(+(x, y), z) -> +(x, +(y, z)),
                     +(1(x), 0(y)) -> 1(+(x, y)),
                     +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                     *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                         *(#(), x) -> #(),
                        *(0(x), y) -> 0(*(x, y)),
                        *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                  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:
     {              0(#()) -> #(),
                 +(x, #()) -> x,
                 +(#(), x) -> x,
             +(0(x), 0(y)) -> 0(+(x, y)),
             +(0(x), 1(y)) -> 1(+(x, y)),
             +(+(x, y), z) -> +(x, +(y, z)),
             +(1(x), 0(y)) -> 1(+(x, y)),
             +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
             *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                 *(#(), x) -> #(),
                *(0(x), y) -> 0(*(x, y)),
                *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(app#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(x, +(y, z)) -> *#(x, y),
       *#(x, +(y, z)) -> *#(x, z),
          *#(0(x), y) -> *#(x, y),
          *#(1(x), y) -> *#(x, y),
       *#(*(x, y), z) -> *#(x, *(y, z)),
       *#(*(x, y), z) -> *#(y, z)}
     Weak:
     {              0(#()) -> #(),
                 +(x, #()) -> x,
                 +(#(), x) -> x,
             +(0(x), 0(y)) -> 0(+(x, y)),
             +(0(x), 1(y)) -> 1(+(x, y)),
             +(+(x, y), z) -> +(x, +(y, z)),
             +(1(x), 0(y)) -> 1(+(x, y)),
             +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
             *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                 *(#(), x) -> #(),
                *(0(x), y) -> 0(*(x, y)),
                *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
          prod(cons(x, l)) -> *(x, prod(l))}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {*#(x, +(y, z)) -> *#(x, y),
        *#(x, +(y, z)) -> *#(x, z),
           *#(0(x), y) -> *#(x, y),
        *#(*(x, y), z) -> *#(x, *(y, z)),
        *#(*(x, y), z) -> *#(y, z)}
      EDG:
       {(*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
        (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
        (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y))
        (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z))
        (*#(*(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y))
        (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
        (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
        (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
        (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
        (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
        (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y))
        (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z))
        (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), 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), *#(x, +(y, z)) -> *#(x, y))
        (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
        (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y))
        (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
        (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
        (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
        (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
        (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y))
        (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)))
        (*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(y, z))}
       SCCS:
        Scc:
         {*#(x, +(y, z)) -> *#(x, y),
          *#(x, +(y, z)) -> *#(x, z),
             *#(0(x), y) -> *#(x, y),
          *#(*(x, y), z) -> *#(x, *(y, z)),
          *#(*(x, y), z) -> *#(y, z)}
        SCC:
         Strict:
          {*#(x, +(y, z)) -> *#(x, y),
           *#(x, +(y, z)) -> *#(x, z),
              *#(0(x), y) -> *#(x, y),
           *#(*(x, y), z) -> *#(x, *(y, z)),
           *#(*(x, y), z) -> *#(y, z)}
         Weak:
         {              0(#()) -> #(),
                     +(x, #()) -> x,
                     +(#(), x) -> x,
                 +(0(x), 0(y)) -> 0(+(x, y)),
                 +(0(x), 1(y)) -> 1(+(x, y)),
                 +(+(x, y), z) -> +(x, +(y, z)),
                 +(1(x), 0(y)) -> 1(+(x, y)),
                 +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                 *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                     *(#(), x) -> #(),
                    *(0(x), y) -> 0(*(x, y)),
                    *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
              prod(cons(x, l)) -> *(x, prod(l))}
         SPSC:
          Simple Projection:
           pi(*#) = 0
          Strict:
           {*#(x, +(y, z)) -> *#(x, y),
            *#(x, +(y, z)) -> *#(x, z),
               *#(0(x), y) -> *#(x, y),
            *#(*(x, y), z) -> *#(x, *(y, z))}
          EDG:
           {(*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)))
            (*#(x, +(y, z)) -> *#(x, z), *#(0(x), y) -> *#(x, y))
            (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
            (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
            (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
            (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
            (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
            (*#(0(x), y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
            (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
            (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
            (*#(x, +(y, z)) -> *#(x, y), *#(0(x), y) -> *#(x, y))
            (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
            (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y))
            (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z))
            (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> *#(x, y))
            (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))}
           SCCS:
            Scc:
             {*#(x, +(y, z)) -> *#(x, y),
              *#(x, +(y, z)) -> *#(x, z),
                 *#(0(x), y) -> *#(x, y),
              *#(*(x, y), z) -> *#(x, *(y, z))}
            SCC:
             Strict:
              {*#(x, +(y, z)) -> *#(x, y),
               *#(x, +(y, z)) -> *#(x, z),
                  *#(0(x), y) -> *#(x, y),
               *#(*(x, y), z) -> *#(x, *(y, z))}
             Weak:
             {              0(#()) -> #(),
                         +(x, #()) -> x,
                         +(#(), x) -> x,
                     +(0(x), 0(y)) -> 0(+(x, y)),
                     +(0(x), 1(y)) -> 1(+(x, y)),
                     +(+(x, y), z) -> +(x, +(y, z)),
                     +(1(x), 0(y)) -> 1(+(x, y)),
                     +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                     *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                         *(#(), x) -> #(),
                        *(0(x), y) -> 0(*(x, y)),
                        *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                  prod(cons(x, l)) -> *(x, prod(l))}
             SPSC:
              Simple Projection:
               pi(*#) = 0
              Strict:
               {*#(x, +(y, z)) -> *#(x, y),
                *#(x, +(y, z)) -> *#(x, z),
                *#(*(x, y), z) -> *#(x, *(y, z))}
              EDG:
               {(*#(x, +(y, z)) -> *#(x, z), *#(*(x, y), z) -> *#(x, *(y, z)))
                (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
                (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
                (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
                (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
                (*#(x, +(y, z)) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
                (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, y))
                (*#(*(x, y), z) -> *#(x, *(y, z)), *#(x, +(y, z)) -> *#(x, z))
                (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))}
               SCCS:
                Scc:
                 {*#(x, +(y, z)) -> *#(x, y),
                  *#(x, +(y, z)) -> *#(x, z),
                  *#(*(x, y), z) -> *#(x, *(y, z))}
                SCC:
                 Strict:
                  {*#(x, +(y, z)) -> *#(x, y),
                   *#(x, +(y, z)) -> *#(x, z),
                   *#(*(x, y), z) -> *#(x, *(y, z))}
                 Weak:
                 {              0(#()) -> #(),
                             +(x, #()) -> x,
                             +(#(), x) -> x,
                         +(0(x), 0(y)) -> 0(+(x, y)),
                         +(0(x), 1(y)) -> 1(+(x, y)),
                         +(+(x, y), z) -> +(x, +(y, z)),
                         +(1(x), 0(y)) -> 1(+(x, y)),
                         +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                         *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                             *(#(), x) -> #(),
                            *(0(x), y) -> 0(*(x, y)),
                            *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                      prod(cons(x, l)) -> *(x, prod(l))}
                 SPSC:
                  Simple Projection:
                   pi(*#) = 0
                  Strict:
                   {*#(x, +(y, z)) -> *#(x, y),
                    *#(x, +(y, z)) -> *#(x, z)}
                  EDG:
                   {(*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
                    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
                    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
                    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))}
                   SCCS:
                    Scc:
                     {*#(x, +(y, z)) -> *#(x, y),
                      *#(x, +(y, z)) -> *#(x, z)}
                    SCC:
                     Strict:
                      {*#(x, +(y, z)) -> *#(x, y),
                       *#(x, +(y, z)) -> *#(x, z)}
                     Weak:
                     {              0(#()) -> #(),
                                 +(x, #()) -> x,
                                 +(#(), x) -> x,
                             +(0(x), 0(y)) -> 0(+(x, y)),
                             +(0(x), 1(y)) -> 1(+(x, y)),
                             +(+(x, y), z) -> +(x, +(y, z)),
                             +(1(x), 0(y)) -> 1(+(x, y)),
                             +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                             *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                                 *(#(), x) -> #(),
                                *(0(x), y) -> 0(*(x, y)),
                                *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                          prod(cons(x, l)) -> *(x, prod(l))}
                     SPSC:
                      Simple Projection:
                       pi(*#) = 1
                      Strict:
                       {*#(x, +(y, z)) -> *#(x, z)}
                      EDG:
                       {(*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))}
                       SCCS:
                        Scc:
                         {*#(x, +(y, z)) -> *#(x, z)}
                        SCC:
                         Strict:
                          {*#(x, +(y, z)) -> *#(x, z)}
                         Weak:
                         {              0(#()) -> #(),
                                     +(x, #()) -> x,
                                     +(#(), x) -> x,
                                 +(0(x), 0(y)) -> 0(+(x, y)),
                                 +(0(x), 1(y)) -> 1(+(x, y)),
                                 +(+(x, y), z) -> +(x, +(y, z)),
                                 +(1(x), 0(y)) -> 1(+(x, y)),
                                 +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                                 *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                                     *(#(), x) -> #(),
                                    *(0(x), y) -> 0(*(x, y)),
                                    *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                              prod(cons(x, l)) -> *(x, prod(l))}
                         SPSC:
                          Simple Projection:
                           pi(*#) = 1
                          Strict:
                           {}
                          Qed
    SCC:
     Strict:
      {+#(0(x), 0(y)) -> +#(x, y),
       +#(0(x), 1(y)) -> +#(x, y),
       +#(+(x, y), z) -> +#(x, +(y, z)),
       +#(+(x, y), z) -> +#(y, z),
       +#(1(x), 0(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(x, y),
       +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
     Weak:
     {              0(#()) -> #(),
                 +(x, #()) -> x,
                 +(#(), x) -> x,
             +(0(x), 0(y)) -> 0(+(x, y)),
             +(0(x), 1(y)) -> 1(+(x, y)),
             +(+(x, y), z) -> +(x, +(y, z)),
             +(1(x), 0(y)) -> 1(+(x, y)),
             +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
             *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                 *(#(), x) -> #(),
                *(0(x), y) -> 0(*(x, y)),
                *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
          prod(cons(x, l)) -> *(x, prod(l))}
     POLY:
      Argument Filtering:
       pi(prod) = [], pi(sum) = [], pi(cons) = [], pi(nil) = [], pi(app) = [], pi(*) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = [0], pi(#) = []
      Usable Rules:
       {}
      Interpretation:
       [+#](x0, x1) = x0 + x1,
       [+](x0, x1) = x0 + x1,
       [1](x0) = x0 + 1,
       [0](x0) = x0 + 1,
       [#] = 0
      Strict:
       {+#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z)}
      Weak:
       {              0(#()) -> #(),
                   +(x, #()) -> x,
                   +(#(), x) -> x,
               +(0(x), 0(y)) -> 0(+(x, y)),
               +(0(x), 1(y)) -> 1(+(x, y)),
               +(+(x, y), z) -> +(x, +(y, z)),
               +(1(x), 0(y)) -> 1(+(x, y)),
               +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
               *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                   *(#(), x) -> #(),
                  *(0(x), y) -> 0(*(x, y)),
                  *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
            prod(cons(x, l)) -> *(x, prod(l))}
      EDG:
       {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(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) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))}
       SCCS:
        Scc:
         {+#(+(x, y), z) -> +#(x, +(y, z)),
          +#(+(x, y), z) -> +#(y, z)}
        SCC:
         Strict:
          {+#(+(x, y), z) -> +#(x, +(y, z)),
           +#(+(x, y), z) -> +#(y, z)}
         Weak:
         {              0(#()) -> #(),
                     +(x, #()) -> x,
                     +(#(), x) -> x,
                 +(0(x), 0(y)) -> 0(+(x, y)),
                 +(0(x), 1(y)) -> 1(+(x, y)),
                 +(+(x, y), z) -> +(x, +(y, z)),
                 +(1(x), 0(y)) -> 1(+(x, y)),
                 +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                 *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                     *(#(), x) -> #(),
                    *(0(x), y) -> 0(*(x, y)),
                    *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
              prod(cons(x, l)) -> *(x, prod(l))}
         SPSC:
          Simple Projection:
           pi(+#) = 0
          Strict:
           {+#(+(x, y), z) -> +#(y, z)}
          EDG:
           {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))}
           SCCS:
            Scc:
             {+#(+(x, y), z) -> +#(y, z)}
            SCC:
             Strict:
              {+#(+(x, y), z) -> +#(y, z)}
             Weak:
             {              0(#()) -> #(),
                         +(x, #()) -> x,
                         +(#(), x) -> x,
                     +(0(x), 0(y)) -> 0(+(x, y)),
                     +(0(x), 1(y)) -> 1(+(x, y)),
                     +(+(x, y), z) -> +(x, +(y, z)),
                     +(1(x), 0(y)) -> 1(+(x, y)),
                     +(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
                     *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                         *(#(), x) -> #(),
                        *(0(x), y) -> 0(*(x, y)),
                        *(1(x), y) -> +(0(*(x, y)), 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()) -> 1(#()),
                  prod(cons(x, l)) -> *(x, prod(l))}
             SPSC:
              Simple Projection:
               pi(+#) = 0
              Strict:
               {}
              Qed