YES

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

Proof:
 DP Processor:
  DPs:
   +#(*(x,y),*(a(),y)) -> +#(x,a())
   +#(*(x,y),*(a(),y)) -> *#(+(x,a()),y)
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
  TRS:
   +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
   *(*(x,y),z) -> *(x,*(y,z))
  Usable Rule Processor:
   DPs:
    +#(*(x,y),*(a(),y)) -> +#(x,a())
    +#(*(x,y),*(a(),y)) -> *#(+(x,a()),y)
    *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(x,*(y,z))
   TRS:
    *(*(x,y),z) -> *(x,*(y,z))
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     
    interpretation:
     [*#](x0, x1) = 2x0,
     
     [+#](x0, x1) = 3x0 + 1,
     
     [+](x0, x1) = 0,
     
     [a] = 1,
     
     [*](x0, x1) = x0 + 2x1 + 2
    orientation:
     +#(*(x,y),*(a(),y)) = 3x + 6y + 7 >= 3x + 1 = +#(x,a())
     
     +#(*(x,y),*(a(),y)) = 3x + 6y + 7 >= 0 = *#(+(x,a()),y)
     
     *#(*(x,y),z) = 2x + 4y + 4 >= 2y = *#(y,z)
     
     *#(*(x,y),z) = 2x + 4y + 4 >= 2x = *#(x,*(y,z))
     
     *(*(x,y),z) = x + 2y + 2z + 4 >= x + 2y + 4z + 6 = *(x,*(y,z))
    problem:
     DPs:
      
     TRS:
      *(*(x,y),z) -> *(x,*(y,z))
    Qed