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

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

Strict Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z))
  , rev(nil()) -> nil()
  , rev(unit(x)) -> unit(x)
  , rev(++(x, y)) -> ++(rev(y), rev(x))
  , rev(rev(x)) -> x }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following dependency tuples:

Strict DPs:
  { flatten^#(flatten(x)) -> c_1(flatten^#(x))
  , flatten^#(nil()) -> c_2()
  , flatten^#(unit(x)) -> c_3(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(x, nil()) -> c_6()
  , ++^#(nil(), y) -> c_7()
  , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
  , rev^#(nil()) -> c_9()
  , rev^#(unit(x)) -> c_10()
  , rev^#(++(x, y)) -> c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x))
  , rev^#(rev(x)) -> c_12() }

and mark the set of starting terms.

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

Strict DPs:
  { flatten^#(flatten(x)) -> c_1(flatten^#(x))
  , flatten^#(nil()) -> c_2()
  , flatten^#(unit(x)) -> c_3(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(x, nil()) -> c_6()
  , ++^#(nil(), y) -> c_7()
  , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
  , rev^#(nil()) -> c_9()
  , rev^#(unit(x)) -> c_10()
  , rev^#(++(x, y)) -> c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x))
  , rev^#(rev(x)) -> c_12() }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z))
  , rev(nil()) -> nil()
  , rev(unit(x)) -> unit(x)
  , rev(++(x, y)) -> ++(rev(y), rev(x))
  , rev(rev(x)) -> x }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

Consider the dependency graph:

  1: flatten^#(flatten(x)) -> c_1(flatten^#(x))
  
  2: flatten^#(nil()) -> c_2()
  
  3: flatten^#(unit(x)) -> c_3(flatten^#(x))
     -->_1 flatten^#(++(unit(x), y)) ->
           c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
     -->_1 flatten^#(++(x, y)) ->
           c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
     -->_1 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
     -->_1 flatten^#(nil()) -> c_2() :2
     -->_1 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
  
  4: flatten^#(++(x, y)) ->
     c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
     -->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
     -->_3 flatten^#(++(unit(x), y)) ->
           c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
     -->_1 ++^#(nil(), y) -> c_7() :7
     -->_1 ++^#(x, nil()) -> c_6() :6
     -->_3 flatten^#(++(x, y)) ->
           c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
     -->_3 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
     -->_2 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
     -->_3 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
     -->_2 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
  
  5: flatten^#(++(unit(x), y)) ->
     c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
     -->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
     -->_1 ++^#(nil(), y) -> c_7() :7
     -->_1 ++^#(x, nil()) -> c_6() :6
     -->_3 flatten^#(++(unit(x), y)) ->
           c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
     -->_2 flatten^#(++(unit(x), y)) ->
           c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :5
     -->_3 flatten^#(++(x, y)) ->
           c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
     -->_2 flatten^#(++(x, y)) ->
           c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y)) :4
     -->_3 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
     -->_2 flatten^#(unit(x)) -> c_3(flatten^#(x)) :3
     -->_2 flatten^#(nil()) -> c_2() :2
     -->_3 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
     -->_2 flatten^#(flatten(x)) -> c_1(flatten^#(x)) :1
  
  6: ++^#(x, nil()) -> c_6()
  
  7: ++^#(nil(), y) -> c_7()
  
  8: ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
     -->_2 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
     -->_2 ++^#(x, nil()) -> c_6() :6
     -->_1 ++^#(x, nil()) -> c_6() :6
  
  9: rev^#(nil()) -> c_9()
  
  10: rev^#(unit(x)) -> c_10()
  
  11: rev^#(++(x, y)) ->
      c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x))
     -->_3 rev^#(rev(x)) -> c_12() :12
     -->_2 rev^#(rev(x)) -> c_12() :12
     -->_2 rev^#(++(x, y)) ->
           c_11(++^#(rev(y), rev(x)), rev^#(y), rev^#(x)) :11
     -->_3 rev^#(unit(x)) -> c_10() :10
     -->_2 rev^#(unit(x)) -> c_10() :10
     -->_1 ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) :8
     -->_1 ++^#(nil(), y) -> c_7() :7
     -->_1 ++^#(x, nil()) -> c_6() :6
  
  12: rev^#(rev(x)) -> c_12()
  

Only the nodes {2,3,5,8,6,7,4,1,9,10} are reachable from nodes
{2,3,6,7,9,10} 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^1)).

Strict DPs:
  { flatten^#(flatten(x)) -> c_1(flatten^#(x))
  , flatten^#(nil()) -> c_2()
  , flatten^#(unit(x)) -> c_3(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(x, nil()) -> c_6()
  , ++^#(nil(), y) -> c_7()
  , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
  , rev^#(nil()) -> c_9()
  , rev^#(unit(x)) -> c_10() }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z))
  , rev(nil()) -> nil()
  , rev(unit(x)) -> unit(x)
  , rev(++(x, y)) -> ++(rev(y), rev(x))
  , rev(rev(x)) -> x }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

  DPs:
    { 1: flatten^#(flatten(x)) -> c_1(flatten^#(x))
    , 2: flatten^#(nil()) -> c_2()
    , 3: flatten^#(unit(x)) -> c_3(flatten^#(x))
    , 4: flatten^#(++(x, y)) ->
         c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
    , 5: flatten^#(++(unit(x), y)) ->
         c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
    , 6: ++^#(x, nil()) -> c_6()
    , 7: ++^#(nil(), y) -> c_7()
    , 8: ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z))
    , 9: rev^#(nil()) -> c_9()
    , 10: rev^#(unit(x)) -> c_10() }

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

Strict DPs:
  { flatten^#(unit(x)) -> c_3(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) }
Weak DPs:
  { flatten^#(flatten(x)) -> c_1(flatten^#(x))
  , flatten^#(nil()) -> c_2()
  , ++^#(x, nil()) -> c_6()
  , ++^#(nil(), y) -> c_7()
  , rev^#(nil()) -> c_9()
  , rev^#(unit(x)) -> c_10() }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z))
  , rev(nil()) -> nil()
  , rev(unit(x)) -> unit(x)
  , rev(++(x, y)) -> ++(rev(y), rev(x))
  , rev(rev(x)) -> x }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

{ flatten^#(flatten(x)) -> c_1(flatten^#(x))
, flatten^#(nil()) -> c_2()
, ++^#(x, nil()) -> c_6()
, ++^#(nil(), y) -> c_7()
, rev^#(nil()) -> c_9()
, rev^#(unit(x)) -> c_10() }

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

Strict DPs:
  { flatten^#(unit(x)) -> c_3(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_4(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_5(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z))
  , rev(nil()) -> nil()
  , rev(unit(x)) -> unit(x)
  , rev(++(x, y)) -> ++(rev(y), rev(x))
  , rev(rev(x)) -> x }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

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

  { ++^#(++(x, y), z) -> c_8(++^#(x, ++(y, z)), ++^#(y, z)) }

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

Strict DPs:
  { flatten^#(unit(x)) -> c_1(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z))
  , rev(nil()) -> nil()
  , rev(unit(x)) -> unit(x)
  , rev(++(x, y)) -> ++(rev(y), rev(x))
  , rev(rev(x)) -> x }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { flatten(flatten(x)) -> flatten(x)
    , flatten(nil()) -> nil()
    , flatten(unit(x)) -> flatten(x)
    , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
    , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
    , ++(x, nil()) -> x
    , ++(nil(), y) -> y
    , ++(++(x, y), z) -> ++(x, ++(y, z)) }

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

Strict DPs:
  { flatten^#(unit(x)) -> c_1(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z)) }
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: flatten^#(unit(x)) -> c_1(flatten^#(x))
  , 2: flatten^#(++(x, y)) ->
       c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , 3: flatten^#(++(unit(x), y)) ->
       c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , 4: ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Trs:
  { flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z)) }

Sub-proof:
----------
  The following argument positions are usable:
    Uargs(c_1) = {1}, Uargs(c_2) = {1, 2, 3}, Uargs(c_3) = {1, 2, 3},
    Uargs(c_4) = {1}
  
  TcT has computed the following constructor-based matrix
  interpretation satisfying not(EDA).
  
         [flatten](x1) = [2] x1 + [0]                  
                                                       
                 [nil] = [0]                           
                                                       
            [unit](x1) = [1] x1 + [1]                  
                                                       
          [++](x1, x2) = [3] x1 + [1] x2 + [2]         
                                                       
             [rev](x1) = [7] x1 + [0]                  
                                                       
       [flatten^#](x1) = [3] x1 + [0]                  
                                                       
             [c_1](x1) = [7] x1 + [0]                  
                                                       
                 [c_2] = [0]                           
                                                       
             [c_3](x1) = [7] x1 + [0]                  
                                                       
     [c_4](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
                                                       
        [++^#](x1, x2) = [1] x1 + [0]                  
                                                       
     [c_5](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
                                                       
                 [c_6] = [0]                           
                                                       
                 [c_7] = [0]                           
                                                       
         [c_8](x1, x2) = [7] x1 + [7] x2 + [0]         
                                                       
           [rev^#](x1) = [7] x1 + [0]                  
                                                       
                 [c_9] = [0]                           
                                                       
                [c_10] = [0]                           
                                                       
    [c_11](x1, x2, x3) = [7] x1 + [7] x2 + [7] x3 + [0]
                                                       
                [c_12] = [0]                           
                                                       
                   [c] = [0]                           
                                                       
             [c_1](x1) = [1] x1 + [1]                  
                                                       
     [c_2](x1, x2, x3) = [2] x1 + [1] x2 + [1] x3 + [3]
                                                       
     [c_3](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [3]
                                                       
             [c_4](x1) = [1] x1 + [1]                  
  
  The following symbols are considered usable
  
    {flatten, ++, flatten^#, ++^#}
  
  The order satisfies the following ordering constraints:
  
          [flatten(flatten(x))] =  [4] x + [0]                                                    
                                >= [2] x + [0]                                                    
                                =  [flatten(x)]                                                   
                                                                                                  
               [flatten(nil())] =  [0]                                                            
                                >= [0]                                                            
                                =  [nil()]                                                        
                                                                                                  
             [flatten(unit(x))] =  [2] x + [2]                                                    
                                >  [2] x + [0]                                                    
                                =  [flatten(x)]                                                   
                                                                                                  
            [flatten(++(x, y))] =  [6] x + [2] y + [4]                                            
                                >  [6] x + [2] y + [2]                                            
                                =  [++(flatten(x), flatten(y))]                                   
                                                                                                  
      [flatten(++(unit(x), y))] =  [6] x + [2] y + [10]                                           
                                >  [6] x + [2] y + [2]                                            
                                =  [++(flatten(x), flatten(y))]                                   
                                                                                                  
                 [++(x, nil())] =  [3] x + [2]                                                    
                                >  [1] x + [0]                                                    
                                =  [x]                                                            
                                                                                                  
                 [++(nil(), y)] =  [1] y + [2]                                                    
                                >  [1] y + [0]                                                    
                                =  [y]                                                            
                                                                                                  
              [++(++(x, y), z)] =  [9] x + [3] y + [1] z + [8]                                    
                                >  [3] x + [3] y + [1] z + [4]                                    
                                =  [++(x, ++(y, z))]                                              
                                                                                                  
           [flatten^#(unit(x))] =  [3] x + [3]                                                    
                                >  [3] x + [1]                                                    
                                =  [c_1(flatten^#(x))]                                            
                                                                                                  
          [flatten^#(++(x, y))] =  [9] x + [3] y + [6]                                            
                                >  [7] x + [3] y + [3]                                            
                                =  [c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))]
                                                                                                  
    [flatten^#(++(unit(x), y))] =  [9] x + [3] y + [15]                                           
                                >  [8] x + [3] y + [3]                                            
                                =  [c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))]
                                                                                                  
            [++^#(++(x, y), z)] =  [3] x + [1] y + [2]                                            
                                >  [1] y + [1]                                                    
                                =  [c_4(++^#(y, 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(1)).

Weak DPs:
  { flatten^#(unit(x)) -> c_1(flatten^#(x))
  , flatten^#(++(x, y)) ->
    c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , flatten^#(++(unit(x), y)) ->
    c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
  , ++^#(++(x, y), z) -> c_4(++^#(y, z)) }
Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z)) }
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.

{ flatten^#(unit(x)) -> c_1(flatten^#(x))
, flatten^#(++(x, y)) ->
  c_2(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, flatten^#(++(unit(x), y)) ->
  c_3(++^#(flatten(x), flatten(y)), flatten^#(x), flatten^#(y))
, ++^#(++(x, y), z) -> c_4(++^#(y, z)) }

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

Weak Trs:
  { flatten(flatten(x)) -> flatten(x)
  , flatten(nil()) -> nil()
  , flatten(unit(x)) -> flatten(x)
  , flatten(++(x, y)) -> ++(flatten(x), flatten(y))
  , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
  , ++(x, nil()) -> x
  , ++(nil(), y) -> y
  , ++(++(x, y), z) -> ++(x, ++(y, z)) }
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^1))