YES

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

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