YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                 [1 2]     [1 4]     [0]
   [f](x0, x1) = [0 1]x0 + [0 1]x1 + [2],
   
         [0]
   [a] = [0]
  orientation:
                            [1  10]    [20]    [1  10]    [16]                         
   f(a(),f(f(a(),x),a())) = [0  1 ]x + [6 ] >= [0  1 ]x + [6 ] = f(f(a(),f(a(),x)),a())
  problem:
   
  Qed