TRS:
 {  f(n__f(n__a())) -> f(n__g(n__f(n__a()))),
               f(X) -> n__f(X),
                a() -> n__a(),
               g(X) -> n__g(X),
  activate(n__f(X)) -> f(X),
   activate(n__a()) -> a(),
  activate(n__g(X)) -> g(activate(X)),
        activate(X) -> X}
 POP* + Boolean Semantic Labelling:
  Normal positions:
  pi(activate_sl=1) = [1], pi(g_sl=1) = [1]
  
Safe positions:
   pi(activate_sl=0) = [1], pi(g_sl=0) = [1], pi(n__f_sl=1) = [1], pi(n__f_sl=0) = [1], pi(n__g_sl=1) = [1], pi(n__g_sl=0) = [1], pi(f_sl=1) = [1], pi(f_sl=0) = [1]
  
Precedence:
   activate_sl=0 > f_sl=0, 
   activate_sl=0 > f_sl=1, 
   activate_sl=0 > a_sl=0, 
   a_sl=0 > n__a_sl=1, 
   f_sl=1 > n__f_sl=1, 
   f_sl=0 > f_sl=1, 
   f_sl=0 > n__g_sl=0, 
   f_sl=0 > n__f_sl=0, 
   f_sl=0 > n__a_sl=1, 
   g_sl=0 > n__g_sl=0, 
   activate_sl=1 > activate_sl=0, 
   activate_sl=1 > g_sl=0
   empty
  
Interpretation:
   f^(1):
   0 | 0
   1 | 0
   n__g^(1):
   0 | 1
   1 | 1
   n__f^(1):
   0 | 0
   1 | 0
   n__a^(0):
    | 0
   a^(0):
    | 0
   g^(1):
   0 | 1
   1 | 1
   activate^(1):
   0 | 0
   1 | 1
   
  
Labelling:
   f^(1):
   0 | 0
   1 | 1
   n__g^(1):
   0 | 0
   1 | 0
   n__f^(1):
   0 | 0
   1 | 1
   n__a^(0):
    | 1
   a^(0):
    | 0
   g^(1):
   0 | 0
   1 | 0
   activate^(1):
   0 | 0
   1 | 1
   
  
Labelled predicative System:
   {f_sl=0(;n__f_sl=0(;n__a_sl=1())) -> f_sl=1(;n__g_sl=0(;n__f_sl=0(;n__a_sl=1()))),
                          f_sl=0(;X) -> n__f_sl=0(;X),
                          f_sl=1(;X) -> n__f_sl=1(;X),
                            a_sl=0() -> n__a_sl=1(),
                          g_sl=0(;X) -> n__g_sl=0(;X),
                          g_sl=0(;X) -> n__g_sl=0(;X),
       activate_sl=0(;n__f_sl=0(;X)) -> f_sl=0(;X),
       activate_sl=0(;n__f_sl=1(;X)) -> f_sl=1(;X),
         activate_sl=0(;n__a_sl=1()) -> a_sl=0(),
       activate_sl=1(n__g_sl=0(;X);) -> g_sl=0(;activate_sl=0(;X)),
       activate_sl=1(n__g_sl=0(;X);) -> g_sl=0(;activate_sl=1(X;)),
                   activate_sl=0(;X) -> X,
                   activate_sl=1(X;) -> X}
  

  Qed