YES(?,O(n^2))

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

Proof:
 RT Transformation Processor:
  strict:
   *(x,*(y,z)) -> *(*(x,y),z)
   *(x,x) -> x
  weak:
   
  Bounds Processor:
   bound: 0
   enrichment: match-rt
   automaton:
    final states: {2}
    transitions:
     *0(2,2) -> 2*
   problem:
    strict:
     *(x,*(y,z)) -> *(*(x,y),z)
    weak:
     *(x,x) -> x
   Matrix Interpretation Processor:
    dimension: 2
    interpretation:
                        [1 1]     [2]
     [*](x0, x1) = x0 + [0 1]x1 + [1]
    orientation:
                       [1 1]    [1 2]    [5]        [1 1]    [1 1]    [4]              
     *(x,*(y,z)) = x + [0 1]y + [0 1]z + [2] >= x + [0 1]y + [0 1]z + [2] = *(*(x,y),z)
     
              [2 1]    [2]         
     *(x,x) = [0 2]x + [1] >= x = x
    problem:
     strict:
      
     weak:
      *(x,*(y,z)) -> *(*(x,y),z)
      *(x,x) -> x
    Qed