YES

Problem:
 strict:
  f(g(x)) -> x
 weak:
  a() -> h(g(f(a())))

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