YES
Time: 0.051593
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)}
  UR:
   {}
   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# s 0() -> f# 0(), 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# x)
     (f# s 0() -> f# 0(), 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)}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {      f# s 0() -> f# 0(),
            f# +(x, y) -> f# x,
            f# +(x, y) -> f# y,
        f# +(x, s 0()) -> f# x}
      
      SCC (4):
       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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [*](x0, x1) = 0,
         
         [+](x0, x1) = x0 + x1 + 1,
         
         [s](x0) = 0,
         
         [f](x0) = x0,
         
         [0] = 0,
         
         [f#](x0) = x0
        Strict:
         f# +(x, s 0()) -> f# x
         1 + 1x >= 0 + 1x
         f# +(x, y) -> f# y
         1 + 1x + 1y >= 0 + 1y
         f# +(x, y) -> f# x
         1 + 1x + 1y >= 0 + 1x
         f# s 0() -> f# 0()
         0 >= 0
        Weak:
         f +(x, s 0()) -> +(s s 0(), f x)
         1 + 1x >= 1 + 1x
         f +(x, y) -> *(f x, f y)
         1 + 1x + 1y >= 0 + 0x + 0y
         f 0() -> s 0()
         0 >= 0
         f s 0() -> *(s s 0(), f 0())
         0 >= 0
         f s 0() -> s s 0()
         0 >= 0
       SCCS (1):
        Scc:
         {f# s 0() -> f# 0()}
        
        SCC (1):
         Strict:
          {f# s 0() -> f# 0()}
         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)}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [*](x0, x1) = 0,
           
           [+](x0, x1) = x0,
           
           [s](x0) = x0 + 1,
           
           [f](x0) = 0,
           
           [0] = 0,
           
           [f#](x0) = x0
          Strict:
           f# s 0() -> f# 0()
           1 >= 0
          Weak:
           f +(x, s 0()) -> +(s s 0(), f x)
           0 + 0x >= 2 + 0x
           f +(x, y) -> *(f x, f y)
           0 + 0x + 0y >= 0 + 0x + 0y
           f 0() -> s 0()
           0 >= 1
           f s 0() -> *(s s 0(), f 0())
           0 >= 0
           f s 0() -> s s 0()
           0 >= 2
         Qed