We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a())))
  , a() -> n__a()
  , g(X) -> n__g(X)
  , activate(X) -> X
  , activate(n__f(X)) -> f(X)
  , activate(n__a()) -> a()
  , activate(n__g(X)) -> g(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following weak dependency pairs:

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
  , a^#() -> c_3()
  , g^#(X) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__f(X)) -> c_6(f^#(X))
  , activate^#(n__a()) -> c_7(a^#())
  , activate^#(n__g(X)) -> c_8(g^#(X)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
  , a^#() -> c_3()
  , g^#(X) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__f(X)) -> c_6(f^#(X))
  , activate^#(n__a()) -> c_7(a^#())
  , activate^#(n__g(X)) -> c_8(g^#(X)) }
Strict Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a())))
  , a() -> n__a()
  , g(X) -> n__g(X)
  , activate(X) -> X
  , activate(n__f(X)) -> f(X)
  , activate(n__a()) -> a()
  , activate(n__g(X)) -> g(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { f(X) -> n__f(X)
    , f(n__f(n__a())) -> f(n__g(f(n__a()))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
  , a^#() -> c_3()
  , g^#(X) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__f(X)) -> c_6(f^#(X))
  , activate^#(n__a()) -> c_7(a^#())
  , activate^#(n__g(X)) -> c_8(g^#(X)) }
Strict Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(f) = {1}, Uargs(n__g) = {1}, Uargs(f^#) = {1},
  Uargs(c_2) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1},
  Uargs(c_8) = {1}

TcT has computed the following constructor-restricted matrix
interpretation.

           [f](x1) = [1 2] x1 + [2]
                     [0 0]      [1]
                                   
        [n__f](x1) = [1 1] x1 + [1]
                     [0 0]      [1]
                                   
            [n__a] = [0]           
                     [0]           
                                   
        [n__g](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
         [f^#](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
             [c_1] = [0]           
                     [0]           
                                   
         [c_2](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
             [a^#] = [1]           
                     [1]           
                                   
             [c_3] = [0]           
                     [0]           
                                   
         [g^#](x1) = [1]           
                     [1]           
                                   
             [c_4] = [0]           
                     [0]           
                                   
  [activate^#](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
             [c_5] = [0]           
                     [0]           
                                   
         [c_6](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
         [c_7](x1) = [1 0] x1 + [1]
                     [0 1]      [1]
                                   
         [c_8](x1) = [1 0] x1 + [1]
                     [0 1]      [1]

The order satisfies the following ordering constraints:

                 [f(X)] =  [1 2] X + [2]              
                           [0 0]     [1]              
                        >  [1 1] X + [1]              
                           [0 0]     [1]              
                        =  [n__f(X)]                  
                                                      
      [f(n__f(n__a()))] =  [5]                        
                           [1]                        
                        >  [4]                        
                           [1]                        
                        =  [f(n__g(f(n__a())))]       
                                                      
               [f^#(X)] =  [1 0] X + [0]              
                           [0 0]     [0]              
                        >= [0]                        
                           [0]                        
                        =  [c_1()]                    
                                                      
    [f^#(n__f(n__a()))] =  [1]                        
                           [0]                        
                        ?  [2]                        
                           [0]                        
                        =  [c_2(f^#(n__g(f(n__a()))))]
                                                      
                [a^#()] =  [1]                        
                           [1]                        
                        >  [0]                        
                           [0]                        
                        =  [c_3()]                    
                                                      
               [g^#(X)] =  [1]                        
                           [1]                        
                        >  [0]                        
                           [0]                        
                        =  [c_4()]                    
                                                      
        [activate^#(X)] =  [1 0] X + [0]              
                           [0 0]     [0]              
                        >= [0]                        
                           [0]                        
                        =  [c_5()]                    
                                                      
  [activate^#(n__f(X))] =  [1 1] X + [1]              
                           [0 0]     [0]              
                        >  [1 0] X + [0]              
                           [0 0]     [0]              
                        =  [c_6(f^#(X))]              
                                                      
   [activate^#(n__a())] =  [0]                        
                           [0]                        
                        ?  [2]                        
                           [2]                        
                        =  [c_7(a^#())]               
                                                      
  [activate^#(n__g(X))] =  [1 0] X + [0]              
                           [0 0]     [0]              
                        ?  [2]                        
                           [2]                        
                        =  [c_8(g^#(X))]              
                                                      

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
  , activate^#(X) -> c_5()
  , activate^#(n__a()) -> c_7(a^#())
  , activate^#(n__g(X)) -> c_8(g^#(X)) }
Weak DPs:
  { a^#() -> c_3()
  , g^#(X) -> c_4()
  , activate^#(n__f(X)) -> c_6(f^#(X)) }
Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {3,4,5} by applications of
Pre({3,4,5}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: f^#(X) -> c_1()
    , 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
    , 3: activate^#(X) -> c_5()
    , 4: activate^#(n__a()) -> c_7(a^#())
    , 5: activate^#(n__g(X)) -> c_8(g^#(X))
    , 6: a^#() -> c_3()
    , 7: g^#(X) -> c_4()
    , 8: activate^#(n__f(X)) -> c_6(f^#(X)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak DPs:
  { a^#() -> c_3()
  , g^#(X) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__f(X)) -> c_6(f^#(X))
  , activate^#(n__a()) -> c_7(a^#())
  , activate^#(n__g(X)) -> c_8(g^#(X)) }
Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak DPs: { activate^#(n__f(X)) -> c_6(f^#(X)) }
Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Consider the dependency graph

  1: f^#(X) -> c_1()
  
  2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
     -->_1 f^#(X) -> c_1() :1
  
  3: activate^#(n__f(X)) -> c_6(f^#(X))
     -->_1 f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) :2
     -->_1 f^#(X) -> c_1() :1
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { activate^#(n__f(X)) -> c_6(f^#(X)) }


We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {1} by applications of
Pre({1}) = {2}. Here rules are labeled as follows:

  DPs:
    { 1: f^#(X) -> c_1()
    , 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs: { f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak DPs: { f^#(X) -> c_1() }
Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {1} by applications of
Pre({1}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
    , 2: f^#(X) -> c_1() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs:
  { f^#(X) -> c_1()
  , f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { f(X) -> n__f(X)
  , f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))