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

Strict Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , zero(0()) -> true()
  , zero(s(X)) -> false()
  , add(0(), X) -> X
  , add(s(X), Y) -> s(add(X, Y))
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , prod(0(), X) -> 0()
  , prod(s(X), Y) -> add(Y, prod(X, Y))
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X)
  , p(s(X)) -> X }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Arguments of following rules are not normal-forms:

{ zero(0()) -> true()
, zero(s(X)) -> false()
, add(0(), X) -> X
, add(s(X), Y) -> s(add(X, Y))
, prod(0(), X) -> 0()
, prod(s(X), Y) -> add(Y, prod(X, Y))
, p(s(X)) -> X }

All above mentioned rules can be savely removed.

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

Strict Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following dependency tuples:

Strict DPs:
  { fact^#(X) ->
    c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
  , fact^#(X) -> c_2()
  , if^#(true(), X, Y) -> c_3(activate^#(X))
  , if^#(false(), X, Y) -> c_4(activate^#(Y))
  , activate^#(X) -> c_8()
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__0()) -> c_10(0^#())
  , activate^#(n__prod(X1, X2)) ->
    c_11(prod^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__fact(X)) ->
    c_12(fact^#(activate(X)), activate^#(X))
  , activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X))
  , 0^#() -> c_5()
  , s^#(X) -> c_6()
  , prod^#(X1, X2) -> c_7()
  , p^#(X) -> c_14() }

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:
  { fact^#(X) ->
    c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
  , fact^#(X) -> c_2()
  , if^#(true(), X, Y) -> c_3(activate^#(X))
  , if^#(false(), X, Y) -> c_4(activate^#(Y))
  , activate^#(X) -> c_8()
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__0()) -> c_10(0^#())
  , activate^#(n__prod(X1, X2)) ->
    c_11(prod^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__fact(X)) ->
    c_12(fact^#(activate(X)), activate^#(X))
  , activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X))
  , 0^#() -> c_5()
  , s^#(X) -> c_6()
  , prod^#(X1, X2) -> c_7()
  , p^#(X) -> c_14() }
Weak Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {1,2,5,11,12,13,14} by
applications of Pre({1,2,5,11,12,13,14}) = {3,4,6,7,8,9,10}. Here
rules are labeled as follows:

  DPs:
    { 1: fact^#(X) ->
         c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
    , 2: fact^#(X) -> c_2()
    , 3: if^#(true(), X, Y) -> c_3(activate^#(X))
    , 4: if^#(false(), X, Y) -> c_4(activate^#(Y))
    , 5: activate^#(X) -> c_8()
    , 6: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
    , 7: activate^#(n__0()) -> c_10(0^#())
    , 8: activate^#(n__prod(X1, X2)) ->
         c_11(prod^#(activate(X1), activate(X2)),
              activate^#(X1),
              activate^#(X2))
    , 9: activate^#(n__fact(X)) ->
         c_12(fact^#(activate(X)), activate^#(X))
    , 10: activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X))
    , 11: 0^#() -> c_5()
    , 12: s^#(X) -> c_6()
    , 13: prod^#(X1, X2) -> c_7()
    , 14: p^#(X) -> c_14() }

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

Strict DPs:
  { if^#(true(), X, Y) -> c_3(activate^#(X))
  , if^#(false(), X, Y) -> c_4(activate^#(Y))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__0()) -> c_10(0^#())
  , activate^#(n__prod(X1, X2)) ->
    c_11(prod^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__fact(X)) ->
    c_12(fact^#(activate(X)), activate^#(X))
  , activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X)) }
Weak DPs:
  { fact^#(X) ->
    c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
  , fact^#(X) -> c_2()
  , activate^#(X) -> c_8()
  , 0^#() -> c_5()
  , s^#(X) -> c_6()
  , prod^#(X1, X2) -> c_7()
  , p^#(X) -> c_14() }
Weak Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

  DPs:
    { 1: if^#(true(), X, Y) -> c_3(activate^#(X))
    , 2: if^#(false(), X, Y) -> c_4(activate^#(Y))
    , 3: activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
    , 4: activate^#(n__0()) -> c_10(0^#())
    , 5: activate^#(n__prod(X1, X2)) ->
         c_11(prod^#(activate(X1), activate(X2)),
              activate^#(X1),
              activate^#(X2))
    , 6: activate^#(n__fact(X)) ->
         c_12(fact^#(activate(X)), activate^#(X))
    , 7: activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X))
    , 8: fact^#(X) ->
         c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
    , 9: fact^#(X) -> c_2()
    , 10: activate^#(X) -> c_8()
    , 11: 0^#() -> c_5()
    , 12: s^#(X) -> c_6()
    , 13: prod^#(X1, X2) -> c_7()
    , 14: p^#(X) -> c_14() }

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

Strict DPs:
  { if^#(true(), X, Y) -> c_3(activate^#(X))
  , if^#(false(), X, Y) -> c_4(activate^#(Y))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_11(prod^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__fact(X)) ->
    c_12(fact^#(activate(X)), activate^#(X))
  , activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X)) }
Weak DPs:
  { fact^#(X) ->
    c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
  , fact^#(X) -> c_2()
  , activate^#(X) -> c_8()
  , activate^#(n__0()) -> c_10(0^#())
  , 0^#() -> c_5()
  , s^#(X) -> c_6()
  , prod^#(X1, X2) -> c_7()
  , p^#(X) -> c_14() }
Weak Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

{ fact^#(X) ->
  c_1(if^#(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X)))))
, fact^#(X) -> c_2()
, activate^#(X) -> c_8()
, activate^#(n__0()) -> c_10(0^#())
, 0^#() -> c_5()
, s^#(X) -> c_6()
, prod^#(X1, X2) -> c_7()
, p^#(X) -> c_14() }

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

Strict DPs:
  { if^#(true(), X, Y) -> c_3(activate^#(X))
  , if^#(false(), X, Y) -> c_4(activate^#(Y))
  , activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_11(prod^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__fact(X)) ->
    c_12(fact^#(activate(X)), activate^#(X))
  , activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X)) }
Weak Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { activate^#(n__s(X)) -> c_9(s^#(activate(X)), activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_11(prod^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
  , activate^#(n__fact(X)) ->
    c_12(fact^#(activate(X)), activate^#(X))
  , activate^#(n__p(X)) -> c_13(p^#(activate(X)), activate^#(X)) }

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

Strict DPs:
  { if^#(true(), X, Y) -> c_1(activate^#(X))
  , if^#(false(), X, Y) -> c_2(activate^#(Y))
  , activate^#(n__s(X)) -> c_3(activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__fact(X)) -> c_5(activate^#(X))
  , activate^#(n__p(X)) -> c_6(activate^#(X)) }
Weak Trs:
  { fact(X) ->
    if(zero(X), n__s(n__0()), n__prod(X, n__fact(n__p(X))))
  , fact(X) -> n__fact(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , prod(X1, X2) -> n__prod(X1, X2)
  , activate(X) -> X
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0()
  , activate(n__prod(X1, X2)) -> prod(activate(X1), activate(X2))
  , activate(n__fact(X)) -> fact(activate(X))
  , activate(n__p(X)) -> p(activate(X))
  , p(X) -> n__p(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^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(n^1)).

Strict DPs:
  { if^#(true(), X, Y) -> c_1(activate^#(X))
  , if^#(false(), X, Y) -> c_2(activate^#(Y))
  , activate^#(n__s(X)) -> c_3(activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__fact(X)) -> c_5(activate^#(X))
  , activate^#(n__p(X)) -> c_6(activate^#(X)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Consider the dependency graph

  1: if^#(true(), X, Y) -> c_1(activate^#(X))
     -->_1 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_1 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  
  2: if^#(false(), X, Y) -> c_2(activate^#(Y))
     -->_1 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_1 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  
  3: activate^#(n__s(X)) -> c_3(activate^#(X))
     -->_1 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_1 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  
  4: activate^#(n__prod(X1, X2)) ->
     c_4(activate^#(X1), activate^#(X2))
     -->_2 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_1 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_2 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_2 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_2 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  
  5: activate^#(n__fact(X)) -> c_5(activate^#(X))
     -->_1 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_1 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  
  6: activate^#(n__p(X)) -> c_6(activate^#(X))
     -->_1 activate^#(n__p(X)) -> c_6(activate^#(X)) :6
     -->_1 activate^#(n__fact(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__prod(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  

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

  { if^#(true(), X, Y) -> c_1(activate^#(X))
  , if^#(false(), X, Y) -> c_2(activate^#(Y)) }


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

Strict DPs:
  { activate^#(n__s(X)) -> c_3(activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__fact(X)) -> c_5(activate^#(X))
  , activate^#(n__p(X)) -> c_6(activate^#(X)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 3: activate^#(n__fact(X)) -> c_5(activate^#(X))
  , 4: activate^#(n__p(X)) -> c_6(activate^#(X)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1},
    Uargs(c_6) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [n__s](x1) = [1] x1 + [0]         
                                             
    [n__prod](x1, x2) = [1] x1 + [1] x2 + [0]
                                             
        [n__fact](x1) = [1] x1 + [2]         
                                             
           [n__p](x1) = [1] x1 + [2]         
                                             
     [activate^#](x1) = [4] x1 + [0]         
                                             
            [c_3](x1) = [1] x1 + [0]         
                                             
        [c_4](x1, x2) = [1] x1 + [1] x2 + [0]
                                             
            [c_5](x1) = [1] x1 + [0]         
                                             
            [c_6](x1) = [1] x1 + [1]         
  
  The order satisfies the following ordering constraints:
  
            [activate^#(n__s(X))] =  [4] X + [0]                          
                                  >= [4] X + [0]                          
                                  =  [c_3(activate^#(X))]                 
                                                                          
    [activate^#(n__prod(X1, X2))] =  [4] X1 + [4] X2 + [0]                
                                  >= [4] X1 + [4] X2 + [0]                
                                  =  [c_4(activate^#(X1), activate^#(X2))]
                                                                          
         [activate^#(n__fact(X))] =  [4] X + [8]                          
                                  >  [4] X + [0]                          
                                  =  [c_5(activate^#(X))]                 
                                                                          
            [activate^#(n__p(X))] =  [4] X + [8]                          
                                  >  [4] X + [1]                          
                                  =  [c_6(activate^#(X))]                 
                                                                          

The strictly oriented rules are moved into the weak component.

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

Strict DPs:
  { activate^#(n__s(X)) -> c_3(activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2)) }
Weak DPs:
  { activate^#(n__fact(X)) -> c_5(activate^#(X))
  , activate^#(n__p(X)) -> c_6(activate^#(X)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.

DPs:
  { 1: activate^#(n__s(X)) -> c_3(activate^#(X))
  , 2: activate^#(n__prod(X1, X2)) ->
       c_4(activate^#(X1), activate^#(X2))
  , 3: activate^#(n__fact(X)) -> c_5(activate^#(X))
  , 4: activate^#(n__p(X)) -> c_6(activate^#(X)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1},
    Uargs(c_6) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [n__s](x1) = [1] x1 + [4]         
                                             
    [n__prod](x1, x2) = [1] x1 + [1] x2 + [4]
                                             
        [n__fact](x1) = [1] x1 + [4]         
                                             
           [n__p](x1) = [1] x1 + [4]         
                                             
     [activate^#](x1) = [2] x1 + [0]         
                                             
            [c_3](x1) = [1] x1 + [0]         
                                             
        [c_4](x1, x2) = [1] x1 + [1] x2 + [1]
                                             
            [c_5](x1) = [1] x1 + [1]         
                                             
            [c_6](x1) = [1] x1 + [0]         
  
  The order satisfies the following ordering constraints:
  
            [activate^#(n__s(X))] = [2] X + [8]                          
                                  > [2] X + [0]                          
                                  = [c_3(activate^#(X))]                 
                                                                         
    [activate^#(n__prod(X1, X2))] = [2] X1 + [2] X2 + [8]                
                                  > [2] X1 + [2] X2 + [1]                
                                  = [c_4(activate^#(X1), activate^#(X2))]
                                                                         
         [activate^#(n__fact(X))] = [2] X + [8]                          
                                  > [2] X + [1]                          
                                  = [c_5(activate^#(X))]                 
                                                                         
            [activate^#(n__p(X))] = [2] X + [8]                          
                                  > [2] X + [0]                          
                                  = [c_6(activate^#(X))]                 
                                                                         

The strictly oriented rules are moved into the weak component.

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

Weak DPs:
  { activate^#(n__s(X)) -> c_3(activate^#(X))
  , activate^#(n__prod(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__fact(X)) -> c_5(activate^#(X))
  , activate^#(n__p(X)) -> c_6(activate^#(X)) }
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.

{ activate^#(n__s(X)) -> c_3(activate^#(X))
, activate^#(n__prod(X1, X2)) ->
  c_4(activate^#(X1), activate^#(X2))
, activate^#(n__fact(X)) -> c_5(activate^#(X))
, activate^#(n__p(X)) -> c_6(activate^#(X)) }

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