YES(?,O(n^2))

Problem:
 f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a()))

Proof:
 RT Transformation Processor:
  strict:
   f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a()))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 2
   interpretation:
                  [1 2]       
    [f](x0, x1) = [0 1]x0 + x1,
    
          [0]
    [a] = [2]
   orientation:
                             [1 4]    [12]    [1 4]    [8]                         
    f(f(a(),f(x,a())),a()) = [0 1]x + [6 ] >= [0 1]x + [6] = f(a(),f(f(x,a()),a()))
   problem:
    strict:
     
    weak:
     f(f(a(),f(x,a())),a()) -> f(a(),f(f(x,a()),a()))
   Qed