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

Strict Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(app(l, cons(x, cons(y, k)))) ->
    sum(app(l, sum(cons(x, cons(y, k)))))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We add the following dependency tuples:

Strict DPs:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(app(l, cons(x, cons(y, k)))) ->
    c_4(sum^#(app(l, sum(cons(x, cons(y, k))))),
        app^#(l, sum(cons(x, cons(y, k)))),
        sum^#(cons(x, cons(y, k))))
  , sum^#(cons(x, nil())) -> c_5()
  , sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(0(), y) -> c_7()
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }

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:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(app(l, cons(x, cons(y, k)))) ->
    c_4(sum^#(app(l, sum(cons(x, cons(y, k))))),
        app^#(l, sum(cons(x, cons(y, k)))),
        sum^#(cons(x, cons(y, k))))
  , sum^#(cons(x, nil())) -> c_5()
  , sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(0(), y) -> c_7()
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(app(l, cons(x, cons(y, k)))) ->
    sum(app(l, sum(cons(x, cons(y, k)))))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

Consider the dependency graph:

  1: app^#(l, nil()) -> c_1()
  
  2: app^#(nil(), k) -> c_2()
  
  3: app^#(cons(x, l), k) -> c_3(app^#(l, k))
     -->_1 app^#(cons(x, l), k) -> c_3(app^#(l, k)) :3
     -->_1 app^#(nil(), k) -> c_2() :2
     -->_1 app^#(l, nil()) -> c_1() :1
  
  4: sum^#(app(l, cons(x, cons(y, k)))) ->
     c_4(sum^#(app(l, sum(cons(x, cons(y, k))))),
         app^#(l, sum(cons(x, cons(y, k)))),
         sum^#(cons(x, cons(y, k))))
     -->_3 sum^#(cons(x, cons(y, l))) ->
           c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6
     -->_1 sum^#(cons(x, cons(y, l))) ->
           c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6
     -->_1 sum^#(cons(x, nil())) -> c_5() :5
     -->_1 sum^#(app(l, cons(x, cons(y, k)))) ->
           c_4(sum^#(app(l, sum(cons(x, cons(y, k))))),
               app^#(l, sum(cons(x, cons(y, k)))),
               sum^#(cons(x, cons(y, k)))) :4
     -->_2 app^#(l, nil()) -> c_1() :1
  
  5: sum^#(cons(x, nil())) -> c_5()
  
  6: sum^#(cons(x, cons(y, l))) ->
     c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
     -->_2 plus^#(s(x), y) -> c_8(plus^#(x, y)) :8
     -->_2 plus^#(0(), y) -> c_7() :7
     -->_1 sum^#(cons(x, cons(y, l))) ->
           c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) :6
     -->_1 sum^#(cons(x, nil())) -> c_5() :5
  
  7: plus^#(0(), y) -> c_7()
  
  8: plus^#(s(x), y) -> c_8(plus^#(x, y))
     -->_1 plus^#(s(x), y) -> c_8(plus^#(x, y)) :8
     -->_1 plus^#(0(), y) -> c_7() :7
  

Only the nodes {1,2,3,5,6,8,7} are reachable from nodes
{1,2,3,5,6,7,8} that start derivation from marked basic terms. The
nodes not reachable are removed from the problem.

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

Strict DPs:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, nil())) -> c_5()
  , sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(0(), y) -> c_7()
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(app(l, cons(x, cons(y, k)))) ->
    sum(app(l, sum(cons(x, cons(y, k)))))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

  DPs:
    { 1: app^#(l, nil()) -> c_1()
    , 2: app^#(nil(), k) -> c_2()
    , 3: app^#(cons(x, l), k) -> c_3(app^#(l, k))
    , 4: sum^#(cons(x, nil())) -> c_5()
    , 5: sum^#(cons(x, cons(y, l))) ->
         c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
    , 6: plus^#(0(), y) -> c_7()
    , 7: plus^#(s(x), y) -> c_8(plus^#(x, y)) }

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

Strict DPs:
  { app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak DPs:
  { app^#(l, nil()) -> c_1()
  , app^#(nil(), k) -> c_2()
  , sum^#(cons(x, nil())) -> c_5()
  , plus^#(0(), y) -> c_7() }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(app(l, cons(x, cons(y, k)))) ->
    sum(app(l, sum(cons(x, cons(y, k)))))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
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.

{ app^#(l, nil()) -> c_1()
, app^#(nil(), k) -> c_2()
, sum^#(cons(x, nil())) -> c_5()
, plus^#(0(), y) -> c_7() }

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

Strict DPs:
  { app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak Trs:
  { app(l, nil()) -> l
  , app(nil(), k) -> k
  , app(cons(x, l), k) -> cons(x, app(l, k))
  , sum(app(l, cons(x, cons(y, k)))) ->
    sum(app(l, sum(cons(x, cons(y, k)))))
  , sum(cons(x, nil())) -> cons(x, nil())
  , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { plus(0(), y) -> y
    , plus(s(x), y) -> s(plus(x, y)) }

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

Strict DPs:
  { app^#(cons(x, l), k) -> c_3(app^#(l, k))
  , sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak Trs:
  { plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

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

DPs:
  { 1: app^#(cons(x, l), k) -> c_3(app^#(l, k)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_3) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_8) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
      [cons](x1, x2) = [1] x1 + [1] x2 + [1]
                                            
      [plus](x1, x2) = [4]                  
                                            
                 [0] = [0]                  
                                            
             [s](x1) = [1] x1 + [3]         
                                            
     [app^#](x1, x2) = [1] x1 + [0]         
                                            
           [c_3](x1) = [1] x1 + [0]         
                                            
         [sum^#](x1) = [0]                  
                                            
       [c_6](x1, x2) = [1] x1 + [2] x2 + [0]
                                            
    [plus^#](x1, x2) = [0]                  
                                            
           [c_8](x1) = [1] x1 + [0]         
  
  The order satisfies the following ordering constraints:
  
                  [plus(0(), y)] =  [4]                                            
                                 ?  [1] y + [0]                                    
                                 =  [y]                                            
                                                                                   
                 [plus(s(x), y)] =  [4]                                            
                                 ?  [7]                                            
                                 =  [s(plus(x, y))]                                
                                                                                   
          [app^#(cons(x, l), k)] =  [1] l + [1] x + [1]                            
                                 >  [1] l + [0]                                    
                                 =  [c_3(app^#(l, k))]                             
                                                                                   
    [sum^#(cons(x, cons(y, l)))] =  [0]                                            
                                 >= [0]                                            
                                 =  [c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))]
                                                                                   
               [plus^#(s(x), y)] =  [0]                                            
                                 >= [0]                                            
                                 =  [c_8(plus^#(x, y))]                            
                                                                                   

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

Strict DPs:
  { sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak DPs: { app^#(cons(x, l), k) -> c_3(app^#(l, k)) }
Weak Trs:
  { plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
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.

{ app^#(cons(x, l), k) -> c_3(app^#(l, k)) }

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

Strict DPs:
  { sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y))
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak Trs:
  { plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
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

  { sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) }

and lower component

  { plus^#(s(x), y) -> c_8(plus^#(x, y)) }

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

{ sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l))
, sum^#(cons(x, cons(y, l))) -> plus^#(x, y) }

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:
    { sum^#(cons(x, cons(y, l))) ->
      c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) }
  Weak Trs:
    { plus(0(), y) -> y
    , plus(s(x), y) -> s(plus(x, y)) }
  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: sum^#(cons(x, cons(y, l))) ->
         c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) }
  
  Sub-proof:
  ----------
    The input was oriented with the instance of 'Small Polynomial Path
    Order (PS,1-bounded)' as induced by the safe mapping
    
     safe(cons) = {1, 2}, safe(plus) = {}, safe(0) = {}, safe(s) = {1},
     safe(sum^#) = {}, safe(c_6) = {}, safe(plus^#) = {}
    
    and precedence
    
     empty .
    
    Following symbols are considered recursive:
    
     {sum^#}
    
    The recursion depth is 1.
    
    Further, following argument filtering is employed:
    
     pi(cons) = [1, 2], pi(plus) = 2, pi(0) = [], pi(s) = 1,
     pi(sum^#) = [1], pi(c_6) = [1, 2], pi(plus^#) = []
    
    Usable defined function symbols are a subset of:
    
     {plus, sum^#, plus^#}
    
    For your convenience, here are the satisfied ordering constraints:
    
      pi(sum^#(cons(x, cons(y, l)))) =  sum^#(cons(; x,  cons(; y,  l));)                
                                     >  c_6(sum^#(cons(; y,  l);),  plus^#();)           
                                     =  pi(c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)))
                                                                                         
                    pi(plus(0(), y)) =  y                                                
                                     >= y                                                
                                     =  pi(y)                                            
                                                                                         
                   pi(plus(s(x), y)) =  y                                                
                                     >= y                                                
                                     =  pi(s(plus(x, y)))                                
                                                                                         
  
  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:
    { sum^#(cons(x, cons(y, l))) ->
      c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) }
  Weak Trs:
    { plus(0(), y) -> y
    , plus(s(x), y) -> s(plus(x, y)) }
  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.
  
  { sum^#(cons(x, cons(y, l))) ->
    c_6(sum^#(cons(plus(x, y), l)), plus^#(x, y)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { plus(0(), y) -> y
    , plus(s(x), y) -> s(plus(x, y)) }
  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: { plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak DPs:
  { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l))
  , sum^#(cons(x, cons(y, l))) -> plus^#(x, y) }
Weak Trs:
  { plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
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: plus^#(s(x), y) -> c_8(plus^#(x, y)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_8) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
      [cons](x1, x2) = [1] x1 + [1] x2 + [0]
                                            
      [plus](x1, x2) = [1] x1 + [1] x2 + [0]
                                            
                 [0] = [0]                  
                                            
             [s](x1) = [1] x1 + [1]         
                                            
         [sum^#](x1) = [2] x1 + [0]         
                                            
    [plus^#](x1, x2) = [1] x1 + [0]         
                                            
           [c_8](x1) = [1] x1 + [0]         
  
  The order satisfies the following ordering constraints:
  
                  [plus(0(), y)] =  [1] y + [0]                 
                                 >= [1] y + [0]                 
                                 =  [y]                         
                                                                
                 [plus(s(x), y)] =  [1] x + [1] y + [1]         
                                 >= [1] x + [1] y + [1]         
                                 =  [s(plus(x, y))]             
                                                                
    [sum^#(cons(x, cons(y, l)))] =  [2] l + [2] x + [2] y + [0] 
                                 >= [2] l + [2] x + [2] y + [0] 
                                 =  [sum^#(cons(plus(x, y), l))]
                                                                
    [sum^#(cons(x, cons(y, l)))] =  [2] l + [2] x + [2] y + [0] 
                                 >= [1] x + [0]                 
                                 =  [plus^#(x, y)]              
                                                                
               [plus^#(s(x), y)] =  [1] x + [1]                 
                                 >  [1] x + [0]                 
                                 =  [c_8(plus^#(x, y))]         
                                                                

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:
  { sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l))
  , sum^#(cons(x, cons(y, l))) -> plus^#(x, y)
  , plus^#(s(x), y) -> c_8(plus^#(x, y)) }
Weak Trs:
  { plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
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.

{ sum^#(cons(x, cons(y, l))) -> sum^#(cons(plus(x, y), l))
, sum^#(cons(x, cons(y, l))) -> plus^#(x, y)
, plus^#(s(x), y) -> c_8(plus^#(x, y)) }

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

Weak Trs:
  { plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y)) }
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))