YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 0]     [1]
   [c](x0) = [0 0]x0 + [0],
   
             [1 8]     [0]
   [a](x0) = [0 1]x0 + [1],
   
             [1 2]     [15]
   [b](x0) = [0 1]x0 + [2 ]
  orientation:
              [1  10]     [31]    [1  10]     [17]           
   a(b(x1)) = [0  1 ]x1 + [3 ] >= [0  1 ]x1 + [3 ] = b(a(x1))
   
              [1  10]     [17]    [1 2]     [16]              
   b(a(x1)) = [0  1 ]x1 + [3 ] >= [0 0]x1 + [1 ] = a(c(b(x1)))
  problem:
   
  Qed