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

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

Arguments of following rules are not normal-forms:

{ p(0()) -> 0()
, p(s(X)) -> X
, leq(0(), Y) -> true()
, leq(s(X), 0()) -> false()
, leq(s(X), s(Y)) -> leq(X, Y) }

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:
  { p(X) -> n__p(X)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2))
  , activate(n__p(X)) -> p(activate(X))
  , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))
  , diff(X1, X2) -> n__diff(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following dependency tuples:

Strict DPs:
  { p^#(X) -> c_1()
  , 0^#() -> c_2()
  , s^#(X) -> c_3()
  , if^#(true(), X, Y) -> c_4(activate^#(X))
  , if^#(false(), X, Y) -> c_5(activate^#(Y))
  , activate^#(X) -> c_6()
  , activate^#(n__0()) -> c_7(0^#())
  , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X))
  , activate^#(n__diff(X1, X2)) ->
    c_9(diff^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X))
  , diff^#(X, Y) ->
    c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))))
  , diff^#(X1, X2) -> c_12() }

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

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

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

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

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

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

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_4(activate^#(X))
  , if^#(false(), X, Y) -> c_5(activate^#(Y))
  , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X))
  , activate^#(n__diff(X1, X2)) ->
    c_9(diff^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) }
Weak DPs:
  { p^#(X) -> c_1()
  , 0^#() -> c_2()
  , s^#(X) -> c_3()
  , activate^#(X) -> c_6()
  , activate^#(n__0()) -> c_7(0^#())
  , diff^#(X, Y) ->
    c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))))
  , diff^#(X1, X2) -> c_12() }
Weak Trs:
  { p(X) -> n__p(X)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2))
  , activate(n__p(X)) -> p(activate(X))
  , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))
  , diff(X1, X2) -> n__diff(X1, X2) }
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.

{ p^#(X) -> c_1()
, 0^#() -> c_2()
, s^#(X) -> c_3()
, activate^#(X) -> c_6()
, activate^#(n__0()) -> c_7(0^#())
, diff^#(X, Y) ->
  c_11(if^#(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y))))
, diff^#(X1, X2) -> c_12() }

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_4(activate^#(X))
  , if^#(false(), X, Y) -> c_5(activate^#(Y))
  , activate^#(n__s(X)) -> c_8(s^#(activate(X)), activate^#(X))
  , activate^#(n__diff(X1, X2)) ->
    c_9(diff^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , activate^#(n__p(X)) -> c_10(p^#(activate(X)), activate^#(X)) }
Weak Trs:
  { p(X) -> n__p(X)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2))
  , activate(n__p(X)) -> p(activate(X))
  , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))
  , diff(X1, X2) -> n__diff(X1, X2) }
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_8(s^#(activate(X)), activate^#(X))
  , activate^#(n__diff(X1, X2)) ->
    c_9(diff^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , activate^#(n__p(X)) -> c_10(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__diff(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__p(X)) -> c_5(activate^#(X)) }
Weak Trs:
  { p(X) -> n__p(X)
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y)
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__diff(X1, X2)) -> diff(activate(X1), activate(X2))
  , activate(n__p(X)) -> p(activate(X))
  , diff(X, Y) -> if(leq(X, Y), n__0(), n__s(n__diff(n__p(X), Y)))
  , diff(X1, X2) -> n__diff(X1, X2) }
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__diff(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__p(X)) -> c_5(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_5(activate^#(X)) :5
     -->_1 activate^#(n__diff(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_5(activate^#(X)) :5
     -->_1 activate^#(n__diff(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_5(activate^#(X)) :5
     -->_1 activate^#(n__diff(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__s(X)) -> c_3(activate^#(X)) :3
  
  4: activate^#(n__diff(X1, X2)) ->
     c_4(activate^#(X1), activate^#(X2))
     -->_2 activate^#(n__p(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5
     -->_2 activate^#(n__diff(X1, X2)) ->
           c_4(activate^#(X1), activate^#(X2)) :4
     -->_1 activate^#(n__diff(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__p(X)) -> c_5(activate^#(X))
     -->_1 activate^#(n__p(X)) -> c_5(activate^#(X)) :5
     -->_1 activate^#(n__diff(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__diff(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__p(X)) -> c_5(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__p(X)) -> c_5(activate^#(X)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [n__s](x1) = [1] x1 + [0]         
                                             
    [n__diff](x1, x2) = [1] x1 + [1] x2 + [0]
                                             
           [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 + [1]         
  
  The order satisfies the following ordering constraints:
  
            [activate^#(n__s(X))] =  [4] X + [0]                          
                                  >= [4] X + [0]                          
                                  =  [c_3(activate^#(X))]                 
                                                                          
    [activate^#(n__diff(X1, X2))] =  [4] X1 + [4] X2 + [0]                
                                  >= [4] X1 + [4] X2 + [0]                
                                  =  [c_4(activate^#(X1), activate^#(X2))]
                                                                          
            [activate^#(n__p(X))] =  [4] X + [8]                          
                                  >  [4] X + [1]                          
                                  =  [c_5(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__diff(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2)) }
Weak DPs: { activate^#(n__p(X)) -> c_5(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:
  { 2: activate^#(n__diff(X1, X2)) ->
       c_4(activate^#(X1), activate^#(X2))
  , 3: activate^#(n__p(X)) -> c_5(activate^#(X)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
           [n__s](x1) = [1] x1 + [0]         
                                             
    [n__diff](x1, x2) = [1] x1 + [1] x2 + [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 + [1]
                                             
            [c_5](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__diff(X1, X2))] =  [4] X1 + [4] X2 + [8]                
                                  >  [4] X1 + [4] X2 + [1]                
                                  =  [c_4(activate^#(X1), activate^#(X2))]
                                                                          
            [activate^#(n__p(X))] =  [4] X + [8]                          
                                  >  [4] X + [1]                          
                                  =  [c_5(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)) }
Weak DPs:
  { activate^#(n__diff(X1, X2)) ->
    c_4(activate^#(X1), activate^#(X2))
  , activate^#(n__p(X)) -> c_5(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__diff(X1, X2)) ->
       c_4(activate^#(X1), activate^#(X2))
  , 3: activate^#(n__p(X)) -> c_5(activate^#(X)) }

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