YES(?,O(n^3))

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

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