YES(?,O(n^2))

Problem:
 a(b(x)) -> b(a(x))
 a(c(x)) -> x

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 2]     [11]
   [c](x0) = [0 1]x0 + [2 ],
   
             [1 2]     [0 ]
   [a](x0) = [0 1]x0 + [12],
   
                  [1]
   [b](x0) = x0 + [1]
  orientation:
             [1 2]    [3 ]    [1 2]    [1 ]          
   a(b(x)) = [0 1]x + [13] >= [0 1]x + [13] = b(a(x))
   
             [1 4]    [15]         
   a(c(x)) = [0 1]x + [14] >= x = x
  problem:
   
  Qed