YES

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

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