YES

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

Proof:
 DP Processor:
  DPs:
   +#(a(),b()) -> +#(b(),a())
   +#(a(),+(b(),z)) -> +#(a(),z)
   +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   f#(+(x,y),z) -> f#(y,z)
   f#(+(x,y),z) -> f#(x,z)
   f#(+(x,y),z) -> +#(f(x,z),f(y,z))
  TRS:
   +(a(),b()) -> +(b(),a())
   +(a(),+(b(),z)) -> +(b(),+(a(),z))
   +(+(x,y),z) -> +(x,+(y,z))
   f(a(),y) -> a()
   f(b(),y) -> b()
   f(+(x,y),z) -> +(f(x,z),f(y,z))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [f#](x0, x1) = 7x0 + 2x1 + 3,
    
    [+#](x0, x1) = 2x0 + x1,
    
    [f](x0, x1) = 2x0 + 4,
    
    [+](x0, x1) = x0 + x1 + 4,
    
    [b] = 2,
    
    [a] = 4
   orientation:
    +#(a(),b()) = 10 >= 8 = +#(b(),a())
    
    +#(a(),+(b(),z)) = z + 14 >= z + 8 = +#(a(),z)
    
    +#(a(),+(b(),z)) = z + 14 >= z + 12 = +#(b(),+(a(),z))
    
    +#(+(x,y),z) = 2x + 2y + z + 8 >= 2y + z = +#(y,z)
    
    +#(+(x,y),z) = 2x + 2y + z + 8 >= 2x + y + z + 4 = +#(x,+(y,z))
    
    f#(+(x,y),z) = 7x + 7y + 2z + 31 >= 7y + 2z + 3 = f#(y,z)
    
    f#(+(x,y),z) = 7x + 7y + 2z + 31 >= 7x + 2z + 3 = f#(x,z)
    
    f#(+(x,y),z) = 7x + 7y + 2z + 31 >= 4x + 2y + 12 = +#(f(x,z),f(y,z))
    
    +(a(),b()) = 10 >= 10 = +(b(),a())
    
    +(a(),+(b(),z)) = z + 14 >= z + 14 = +(b(),+(a(),z))
    
    +(+(x,y),z) = x + y + z + 8 >= x + y + z + 8 = +(x,+(y,z))
    
    f(a(),y) = 12 >= 4 = a()
    
    f(b(),y) = 8 >= 2 = b()
    
    f(+(x,y),z) = 2x + 2y + 12 >= 2x + 2y + 12 = +(f(x,z),f(y,z))
   problem:
    DPs:
     
    TRS:
     +(a(),b()) -> +(b(),a())
     +(a(),+(b(),z)) -> +(b(),+(a(),z))
     +(+(x,y),z) -> +(x,+(y,z))
     f(a(),y) -> a()
     f(b(),y) -> b()
     f(+(x,y),z) -> +(f(x,z),f(y,z))
   Qed