YES

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

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