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