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
   
   usable rules:
    +(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))
   interpretation:
    [f#](x0, x1) = 2x0 + 3/2,
    
    [+#](x0, x1) = 2x0 + x1,
    
    [f](x0, x1) = x0,
    
    [+](x0, x1) = x0 + x1 + 1,
    
    [b] = 3/2,
    
    [a] = 2
   orientation:
    +#(a(),b()) = 11/2 >= 5 = +#(b(),a())
    
    +#(a(),+(b(),z)) = z + 13/2 >= z + 4 = +#(a(),z)
    
    +#(a(),+(b(),z)) = z + 13/2 >= z + 6 = +#(b(),+(a(),z))
    
    +#(+(x,y),z) = 2x + 2y + z + 2 >= 2y + z = +#(y,z)
    
    +#(+(x,y),z) = 2x + 2y + z + 2 >= 2x + y + z + 1 = +#(x,+(y,z))
    
    f#(+(x,y),z) = 2x + 2y + 7/2 >= 2y + 3/2 = f#(y,z)
    
    f#(+(x,y),z) = 2x + 2y + 7/2 >= 2x + 3/2 = f#(x,z)
    
    f#(+(x,y),z) = 2x + 2y + 7/2 >= 2x + y = +#(f(x,z),f(y,z))
    
    +(a(),b()) = 9/2 >= 9/2 = +(b(),a())
    
    +(a(),+(b(),z)) = z + 11/2 >= z + 11/2 = +(b(),+(a(),z))
    
    +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z))
    
    f(a(),y) = 2 >= 2 = a()
    
    f(b(),y) = 3/2 >= 3/2 = b()
    
    f(+(x,y),z) = x + y + 1 >= x + y + 1 = +(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