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

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

Strict Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We add the following dependency tuples:

Strict DPs:
  { minus^#(x, 0()) -> c_1()
  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(0(), s(y)) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(nil(), y) -> c_5()
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(nil()) -> c_7()
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(nil()) -> c_9()
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(leaf(), y) -> c_11()
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(x, leaf()) -> c_13()
  , less_leaves^#(leaf(), cons(w, z)) -> c_14()
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }

and mark the set of starting terms.

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

Strict DPs:
  { minus^#(x, 0()) -> c_1()
  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(0(), s(y)) -> c_3()
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(nil(), y) -> c_5()
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(nil()) -> c_7()
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(nil()) -> c_9()
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(leaf(), y) -> c_11()
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(x, leaf()) -> c_13()
  , less_leaves^#(leaf(), cons(w, z)) -> c_14()
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

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

  DPs:
    { 1: minus^#(x, 0()) -> c_1()
    , 2: minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
    , 3: quot^#(0(), s(y)) -> c_3()
    , 4: quot^#(s(x), s(y)) ->
         c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , 5: app^#(nil(), y) -> c_5()
    , 6: app^#(add(n, x), y) -> c_6(app^#(x, y))
    , 7: reverse^#(nil()) -> c_7()
    , 8: reverse^#(add(n, x)) ->
         c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
    , 9: shuffle^#(nil()) -> c_9()
    , 10: shuffle^#(add(n, x)) ->
          c_10(shuffle^#(reverse(x)), reverse^#(x))
    , 11: concat^#(leaf(), y) -> c_11()
    , 12: concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
    , 13: less_leaves^#(x, leaf()) -> c_13()
    , 14: less_leaves^#(leaf(), cons(w, z)) -> c_14()
    , 15: less_leaves^#(cons(u, v), cons(w, z)) ->
          c_15(less_leaves^#(concat(u, v), concat(w, z)),
               concat^#(u, v),
               concat^#(w, z)) }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak DPs:
  { minus^#(x, 0()) -> c_1()
  , quot^#(0(), s(y)) -> c_3()
  , app^#(nil(), y) -> c_5()
  , reverse^#(nil()) -> c_7()
  , shuffle^#(nil()) -> c_9()
  , concat^#(leaf(), y) -> c_11()
  , less_leaves^#(x, leaf()) -> c_13()
  , less_leaves^#(leaf(), cons(w, z)) -> c_14() }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

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

{ minus^#(x, 0()) -> c_1()
, quot^#(0(), s(y)) -> c_3()
, app^#(nil(), y) -> c_5()
, reverse^#(nil()) -> c_7()
, shuffle^#(nil()) -> c_9()
, concat^#(leaf(), y) -> c_11()
, less_leaves^#(x, leaf()) -> c_13()
, less_leaves^#(leaf(), cons(w, z)) -> c_14() }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , quot(0(), s(y)) -> 0()
  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , shuffle(nil()) -> nil()
  , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y))
  , less_leaves(x, leaf()) -> false()
  , less_leaves(leaf(), cons(w, z)) -> true()
  , less_leaves(cons(u, v), cons(w, z)) ->
    less_leaves(concat(u, v), concat(w, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
    , concat(leaf(), y) -> y
    , concat(cons(u, v), y) -> cons(u, concat(v, y)) }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> c_10(shuffle^#(reverse(x)), reverse^#(x))
  , concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

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

DPs:
  { 6: concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , 7: less_leaves^#(cons(u, v), cons(w, z)) ->
       c_15(less_leaves^#(concat(u, v), concat(w, z)),
            concat^#(u, v),
            concat^#(w, z)) }
Trs:
  { minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_2) = {1}, Uargs(c_4) = {1, 2}, Uargs(c_6) = {1},
    Uargs(c_8) = {1, 2}, Uargs(c_10) = {1, 2}, Uargs(c_12) = {1},
    Uargs(c_15) = {1, 2, 3}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA) and not(IDA(1)).
  
            [minus](x1, x2) = [1 1] x1 + [0 0] x2 + [0]           
                              [2 2]      [0 4]      [0]           
                                                                  
                        [0] = [0]                                 
                              [0]                                 
                                                                  
                    [s](x1) = [0 0] x1 + [4]                      
                              [1 1]      [0]                      
                                                                  
             [quot](x1, x2) = [7 7] x1 + [7 7] x2 + [0]           
                              [0 0]      [0 0]      [0]           
                                                                  
              [app](x1, x2) = [2 0] x2 + [1]                      
                              [0 1]      [0]                      
                                                                  
                      [nil] = [0]                                 
                              [0]                                 
                                                                  
              [add](x1, x2) = [1]                                 
                              [0]                                 
                                                                  
              [reverse](x1) = [4]                                 
                              [0]                                 
                                                                  
              [shuffle](x1) = [7 7] x1 + [0]                      
                              [0 0]      [0]                      
                                                                  
           [concat](x1, x2) = [1 0] x1 + [1 0] x2 + [0]           
                              [2 0]      [0 4]      [4]           
                                                                  
                     [leaf] = [0]                                 
                              [0]                                 
                                                                  
             [cons](x1, x2) = [1 1] x1 + [1 0] x2 + [2]           
                              [0 0]      [0 1]      [4]           
                                                                  
      [less_leaves](x1, x2) = [7 7] x1 + [7 7] x2 + [0]           
                              [0 0]      [0 0]      [0]           
                                                                  
                    [false] = [0]                                 
                              [0]                                 
                                                                  
                     [true] = [0]                                 
                              [0]                                 
                                                                  
          [minus^#](x1, x2) = [0 0] x1 + [0 0] x2 + [0]           
                              [0 4]      [0 4]      [4]           
                                                                  
                      [c_1] = [0]                                 
                              [0]                                 
                                                                  
                  [c_2](x1) = [4 0] x1 + [0]                      
                              [0 0]      [3]                      
                                                                  
           [quot^#](x1, x2) = [0 0] x1 + [0]                      
                              [2 4]      [0]                      
                                                                  
                      [c_3] = [0]                                 
                              [0]                                 
                                                                  
              [c_4](x1, x2) = [2 0] x1 + [4 0] x2 + [0]           
                              [0 0]      [0 0]      [7]           
                                                                  
            [app^#](x1, x2) = [0 0] x1 + [0]                      
                              [2 0]      [6]                      
                                                                  
                      [c_5] = [0]                                 
                              [0]                                 
                                                                  
                  [c_6](x1) = [4 0] x1 + [0]                      
                              [0 0]      [7]                      
                                                                  
            [reverse^#](x1) = [0 0] x1 + [0]                      
                              [6 0]      [2]                      
                                                                  
                      [c_7] = [0]                                 
                              [0]                                 
                                                                  
              [c_8](x1, x2) = [1 0] x1 + [4 0] x2 + [0]           
                              [0 0]      [0 0]      [3]           
                                                                  
            [shuffle^#](x1) = [0]                                 
                              [4]                                 
                                                                  
                      [c_9] = [0]                                 
                              [0]                                 
                                                                  
             [c_10](x1, x2) = [4 0] x1 + [4 0] x2 + [0]           
                              [0 0]      [0 0]      [3]           
                                                                  
         [concat^#](x1, x2) = [0 1] x1 + [0 0] x2 + [0]           
                              [0 0]      [0 4]      [0]           
                                                                  
                     [c_11] = [0]                                 
                              [0]                                 
                                                                  
                 [c_12](x1) = [1 0] x1 + [1]                      
                              [0 0]      [0]                      
                                                                  
    [less_leaves^#](x1, x2) = [4 0] x1 + [2 0] x2 + [0]           
                              [0 0]      [0 0]      [4]           
                                                                  
                     [c_13] = [0]                                 
                              [0]                                 
                                                                  
                     [c_14] = [0]                                 
                              [0]                                 
                                                                  
         [c_15](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [2 0] x3 + [3]
                              [0 0]      [0 0]      [0 0]      [3]
  
  The following symbols are considered usable
  
    {minus, app, reverse, concat, minus^#, quot^#, app^#, reverse^#,
     shuffle^#, concat^#, less_leaves^#}
  
  The order satisfies the following ordering constraints:
  
                            [minus(x, 0())] =  [1 1] x + [0]                                        
                                               [2 2]     [0]                                        
                                            >= [1 0] x + [0]                                        
                                               [0 1]     [0]                                        
                                            =  [x]                                                  
                                                                                                    
                        [minus(s(x), s(y))] =  [1 1] x + [0 0] y + [4]                              
                                               [2 2]     [4 4]     [8]                              
                                            >  [1 1] x + [0 0] y + [0]                              
                                               [2 2]     [0 4]     [0]                              
                                            =  [minus(x, y)]                                        
                                                                                                    
                            [app(nil(), y)] =  [2 0] y + [1]                                        
                                               [0 1]     [0]                                        
                                            >  [1 0] y + [0]                                        
                                               [0 1]     [0]                                        
                                            =  [y]                                                  
                                                                                                    
                        [app(add(n, x), y)] =  [2 0] y + [1]                                        
                                               [0 1]     [0]                                        
                                            >= [1]                                                  
                                               [0]                                                  
                                            =  [add(n, app(x, y))]                                  
                                                                                                    
                           [reverse(nil())] =  [4]                                                  
                                               [0]                                                  
                                            >  [0]                                                  
                                               [0]                                                  
                                            =  [nil()]                                              
                                                                                                    
                       [reverse(add(n, x))] =  [4]                                                  
                                               [0]                                                  
                                            >  [3]                                                  
                                               [0]                                                  
                                            =  [app(reverse(x), add(n, nil()))]                     
                                                                                                    
                        [concat(leaf(), y)] =  [1 0] y + [0]                                        
                                               [0 4]     [4]                                        
                                            >= [1 0] y + [0]                                        
                                               [0 1]     [0]                                        
                                            =  [y]                                                  
                                                                                                    
                    [concat(cons(u, v), y)] =  [1 0] y + [1 1] u + [1 0] v + [2]                    
                                               [0 4]     [2 2]     [2 0]     [8]                    
                                            >= [1 0] y + [1 1] u + [1 0] v + [2]                    
                                               [0 4]     [0 0]     [2 0]     [8]                    
                                            =  [cons(u, concat(v, y))]                              
                                                                                                    
                      [minus^#(s(x), s(y))] =  [0 0] x + [0 0] y + [0]                              
                                               [4 4]     [4 4]     [4]                              
                                            >= [0]                                                  
                                               [3]                                                  
                                            =  [c_2(minus^#(x, y))]                                 
                                                                                                    
                       [quot^#(s(x), s(y))] =  [0 0] x + [0]                                        
                                               [4 4]     [8]                                        
                                            >= [0]                                                  
                                               [7]                                                  
                                            =  [c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))]      
                                                                                                    
                      [app^#(add(n, x), y)] =  [0]                                                  
                                               [8]                                                  
                                            >= [0]                                                  
                                               [7]                                                  
                                            =  [c_6(app^#(x, y))]                                   
                                                                                                    
                     [reverse^#(add(n, x))] =  [0]                                                  
                                               [8]                                                  
                                            >= [0]                                                  
                                               [3]                                                  
                                            =  [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))]
                                                                                                    
                     [shuffle^#(add(n, x))] =  [0]                                                  
                                               [4]                                                  
                                            >= [0]                                                  
                                               [3]                                                  
                                            =  [c_10(shuffle^#(reverse(x)), reverse^#(x))]          
                                                                                                    
                  [concat^#(cons(u, v), y)] =  [0 0] y + [0 1] v + [4]                              
                                               [0 4]     [0 0]     [0]                              
                                            >  [0 1] v + [1]                                        
                                               [0 0]     [0]                                        
                                            =  [c_12(concat^#(v, y))]                               
                                                                                                    
    [less_leaves^#(cons(u, v), cons(w, z))] =  [4 4] u + [4 0] v + [2 2] w + [2 0] z + [12]         
                                               [0 0]     [0 0]     [0 0]     [0 0]     [4]          
                                            >  [4 1] u + [4 0] v + [2 2] w + [2 0] z + [3]          
                                               [0 0]     [0 0]     [0 0]     [0 0]     [3]          
                                            =  [c_15(less_leaves^#(concat(u, v), concat(w, z)),     
                                                     concat^#(u, v),                                
                                                     concat^#(w, z))]                               
                                                                                                    

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) ->
    c_10(shuffle^#(reverse(x)), reverse^#(x)) }
Weak DPs:
  { concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
  , less_leaves^#(cons(u, v), cons(w, z)) ->
    c_15(less_leaves^#(concat(u, v), concat(w, z)),
         concat^#(u, v),
         concat^#(w, z)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

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

{ concat^#(cons(u, v), y) -> c_12(concat^#(v, y))
, less_leaves^#(cons(u, v), cons(w, z)) ->
  c_15(less_leaves^#(concat(u, v), concat(w, z)),
       concat^#(u, v),
       concat^#(w, z)) }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) ->
    c_10(shuffle^#(reverse(x)), reverse^#(x)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
  , concat(leaf(), y) -> y
  , concat(cons(u, v), y) -> cons(u, concat(v, y)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }

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

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) ->
    c_10(shuffle^#(reverse(x)), reverse^#(x)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^3))

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

  { quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
  , shuffle^#(add(n, x)) ->
    c_10(shuffle^#(reverse(x)), reverse^#(x)) }

and lower component

  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) }

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

{ quot^#(s(x), s(y)) -> minus^#(x, y)
, quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
, shuffle^#(add(n, x)) -> reverse^#(x)
, shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }

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:
    { quot^#(s(x), s(y)) ->
      c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))
    , shuffle^#(add(n, x)) ->
      c_10(shuffle^#(reverse(x)), reverse^#(x)) }
  Weak Trs:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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: quot^#(s(x), s(y)) ->
         c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) }
  Trs:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  
  Sub-proof:
  ----------
    The following argument positions are usable:
      Uargs(c_4) = {1}, Uargs(c_10) = {1}
    
    TcT has computed the following constructor-based matrix
    interpretation satisfying not(EDA).
    
              [minus](x1, x2) = [1] x1 + [1]                  
                                                              
                          [0] = [7]                           
                                                              
                      [s](x1) = [1] x1 + [4]                  
                                                              
               [quot](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                [app](x1, x2) = [1] x2 + [1]                  
                                                              
                        [nil] = [0]                           
                                                              
                [add](x1, x2) = [1]                           
                                                              
                [reverse](x1) = [4] x1 + [4]                  
                                                              
                [shuffle](x1) = [7] x1 + [0]                  
                                                              
             [concat](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [leaf] = [0]                           
                                                              
               [cons](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                              
        [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                      [false] = [0]                           
                                                              
                       [true] = [0]                           
                                                              
            [minus^#](x1, x2) = [7] x1 + [7] x2 + [7]         
                                                              
                        [c_1] = [0]                           
                                                              
                    [c_2](x1) = [7] x1 + [0]                  
                                                              
             [quot^#](x1, x2) = [1] x1 + [0]                  
                                                              
                        [c_3] = [0]                           
                                                              
                [c_4](x1, x2) = [1] x1 + [1]                  
                                                              
              [app^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                        [c_5] = [0]                           
                                                              
                    [c_6](x1) = [7] x1 + [0]                  
                                                              
              [reverse^#](x1) = [7] x1 + [7]                  
                                                              
                        [c_7] = [0]                           
                                                              
                [c_8](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
              [shuffle^#](x1) = [0]                           
                                                              
                        [c_9] = [0]                           
                                                              
               [c_10](x1, x2) = [1] x1 + [0]                  
                                                              
           [concat^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [c_11] = [0]                           
                                                              
                   [c_12](x1) = [7] x1 + [0]                  
                                                              
      [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [c_13] = [0]                           
                                                              
                       [c_14] = [0]                           
                                                              
           [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
    
    The following symbols are considered usable
    
      {minus, app, reverse, quot^#, shuffle^#}
    
    The order satisfies the following ordering constraints:
    
             [minus(x, 0())] =  [1] x + [1]                                    
                             >  [1] x + [0]                                    
                             =  [x]                                            
                                                                               
         [minus(s(x), s(y))] =  [1] x + [5]                                    
                             >  [1] x + [1]                                    
                             =  [minus(x, y)]                                  
                                                                               
             [app(nil(), y)] =  [1] y + [1]                                    
                             >  [1] y + [0]                                    
                             =  [y]                                            
                                                                               
         [app(add(n, x), y)] =  [1] y + [1]                                    
                             >= [1]                                            
                             =  [add(n, app(x, y))]                            
                                                                               
            [reverse(nil())] =  [4]                                            
                             >  [0]                                            
                             =  [nil()]                                        
                                                                               
        [reverse(add(n, x))] =  [8]                                            
                             >  [2]                                            
                             =  [app(reverse(x), add(n, nil()))]               
                                                                               
        [quot^#(s(x), s(y))] =  [1] x + [4]                                    
                             >  [1] x + [2]                                    
                             =  [c_4(quot^#(minus(x, y), s(y)), minus^#(x, y))]
                                                                               
      [shuffle^#(add(n, x))] =  [0]                                            
                             >= [0]                                            
                             =  [c_10(shuffle^#(reverse(x)), reverse^#(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:
    { shuffle^#(add(n, x)) ->
      c_10(shuffle^#(reverse(x)), reverse^#(x)) }
  Weak DPs:
    { quot^#(s(x), s(y)) ->
      c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) }
  Weak Trs:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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.
  
  { quot^#(s(x), s(y)) ->
    c_4(quot^#(minus(x, y), s(y)), minus^#(x, y)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs:
    { shuffle^#(add(n, x)) ->
      c_10(shuffle^#(reverse(x)), reverse^#(x)) }
  Weak Trs:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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:
  
    { shuffle^#(add(n, x)) ->
      c_10(shuffle^#(reverse(x)), reverse^#(x)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) }
  Weak Trs:
    { minus(x, 0()) -> x
    , minus(s(x), s(y)) -> minus(x, y)
    , app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  Obligation:
    innermost runtime complexity
  Answer:
    YES(O(1),O(n^1))
  
  We replace rewrite rules by usable rules:
  
    Weak Usable Rules:
      { app(nil(), y) -> y
      , app(add(n, x), y) -> add(n, app(x, y))
      , reverse(nil()) -> nil()
      , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(n^1)).
  
  Strict DPs: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) }
  Weak Trs:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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: shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) }
  
  Sub-proof:
  ----------
    The following argument positions are usable:
      Uargs(c_1) = {1}
    
    TcT has computed the following constructor-based matrix
    interpretation satisfying not(EDA).
    
              [minus](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                          [0] = [0]                           
                                                              
                      [s](x1) = [1] x1 + [0]                  
                                                              
               [quot](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                [app](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                              
                        [nil] = [0]                           
                                                              
                [add](x1, x2) = [1] x1 + [1] x2 + [1]         
                                                              
                [reverse](x1) = [1] x1 + [0]                  
                                                              
                [shuffle](x1) = [7] x1 + [0]                  
                                                              
             [concat](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [leaf] = [0]                           
                                                              
               [cons](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                              
        [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                      [false] = [0]                           
                                                              
                       [true] = [0]                           
                                                              
            [minus^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                        [c_1] = [0]                           
                                                              
                    [c_2](x1) = [7] x1 + [0]                  
                                                              
             [quot^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                        [c_3] = [0]                           
                                                              
                [c_4](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
              [app^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                        [c_5] = [0]                           
                                                              
                    [c_6](x1) = [7] x1 + [0]                  
                                                              
              [reverse^#](x1) = [7] x1 + [0]                  
                                                              
                        [c_7] = [0]                           
                                                              
                [c_8](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
              [shuffle^#](x1) = [1] x1 + [0]                  
                                                              
                        [c_9] = [0]                           
                                                              
               [c_10](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
           [concat^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [c_11] = [0]                           
                                                              
                   [c_12](x1) = [7] x1 + [0]                  
                                                              
      [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [c_13] = [0]                           
                                                              
                       [c_14] = [0]                           
                                                              
           [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
                                                              
                          [c] = [0]                           
                                                              
                    [c_1](x1) = [1] x1 + [0]                  
    
    The following symbols are considered usable
    
      {app, reverse, shuffle^#}
    
    The order satisfies the following ordering constraints:
    
             [app(nil(), y)] =  [1] y + [0]                     
                             >= [1] y + [0]                     
                             =  [y]                             
                                                                
         [app(add(n, x), y)] =  [1] x + [1] y + [1] n + [1]     
                             >= [1] x + [1] y + [1] n + [1]     
                             =  [add(n, app(x, y))]             
                                                                
            [reverse(nil())] =  [0]                             
                             >= [0]                             
                             =  [nil()]                         
                                                                
        [reverse(add(n, x))] =  [1] x + [1] n + [1]             
                             >= [1] x + [1] n + [1]             
                             =  [app(reverse(x), add(n, nil()))]
                                                                
      [shuffle^#(add(n, x))] =  [1] x + [1] n + [1]             
                             >  [1] x + [0]                     
                             =  [c_1(shuffle^#(reverse(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: { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) }
  Weak Trs:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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.
  
  { shuffle^#(add(n, x)) -> c_1(shuffle^#(reverse(x))) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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^2)).

Strict DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) }
Weak DPs:
  { quot^#(s(x), s(y)) -> minus^#(x, y)
  , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
  , shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
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: minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , 4: quot^#(s(x), s(y)) -> minus^#(x, y)
  , 5: quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) }
Trs: { minus(s(x), s(y)) -> minus(x, y) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_2) = {1}, Uargs(c_6) = {1}, Uargs(c_8) = {1, 2}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
            [minus](x1, x2) = [1] x1 + [0]                  
                                                            
                        [0] = [7]                           
                                                            
                    [s](x1) = [1] x1 + [2]                  
                                                            
             [quot](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
              [app](x1, x2) = [4] x2 + [0]                  
                                                            
                      [nil] = [0]                           
                                                            
              [add](x1, x2) = [0]                           
                                                            
              [reverse](x1) = [0]                           
                                                            
              [shuffle](x1) = [7] x1 + [0]                  
                                                            
           [concat](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                     [leaf] = [0]                           
                                                            
             [cons](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                            
      [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                    [false] = [0]                           
                                                            
                     [true] = [0]                           
                                                            
          [minus^#](x1, x2) = [4] x1 + [0]                  
                                                            
                      [c_1] = [0]                           
                                                            
                  [c_2](x1) = [1] x1 + [5]                  
                                                            
           [quot^#](x1, x2) = [4] x1 + [0]                  
                                                            
                      [c_3] = [0]                           
                                                            
              [c_4](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
            [app^#](x1, x2) = [0]                           
                                                            
                      [c_5] = [0]                           
                                                            
                  [c_6](x1) = [2] x1 + [0]                  
                                                            
            [reverse^#](x1) = [0]                           
                                                            
                      [c_7] = [0]                           
                                                            
              [c_8](x1, x2) = [4] x1 + [1] x2 + [0]         
                                                            
            [shuffle^#](x1) = [0]                           
                                                            
                      [c_9] = [0]                           
                                                            
             [c_10](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
         [concat^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                     [c_11] = [0]                           
                                                            
                 [c_12](x1) = [7] x1 + [0]                  
                                                            
    [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                     [c_13] = [0]                           
                                                            
                     [c_14] = [0]                           
                                                            
         [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
  
  The following symbols are considered usable
  
    {minus, app, reverse, minus^#, quot^#, app^#, reverse^#, shuffle^#}
  
  The order satisfies the following ordering constraints:
  
           [minus(x, 0())] =  [1] x + [0]                                          
                           >= [1] x + [0]                                          
                           =  [x]                                                  
                                                                                   
       [minus(s(x), s(y))] =  [1] x + [2]                                          
                           >  [1] x + [0]                                          
                           =  [minus(x, y)]                                        
                                                                                   
           [app(nil(), y)] =  [4] y + [0]                                          
                           >= [1] y + [0]                                          
                           =  [y]                                                  
                                                                                   
       [app(add(n, x), y)] =  [4] y + [0]                                          
                           >= [0]                                                  
                           =  [add(n, app(x, y))]                                  
                                                                                   
          [reverse(nil())] =  [0]                                                  
                           >= [0]                                                  
                           =  [nil()]                                              
                                                                                   
      [reverse(add(n, x))] =  [0]                                                  
                           >= [0]                                                  
                           =  [app(reverse(x), add(n, nil()))]                     
                                                                                   
     [minus^#(s(x), s(y))] =  [4] x + [8]                                          
                           >  [4] x + [5]                                          
                           =  [c_2(minus^#(x, y))]                                 
                                                                                   
      [quot^#(s(x), s(y))] =  [4] x + [8]                                          
                           >  [4] x + [0]                                          
                           =  [minus^#(x, y)]                                      
                                                                                   
      [quot^#(s(x), s(y))] =  [4] x + [8]                                          
                           >  [4] x + [0]                                          
                           =  [quot^#(minus(x, y), s(y))]                          
                                                                                   
     [app^#(add(n, x), y)] =  [0]                                                  
                           >= [0]                                                  
                           =  [c_6(app^#(x, y))]                                   
                                                                                   
    [reverse^#(add(n, x))] =  [0]                                                  
                           >= [0]                                                  
                           =  [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))]
                                                                                   
    [shuffle^#(add(n, x))] =  [0]                                                  
                           >= [0]                                                  
                           =  [reverse^#(x)]                                       
                                                                                   
    [shuffle^#(add(n, x))] =  [0]                                                  
                           >= [0]                                                  
                           =  [shuffle^#(reverse(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^2)).

Strict DPs:
  { app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) }
Weak DPs:
  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
  , quot^#(s(x), s(y)) -> minus^#(x, y)
  , quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y))
  , shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
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.

{ minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
, quot^#(s(x), s(y)) -> minus^#(x, y)
, quot^#(s(x), s(y)) -> quot^#(minus(x, y), s(y)) }

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

Strict DPs:
  { app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) }
Weak DPs:
  { shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
Weak Trs:
  { minus(x, 0()) -> x
  , minus(s(x), s(y)) -> minus(x, y)
  , app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^2))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }

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

Strict DPs:
  { app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) }
Weak DPs:
  { shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
Weak Trs:
  { app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
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

  { reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }

and lower component

  { app^#(add(n, x), y) -> c_6(app^#(x, y)) }

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

{ reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil()))
, reverse^#(add(n, x)) -> reverse^#(x)
, shuffle^#(add(n, x)) -> reverse^#(x)
, shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }

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:
    { reverse^#(add(n, x)) ->
      c_8(app^#(reverse(x), add(n, nil())), reverse^#(x)) }
  Weak DPs:
    { shuffle^#(add(n, x)) -> reverse^#(x)
    , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
  Weak Trs:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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: reverse^#(add(n, x)) ->
         c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
    , 2: shuffle^#(add(n, x)) -> reverse^#(x)
    , 3: shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
  
  Sub-proof:
  ----------
    The following argument positions are usable:
      Uargs(c_8) = {1, 2}
    
    TcT has computed the following constructor-based matrix
    interpretation satisfying not(EDA).
    
              [minus](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                          [0] = [0]                           
                                                              
                      [s](x1) = [1] x1 + [0]                  
                                                              
               [quot](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                [app](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                              
                        [nil] = [0]                           
                                                              
                [add](x1, x2) = [1] x1 + [1] x2 + [1]         
                                                              
                [reverse](x1) = [1] x1 + [0]                  
                                                              
                [shuffle](x1) = [7] x1 + [0]                  
                                                              
             [concat](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [leaf] = [0]                           
                                                              
               [cons](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                              
        [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                      [false] = [0]                           
                                                              
                       [true] = [0]                           
                                                              
            [minus^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                        [c_1] = [0]                           
                                                              
                    [c_2](x1) = [7] x1 + [0]                  
                                                              
             [quot^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                        [c_3] = [0]                           
                                                              
                [c_4](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
              [app^#](x1, x2) = [0]                           
                                                              
                        [c_5] = [0]                           
                                                              
                    [c_6](x1) = [7] x1 + [0]                  
                                                              
              [reverse^#](x1) = [1] x1 + [0]                  
                                                              
                        [c_7] = [0]                           
                                                              
                [c_8](x1, x2) = [4] x1 + [1] x2 + [0]         
                                                              
              [shuffle^#](x1) = [1] x1 + [7]                  
                                                              
                        [c_9] = [0]                           
                                                              
               [c_10](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
           [concat^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [c_11] = [0]                           
                                                              
                   [c_12](x1) = [7] x1 + [0]                  
                                                              
      [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                              
                       [c_13] = [0]                           
                                                              
                       [c_14] = [0]                           
                                                              
           [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
    
    The following symbols are considered usable
    
      {app, reverse, reverse^#, shuffle^#}
    
    The order satisfies the following ordering constraints:
    
             [app(nil(), y)] =  [1] y + [0]                                          
                             >= [1] y + [0]                                          
                             =  [y]                                                  
                                                                                     
         [app(add(n, x), y)] =  [1] x + [1] y + [1] n + [1]                          
                             >= [1] x + [1] y + [1] n + [1]                          
                             =  [add(n, app(x, y))]                                  
                                                                                     
            [reverse(nil())] =  [0]                                                  
                             >= [0]                                                  
                             =  [nil()]                                              
                                                                                     
        [reverse(add(n, x))] =  [1] x + [1] n + [1]                                  
                             >= [1] x + [1] n + [1]                                  
                             =  [app(reverse(x), add(n, nil()))]                     
                                                                                     
      [reverse^#(add(n, x))] =  [1] x + [1] n + [1]                                  
                             >  [1] x + [0]                                          
                             =  [c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))]
                                                                                     
      [shuffle^#(add(n, x))] =  [1] x + [1] n + [8]                                  
                             >  [1] x + [0]                                          
                             =  [reverse^#(x)]                                       
                                                                                     
      [shuffle^#(add(n, x))] =  [1] x + [1] n + [8]                                  
                             >  [1] x + [7]                                          
                             =  [shuffle^#(reverse(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:
    { reverse^#(add(n, x)) ->
      c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
    , shuffle^#(add(n, x)) -> reverse^#(x)
    , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
  Weak Trs:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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.
  
  { reverse^#(add(n, x)) ->
    c_8(app^#(reverse(x), add(n, nil())), reverse^#(x))
  , shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
  
  We are left with following problem, upon which TcT provides the
  certificate YES(O(1),O(1)).
  
  Weak Trs:
    { app(nil(), y) -> y
    , app(add(n, x), y) -> add(n, app(x, y))
    , reverse(nil()) -> nil()
    , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
  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^#(add(n, x), y) -> c_6(app^#(x, y)) }
Weak DPs:
  { reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil()))
  , reverse^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
Weak Trs:
  { app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
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^#(add(n, x), y) -> c_6(app^#(x, y))
  , 2: reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil()))
  , 3: reverse^#(add(n, x)) -> reverse^#(x)
  , 4: shuffle^#(add(n, x)) -> reverse^#(x)
  , 5: shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_6) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
            [minus](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                        [0] = [0]                           
                                                            
                    [s](x1) = [1] x1 + [0]                  
                                                            
             [quot](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
              [app](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                            
                      [nil] = [0]                           
                                                            
              [add](x1, x2) = [1] x1 + [1] x2 + [1]         
                                                            
              [reverse](x1) = [1] x1 + [0]                  
                                                            
              [shuffle](x1) = [7] x1 + [0]                  
                                                            
           [concat](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                     [leaf] = [0]                           
                                                            
             [cons](x1, x2) = [1] x1 + [1] x2 + [0]         
                                                            
      [less_leaves](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                    [false] = [0]                           
                                                            
                     [true] = [0]                           
                                                            
          [minus^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                      [c_1] = [0]                           
                                                            
                  [c_2](x1) = [7] x1 + [0]                  
                                                            
           [quot^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                      [c_3] = [0]                           
                                                            
              [c_4](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
            [app^#](x1, x2) = [1] x1 + [0]                  
                                                            
                      [c_5] = [0]                           
                                                            
                  [c_6](x1) = [1] x1 + [0]                  
                                                            
            [reverse^#](x1) = [1] x1 + [0]                  
                                                            
                      [c_7] = [0]                           
                                                            
              [c_8](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
            [shuffle^#](x1) = [1] x1 + [7]                  
                                                            
                      [c_9] = [0]                           
                                                            
             [c_10](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
         [concat^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                     [c_11] = [0]                           
                                                            
                 [c_12](x1) = [7] x1 + [0]                  
                                                            
    [less_leaves^#](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                            
                     [c_13] = [0]                           
                                                            
                     [c_14] = [0]                           
                                                            
         [c_15](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
  
  The following symbols are considered usable
  
    {app, reverse, app^#, reverse^#, shuffle^#}
  
  The order satisfies the following ordering constraints:
  
           [app(nil(), y)] =  [1] y + [0]                       
                           >= [1] y + [0]                       
                           =  [y]                               
                                                                
       [app(add(n, x), y)] =  [1] x + [1] y + [1] n + [1]       
                           >= [1] x + [1] y + [1] n + [1]       
                           =  [add(n, app(x, y))]               
                                                                
          [reverse(nil())] =  [0]                               
                           >= [0]                               
                           =  [nil()]                           
                                                                
      [reverse(add(n, x))] =  [1] x + [1] n + [1]               
                           >= [1] x + [1] n + [1]               
                           =  [app(reverse(x), add(n, nil()))]  
                                                                
     [app^#(add(n, x), y)] =  [1] x + [1] n + [1]               
                           >  [1] x + [0]                       
                           =  [c_6(app^#(x, y))]                
                                                                
    [reverse^#(add(n, x))] =  [1] x + [1] n + [1]               
                           >  [1] x + [0]                       
                           =  [app^#(reverse(x), add(n, nil()))]
                                                                
    [reverse^#(add(n, x))] =  [1] x + [1] n + [1]               
                           >  [1] x + [0]                       
                           =  [reverse^#(x)]                    
                                                                
    [shuffle^#(add(n, x))] =  [1] x + [1] n + [8]               
                           >  [1] x + [0]                       
                           =  [reverse^#(x)]                    
                                                                
    [shuffle^#(add(n, x))] =  [1] x + [1] n + [8]               
                           >  [1] x + [7]                       
                           =  [shuffle^#(reverse(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:
  { app^#(add(n, x), y) -> c_6(app^#(x, y))
  , reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil()))
  , reverse^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> reverse^#(x)
  , shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }
Weak Trs:
  { app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
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.

{ app^#(add(n, x), y) -> c_6(app^#(x, y))
, reverse^#(add(n, x)) -> app^#(reverse(x), add(n, nil()))
, reverse^#(add(n, x)) -> reverse^#(x)
, shuffle^#(add(n, x)) -> reverse^#(x)
, shuffle^#(add(n, x)) -> shuffle^#(reverse(x)) }

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

Weak Trs:
  { app(nil(), y) -> y
  , app(add(n, x), y) -> add(n, app(x, y))
  , reverse(nil()) -> nil()
  , reverse(add(n, x)) -> app(reverse(x), add(n, nil())) }
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^3))