YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 3
  interpretation:
             [1  2  1 ]  
   [b](x0) = [-& 0  -&]x0
             [-& -& 0 ]  ,
   
             [1  1  0 ]  
   [a](x0) = [-& 0  0 ]x0
             [0  1  1 ]  
  orientation:
                [3 3 3]     [2  2  2 ]           
   a(b(a(x))) = [0 1 1]x >= [-& 0  0 ]x = b(a(x))
                [2 2 2]     [0  1  1 ]           
  problem:
   
  Qed