YES

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

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