YES
Time: 0.001650
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:
  DP:
   {      f# s 0() -> f# 0(),
        f# +(x, y) -> f# x,
        f# +(x, y) -> f# y,
    f# +(x, s 0()) -> f# x}
  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)}
  EDG:
   {(f# +(x, s 0()) -> f# x, f# +(x, s 0()) -> f# x)
    (f# +(x, s 0()) -> f# x, f# +(x, y) -> f# y)
    (f# +(x, s 0()) -> f# x, f# +(x, y) -> f# x)
    (f# +(x, s 0()) -> f# x, f# s 0() -> f# 0())
    (f# +(x, y) -> f# y, f# s 0() -> f# 0())
    (f# +(x, y) -> f# y, f# +(x, y) -> f# x)
    (f# +(x, y) -> f# y, f# +(x, y) -> f# y)
    (f# +(x, y) -> f# y, f# +(x, s 0()) -> f# x)
    (f# +(x, y) -> f# x, f# s 0() -> f# 0())
    (f# +(x, y) -> f# x, f# +(x, y) -> f# x)
    (f# +(x, y) -> f# x, f# +(x, y) -> f# y)
    (f# +(x, y) -> f# x, f# +(x, s 0()) -> f# x)}
   SCCS (1):
    Scc:
     {    f# +(x, y) -> f# x,
          f# +(x, y) -> f# y,
      f# +(x, s 0()) -> f# x}
    SCC (3):
     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 (1):
        Scc:
         {    f# +(x, y) -> f# x,
          f# +(x, s 0()) -> f# x}
        SCC (2):
         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 (1):
            Scc:
             {f# +(x, s 0()) -> f# x}
            SCC (1):
             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