YES

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

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