YES

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

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