YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
   *(*(x,y),z) -> *(x,*(y,z))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [+](x0, x1) = x0 + x1 + 3,
    
    [a] = 14,
    
    [*](x0, x1) = x0 + x1 + 4
   orientation:
    +(*(x,y),*(a(),y)) = x + 2y + 25 >= x + y + 21 = *(+(x,a()),y)
    
    *(*(x,y),z) = x + y + z + 8 >= x + y + z + 8 = *(x,*(y,z))
   problem:
    strict:
     *(*(x,y),z) -> *(x,*(y,z))
    weak:
     +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                   [1 1]          [4]
     [+](x0, x1) = [0 0]x0 + x1 + [2],
     
           [14]
     [a] = [1 ],
     
                   [1 2]          [0]
     [*](x0, x1) = [0 1]x0 + x1 + [8]
    orientation:
                   [1 4]    [1 2]        [16]    [1 2]    [1 2]        [0 ]              
     *(*(x,y),z) = [0 1]x + [0 1]y + z + [16] >= [0 1]x + [0 1]y + z + [16] = *(x,*(y,z))
     
                          [1 3]    [2 1]    [28]    [1 1]        [24]                
     +(*(x,y),*(a(),y)) = [0 0]x + [0 1]y + [11] >= [0 0]x + y + [11] = *(+(x,a()),y)
    problem:
     strict:
      
     weak:
      *(*(x,y),z) -> *(x,*(y,z))
      +(*(x,y),*(a(),y)) -> *(+(x,a()),y)
    Qed