YES(O(1),O(n^1))

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 innermost 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 + [1]
                     [0 0]      [2]
                                   
        [n__f](x1) = [1 0] x1 + [0]
                     [0 0]      [2]
                                   
            [n__a] = [0]           
                     [0]           
                                   
        [n__g](x1) = [1 0] x1 + [0]
                     [0 0]      [0]
                                   
         [f^#](x1) = [2 0] x1 + [2]
                     [0 0]      [2]
                                   
             [c_1] = [1]           
                     [1]           
                                   
         [c_2](x1) = [1 0] x1 + [2]
                     [0 1]      [2]
                                   
             [a^#] = [1]           
                     [1]           
                                   
             [c_3] = [1]           
                     [1]           
                                   
         [g^#](x1) = [1 0] x1 + [1]
                     [2 1]      [1]
                                   
             [c_4] = [1]           
                     [1]           
                                   
  [activate^#](x1) = [2 0] x1 + [0]
                     [0 0]      [0]
                                   
             [c_5] = [1]           
                     [1]           
                                   
         [c_6](x1) = [1 0] x1 + [1]
                     [0 1]      [1]
                                   
         [c_7](x1) = [1 0] x1 + [2]
                     [0 1]      [2]
                                   
         [c_8](x1) = [1 0] x1 + [2]
                     [0 1]      [2]

The following symbols are considered usable

  {f, f^#, a^#, g^#, activate^#}

The order satisfies the following ordering constraints:

                 [f(X)] =  [1 2] X + [1]              
                           [0 0]     [2]              
                        >  [1 0] X + [0]              
                           [0 0]     [2]              
                        =  [n__f(X)]                  
                                                      
      [f(n__f(n__a()))] =  [5]                        
                           [2]                        
                        >  [2]                        
                           [2]                        
                        =  [f(n__g(f(n__a())))]       
                                                      
               [f^#(X)] =  [2 0] X + [2]              
                           [0 0]     [2]              
                        >  [1]                        
                           [1]                        
                        =  [c_1()]                    
                                                      
    [f^#(n__f(n__a()))] =  [2]                        
                           [2]                        
                        ?  [6]                        
                           [4]                        
                        =  [c_2(f^#(n__g(f(n__a()))))]
                                                      
                [a^#()] =  [1]                        
                           [1]                        
                        >= [1]                        
                           [1]                        
                        =  [c_3()]                    
                                                      
               [g^#(X)] =  [1 0] X + [1]              
                           [2 1]     [1]              
                        >= [1]                        
                           [1]                        
                        =  [c_4()]                    
                                                      
        [activate^#(X)] =  [2 0] X + [0]              
                           [0 0]     [0]              
                        ?  [1]                        
                           [1]                        
                        =  [c_5()]                    
                                                      
  [activate^#(n__f(X))] =  [2 0] X + [0]              
                           [0 0]     [0]              
                        ?  [2 0] X + [3]              
                           [0 0]     [3]              
                        =  [c_6(f^#(X))]              
                                                      
   [activate^#(n__a())] =  [0]                        
                           [0]                        
                        ?  [3]                        
                           [3]                        
                        =  [c_7(a^#())]               
                                                      
  [activate^#(n__g(X))] =  [2 0] X + [0]              
                           [0 0]     [0]              
                        ?  [1 0] X + [3]              
                           [2 1]     [3]              
                        =  [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^#(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)) }
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,2,3,4} by applications
of Pre({1,2,3,4}) = {5,6,7}. Here rules are labeled as follows:

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

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

Strict DPs:
  { activate^#(n__f(X)) -> c_6(f^#(X))
  , activate^#(n__a()) -> c_7(a^#())
  , activate^#(n__g(X)) -> c_8(g^#(X)) }
Weak 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() }
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,2,3} by applications of
Pre({1,2,3}) = {}. Here rules are labeled as follows:

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

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()))))
  , 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.

{ 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)) }

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))