WORST_CASE(?,O(n^1))
* Step 1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            concat(cons(U,V),Y) -> cons(U,concat(V,Y))
            concat(leaf(),Y) -> Y
            lessleaves(X,leaf()) -> false()
            lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
            lessleaves(leaf(),cons(W,Z)) -> true()
        - Signature:
            {concat/2,lessleaves/2} / {cons/2,false/0,leaf/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {concat,lessleaves} and constructors {cons,false,leaf
            ,true}
    + Applied Processor:
        NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(cons) = {2},
          uargs(lessleaves) = {1,2}
        
        Following symbols are considered usable:
          {concat,lessleaves}
        TcT has computed the following interpretation:
              p(concat) = [1 2] x1 + [1 0] x2 + [0]
                          [0 2]      [0 1]      [0]
                p(cons) = [1 3] x1 + [1 0] x2 + [0]
                          [0 0]      [0 1]      [7]
               p(false) = [0]                      
                          [0]                      
                p(leaf) = [1]                      
                          [0]                      
          p(lessleaves) = [1 0] x1 + [4 2] x2 + [0]
                          [4 0]      [0 0]      [1]
                p(true) = [0]                      
                          [1]                      
        
        Following rules are strictly oriented:
                    concat(cons(U,V),Y) = [1 3] U + [1 2] V + [1 0] Y + [14]            
                                          [0 0]     [0 2]     [0 1]     [14]            
                                        > [1 3] U + [1 2] V + [1 0] Y + [0]             
                                          [0 0]     [0 2]     [0 1]     [7]             
                                        = cons(U,concat(V,Y))                           
        
                       concat(leaf(),Y) = [1 0] Y + [1]                                 
                                          [0 1]     [0]                                 
                                        > [1 0] Y + [0]                                 
                                          [0 1]     [0]                                 
                                        = Y                                             
        
                   lessleaves(X,leaf()) = [1 0] X + [4]                                 
                                          [4 0]     [1]                                 
                                        > [0]                                           
                                          [0]                                           
                                        = false()                                       
        
        lessleaves(cons(U,V),cons(W,Z)) = [1  3] U + [1 0] V + [4 12] W + [4 2] Z + [14]
                                          [4 12]     [4 0]     [0  0]     [0 0]     [1] 
                                        > [1 2] U + [1 0] V + [4 12] W + [4 2] Z + [0]  
                                          [4 8]     [4 0]     [0  0]     [0 0]     [1]  
                                        = lessleaves(concat(U,V),concat(W,Z))           
        
           lessleaves(leaf(),cons(W,Z)) = [4 12] W + [4 2] Z + [15]                     
                                          [0  0]     [0 0]     [5]                      
                                        > [0]                                           
                                          [1]                                           
                                        = true()                                        
        
        
        Following rules are (at-least) weakly oriented:
        

WORST_CASE(?,O(n^1))