YES

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

Proof:
 DP Processor:
  DPs:
   f#(+(x,0())) -> f#(x)
   +#(x,+(y,z)) -> +#(x,y)
   +#(x,+(y,z)) -> +#(+(x,y),z)
  TRS:
   f(+(x,0())) -> f(x)
   +(x,+(y,z)) -> +(+(x,y),z)
  Usable Rule Processor:
   DPs:
    f#(+(x,0())) -> f#(x)
    +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z)
   TRS:
    +(x,+(y,z)) -> +(+(x,y),z)
   TDG Processor:
    DPs:
     f#(+(x,0())) -> f#(x)
     +#(x,+(y,z)) -> +#(x,y)
     +#(x,+(y,z)) -> +#(+(x,y),z)
    TRS:
     +(x,+(y,z)) -> +(+(x,y),z)
    graph:
     +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z)
     +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(x,y)
     +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
     +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
     f#(+(x,0())) -> f#(x) -> f#(+(x,0())) -> f#(x)
    Restore Modifier:
     DPs:
      f#(+(x,0())) -> f#(x)
      +#(x,+(y,z)) -> +#(x,y)
      +#(x,+(y,z)) -> +#(+(x,y),z)
     TRS:
      f(+(x,0())) -> f(x)
      +(x,+(y,z)) -> +(+(x,y),z)
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 5/9
      DPs:
       f#(+(x,0())) -> f#(x)
      TRS:
       f(+(x,0())) -> f(x)
       +(x,+(y,z)) -> +(+(x,y),z)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0) = x0 + 1,
        
        [f](x0) = 0,
        
        [+](x0, x1) = x0 + x1,
        
        [0] = 1
       orientation:
        f#(+(x,0())) = x + 2 >= x + 1 = f#(x)
        
        f(+(x,0())) = 0 >= 0 = f(x)
        
        +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
       problem:
        DPs:
         
        TRS:
         f(+(x,0())) -> f(x)
         +(x,+(y,z)) -> +(+(x,y),z)
       Qed
      
      DPs:
       +#(x,+(y,z)) -> +#(+(x,y),z)
       +#(x,+(y,z)) -> +#(x,y)
      TRS:
       f(+(x,0())) -> f(x)
       +(x,+(y,z)) -> +(+(x,y),z)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [+#](x0, x1) = x0 + x1,
        
        [f](x0) = 1,
        
        [+](x0, x1) = x0 + x1 + 1,
        
        [0] = 0
       orientation:
        +#(x,+(y,z)) = x + y + z + 1 >= x + y + z + 1 = +#(+(x,y),z)
        
        +#(x,+(y,z)) = x + y + z + 1 >= x + y = +#(x,y)
        
        f(+(x,0())) = 1 >= 1 = f(x)
        
        +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z)
       problem:
        DPs:
         +#(x,+(y,z)) -> +#(+(x,y),z)
        TRS:
         f(+(x,0())) -> f(x)
         +(x,+(y,z)) -> +(+(x,y),z)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [+#](x0, x1) = x1,
         
         [f](x0) = 0,
         
         [+](x0, x1) = x1 + 1,
         
         [0] = 0
        orientation:
         +#(x,+(y,z)) = z + 1 >= z = +#(+(x,y),z)
         
         f(+(x,0())) = 0 >= 0 = f(x)
         
         +(x,+(y,z)) = z + 2 >= z + 1 = +(+(x,y),z)
        problem:
         DPs:
          
         TRS:
          f(+(x,0())) -> f(x)
          +(x,+(y,z)) -> +(+(x,y),z)
        Qed