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

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

Strict Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> naiverev(xs) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add the following dependency tuples:

Strict DPs:
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
  , naiverev^#(Nil()) -> c_2()
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
  , app^#(Nil(), ys) -> c_4()
  , notEmpty^#(Cons(x, xs)) -> c_5()
  , notEmpty^#(Nil()) -> c_6()
  , goal^#(xs) -> c_7(naiverev^#(xs)) }

and mark the set of starting terms.

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

Strict DPs:
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
  , naiverev^#(Nil()) -> c_2()
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
  , app^#(Nil(), ys) -> c_4()
  , notEmpty^#(Cons(x, xs)) -> c_5()
  , notEmpty^#(Nil()) -> c_6()
  , goal^#(xs) -> c_7(naiverev^#(xs)) }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> naiverev(xs) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

  DPs:
    { 1: naiverev^#(Cons(x, xs)) ->
         c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
    , 2: naiverev^#(Nil()) -> c_2()
    , 3: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
    , 4: app^#(Nil(), ys) -> c_4()
    , 5: notEmpty^#(Cons(x, xs)) -> c_5()
    , 6: notEmpty^#(Nil()) -> c_6()
    , 7: goal^#(xs) -> c_7(naiverev^#(xs)) }

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

Strict DPs:
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
  , goal^#(xs) -> c_7(naiverev^#(xs)) }
Weak DPs:
  { naiverev^#(Nil()) -> c_2()
  , app^#(Nil(), ys) -> c_4()
  , notEmpty^#(Cons(x, xs)) -> c_5()
  , notEmpty^#(Nil()) -> c_6() }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> naiverev(xs) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

{ naiverev^#(Nil()) -> c_2()
, app^#(Nil(), ys) -> c_4()
, notEmpty^#(Cons(x, xs)) -> c_5()
, notEmpty^#(Nil()) -> c_6() }

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

Strict DPs:
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
  , goal^#(xs) -> c_7(naiverev^#(xs)) }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> naiverev(xs) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

Consider the dependency graph

  1: naiverev^#(Cons(x, xs)) ->
     c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
     -->_1 app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) :2
     -->_2 naiverev^#(Cons(x, xs)) ->
           c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) :1
  
  2: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
     -->_1 app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) :2
  
  3: goal^#(xs) -> c_7(naiverev^#(xs))
     -->_1 naiverev^#(Cons(x, xs)) ->
           c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) :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).

  { goal^#(xs) -> c_7(naiverev^#(xs)) }


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

Strict DPs:
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , goal(xs) -> naiverev(xs) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
    , naiverev(Nil()) -> Nil()
    , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
    , app(Nil(), ys) -> ys }

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

Strict DPs:
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs))
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We decompose the input problem according to the dependency graph
into the upper component

  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) }

and lower component

  { app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }

Further, following extension rules are added to the lower
component.

{ naiverev^#(Cons(x, xs)) -> naiverev^#(xs)
, naiverev^#(Cons(x, xs)) -> app^#(naiverev(xs), Cons(x, Nil())) }

TcT solves the upper component with certificate YES(O(1),O(n^1)).

Sub-proof:
----------
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { naiverev^#(Cons(x, xs)) ->
      c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) }
  Weak Trs:
    { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
    , naiverev(Nil()) -> Nil()
    , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
    , app(Nil(), ys) -> ys }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
  to orient following rules strictly.
  
  DPs:
    { 1: naiverev^#(Cons(x, xs)) ->
         c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) }
  Trs:
    { naiverev(Nil()) -> Nil()
    , app(Nil(), ys) -> ys }
  
  Sub-proof:
  ----------
    The input was oriented with the instance of 'Small Polynomial Path
    Order (PS,1-bounded)' as induced by the safe mapping
    
     safe(naiverev) = {}, safe(Cons) = {1, 2}, safe(app) = {},
     safe(Nil) = {}, safe(notEmpty) = {}, safe(True) = {},
     safe(False) = {}, safe(goal) = {}, safe(naiverev^#) = {},
     safe(c_1) = {}, safe(app^#) = {}, safe(c_2) = {}, safe(c_3) = {},
     safe(c_4) = {}, safe(notEmpty^#) = {}, safe(c_5) = {},
     safe(c_6) = {}, safe(goal^#) = {}, safe(c_7) = {}
    
    and precedence
    
     naiverev > app, naiverev^# > app .
    
    Following symbols are considered recursive:
    
     {naiverev^#}
    
    The recursion depth is 1.
    
    Further, following argument filtering is employed:
    
     pi(naiverev) = [], pi(Cons) = [2], pi(app) = [2], pi(Nil) = [],
     pi(notEmpty) = [], pi(True) = [], pi(False) = [], pi(goal) = [],
     pi(naiverev^#) = [1], pi(c_1) = [1, 2], pi(app^#) = [],
     pi(c_2) = [], pi(c_3) = [], pi(c_4) = [], pi(notEmpty^#) = [],
     pi(c_5) = [], pi(c_6) = [], pi(goal^#) = [], pi(c_7) = []
    
    Usable defined function symbols are a subset of:
    
     {naiverev^#, app^#, notEmpty^#, goal^#}
    
    For your convenience, here are the satisfied ordering constraints:
    
      pi(naiverev^#(Cons(x, xs))) = naiverev^#(Cons(; xs);)                                     
                                  > c_1(app^#(),  naiverev^#(xs;);)                             
                                  = pi(c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)))
                                                                                                
  
  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:
    { naiverev^#(Cons(x, xs)) ->
      c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) }
  Weak Trs:
    { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
    , naiverev(Nil()) -> Nil()
    , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
    , app(Nil(), ys) -> ys }
  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.
  
  { naiverev^#(Cons(x, xs)) ->
    c_1(app^#(naiverev(xs), Cons(x, Nil())), naiverev^#(xs)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
    , naiverev(Nil()) -> Nil()
    , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
    , app(Nil(), ys) -> ys }
  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

We return to the main proof.

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

Strict DPs: { app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
Weak DPs:
  { naiverev^#(Cons(x, xs)) -> naiverev^#(xs)
  , naiverev^#(Cons(x, xs)) -> app^#(naiverev(xs), Cons(x, Nil())) }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys }
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: app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys))
  , 2: naiverev^#(Cons(x, xs)) -> naiverev^#(xs)
  , 3: naiverev^#(Cons(x, xs)) ->
       app^#(naiverev(xs), Cons(x, Nil())) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
      [naiverev](x1) = [1] x1 + [0]         
                                            
      [Cons](x1, x2) = [1] x1 + [1] x2 + [1]
                                            
       [app](x1, x2) = [1] x1 + [1] x2 + [0]
                                            
               [Nil] = [0]                  
                                            
      [notEmpty](x1) = [7] x1 + [0]         
                                            
              [True] = [0]                  
                                            
             [False] = [0]                  
                                            
          [goal](x1) = [7] x1 + [0]         
                                            
    [naiverev^#](x1) = [4] x1 + [1]         
                                            
       [c_1](x1, x2) = [7] x1 + [7] x2 + [0]
                                            
     [app^#](x1, x2) = [4] x1 + [0]         
                                            
               [c_2] = [0]                  
                                            
           [c_3](x1) = [1] x1 + [1]         
                                            
               [c_4] = [0]                  
                                            
    [notEmpty^#](x1) = [7] x1 + [0]         
                                            
               [c_5] = [0]                  
                                            
               [c_6] = [0]                  
                                            
        [goal^#](x1) = [7] x1 + [0]         
                                            
           [c_7](x1) = [7] x1 + [0]         
  
  The following symbols are considered usable
  
    {naiverev, app, naiverev^#, app^#}
  
  The order satisfies the following ordering constraints:
  
      [naiverev(Cons(x, xs))] =  [1] x + [1] xs + [1]                 
                              >= [1] x + [1] xs + [1]                 
                              =  [app(naiverev(xs), Cons(x, Nil()))]  
                                                                      
            [naiverev(Nil())] =  [0]                                  
                              >= [0]                                  
                              =  [Nil()]                              
                                                                      
       [app(Cons(x, xs), ys)] =  [1] x + [1] xs + [1] ys + [1]        
                              >= [1] x + [1] xs + [1] ys + [1]        
                              =  [Cons(x, app(xs, ys))]               
                                                                      
             [app(Nil(), ys)] =  [1] ys + [0]                         
                              >= [1] ys + [0]                         
                              =  [ys]                                 
                                                                      
    [naiverev^#(Cons(x, xs))] =  [4] x + [4] xs + [5]                 
                              >  [4] xs + [1]                         
                              =  [naiverev^#(xs)]                     
                                                                      
    [naiverev^#(Cons(x, xs))] =  [4] x + [4] xs + [5]                 
                              >  [4] xs + [0]                         
                              =  [app^#(naiverev(xs), Cons(x, Nil()))]
                                                                      
     [app^#(Cons(x, xs), ys)] =  [4] x + [4] xs + [4]                 
                              >  [4] xs + [1]                         
                              =  [c_3(app^#(xs, ys))]                 
                                                                      

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:
  { naiverev^#(Cons(x, xs)) -> naiverev^#(xs)
  , naiverev^#(Cons(x, xs)) -> app^#(naiverev(xs), Cons(x, Nil()))
  , app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }
Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys }
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.

{ naiverev^#(Cons(x, xs)) -> naiverev^#(xs)
, naiverev^#(Cons(x, xs)) -> app^#(naiverev(xs), Cons(x, Nil()))
, app^#(Cons(x, xs), ys) -> c_3(app^#(xs, ys)) }

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

Weak Trs:
  { naiverev(Cons(x, xs)) -> app(naiverev(xs), Cons(x, Nil()))
  , naiverev(Nil()) -> Nil()
  , app(Cons(x, xs), ys) -> Cons(x, app(xs, ys))
  , app(Nil(), ys) -> ys }
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^2))