YES

Problem:
 f(0()) -> s(0())
 f(s(0())) -> s(s(0()))
 f(s(0())) -> *(s(s(0())),f(0()))
 f(+(x,s(0()))) -> +(s(s(0())),f(x))
 f(+(x,y)) -> *(f(x),f(y))

Proof:
 DP Processor:
  DPs:
   f#(s(0())) -> f#(0())
   f#(+(x,s(0()))) -> f#(x)
   f#(+(x,y)) -> f#(y)
   f#(+(x,y)) -> f#(x)
  TRS:
   f(0()) -> s(0())
   f(s(0())) -> s(s(0()))
   f(s(0())) -> *(s(s(0())),f(0()))
   f(+(x,s(0()))) -> +(s(s(0())),f(x))
   f(+(x,y)) -> *(f(x),f(y))
  Usable Rule Processor:
   DPs:
    f#(s(0())) -> f#(0())
    f#(+(x,s(0()))) -> f#(x)
    f#(+(x,y)) -> f#(y)
    f#(+(x,y)) -> f#(x)
   TRS:
    
   CDG Processor:
    DPs:
     f#(s(0())) -> f#(0())
     f#(+(x,s(0()))) -> f#(x)
     f#(+(x,y)) -> f#(y)
     f#(+(x,y)) -> f#(x)
    TRS:
     
    graph:
     f#(+(x,s(0()))) -> f#(x) -> f#(s(0())) -> f#(0())
     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,y)) -> f#(y) -> 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#(x) -> f#(s(0())) -> f#(0())
     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)
    Restore Modifier:
     DPs:
      f#(s(0())) -> f#(0())
      f#(+(x,s(0()))) -> f#(x)
      f#(+(x,y)) -> f#(y)
      f#(+(x,y)) -> f#(x)
     TRS:
      f(0()) -> s(0())
      f(s(0())) -> s(s(0()))
      f(s(0())) -> *(s(s(0())),f(0()))
      f(+(x,s(0()))) -> +(s(s(0())),f(x))
      f(+(x,y)) -> *(f(x),f(y))
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 12/16
      DPs:
       f#(+(x,s(0()))) -> f#(x)
       f#(+(x,y)) -> f#(x)
       f#(+(x,y)) -> f#(y)
      TRS:
       f(0()) -> s(0())
       f(s(0())) -> s(s(0()))
       f(s(0())) -> *(s(s(0())),f(0()))
       f(+(x,s(0()))) -> +(s(s(0())),f(x))
       f(+(x,y)) -> *(f(x),f(y))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0) = x0 + 1,
        
        [+](x0, x1) = x0 + x1 + 1,
        
        [*](x0, x1) = 0,
        
        [s](x0) = 0,
        
        [f](x0) = x0,
        
        [0] = 1
       orientation:
        f#(+(x,s(0()))) = x + 2 >= x + 1 = f#(x)
        
        f#(+(x,y)) = x + y + 2 >= x + 1 = f#(x)
        
        f#(+(x,y)) = x + y + 2 >= y + 1 = f#(y)
        
        f(0()) = 1 >= 0 = s(0())
        
        f(s(0())) = 0 >= 0 = s(s(0()))
        
        f(s(0())) = 0 >= 0 = *(s(s(0())),f(0()))
        
        f(+(x,s(0()))) = x + 1 >= x + 1 = +(s(s(0())),f(x))
        
        f(+(x,y)) = x + y + 1 >= 0 = *(f(x),f(y))
       problem:
        DPs:
         
        TRS:
         f(0()) -> s(0())
         f(s(0())) -> s(s(0()))
         f(s(0())) -> *(s(s(0())),f(0()))
         f(+(x,s(0()))) -> +(s(s(0())),f(x))
         f(+(x,y)) -> *(f(x),f(y))
       Qed