* Step 1: Sum WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(::) = {2},
            uargs(subtrees#2) = {1},
            uargs(subtrees#3) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                    p(::) = [1] x2 + [10]        
                p(append) = [1] x2 + [1]         
              p(append#1) = [1] x2 + [0]         
                  p(leaf) = [0]                  
                   p(nil) = [0]                  
                  p(node) = [1] x2 + [1] x3 + [0]
              p(subtrees) = [0]                  
            p(subtrees#1) = [0]                  
            p(subtrees#2) = [1] x1 + [0]         
            p(subtrees#3) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
          append(@l1,@l2) = [1] @l2 + [1]    
                          > [1] @l2 + [0]    
                          = append#1(@l1,@l2)
          
          
          Following rules are (at-least) weakly oriented:
                append#1(::(@x,@xs),@l2) =  [1] @l2 + [0]                           
                                         >= [1] @l2 + [11]                          
                                         =  ::(@x,append(@xs,@l2))                  
          
                     append#1(nil(),@l2) =  [1] @l2 + [0]                           
                                         >= [1] @l2 + [0]                           
                                         =  @l2                                     
          
                            subtrees(@t) =  [0]                                     
                                         >= [0]                                     
                                         =  subtrees#1(@t)                          
          
                      subtrees#1(leaf()) =  [0]                                     
                                         >= [0]                                     
                                         =  nil()                                   
          
            subtrees#1(node(@x,@t1,@t2)) =  [0]                                     
                                         >= [0]                                     
                                         =  subtrees#2(subtrees(@t1),@t1,@t2,@x)    
          
              subtrees#2(@l1,@t1,@t2,@x) =  [1] @l1 + [0]                           
                                         >= [1] @l1 + [0]                           
                                         =  subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
          
          subtrees#3(@l2,@l1,@t1,@t2,@x) =  [1] @l1 + [1] @l2 + [0]                 
                                         >= [1] @l2 + [11]                          
                                         =  ::(node(@x,@t1,@t2),append(@l1,@l2))    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Weak TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(::) = {2},
            uargs(subtrees#2) = {1},
            uargs(subtrees#3) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                    p(::) = [1] x2 + [0]                  
                p(append) = [1] x1 + [1] x2 + [0]         
              p(append#1) = [1] x1 + [1] x2 + [0]         
                  p(leaf) = [0]                           
                   p(nil) = [0]                           
                  p(node) = [1] x1 + [1] x2 + [1] x3 + [0]
              p(subtrees) = [0]                           
            p(subtrees#1) = [0]                           
            p(subtrees#2) = [1] x1 + [0]                  
            p(subtrees#3) = [1] x1 + [1] x2 + [1]         
          
          Following rules are strictly oriented:
          subtrees#3(@l2,@l1,@t1,@t2,@x) = [1] @l1 + [1] @l2 + [1]             
                                         > [1] @l1 + [1] @l2 + [0]             
                                         = ::(node(@x,@t1,@t2),append(@l1,@l2))
          
          
          Following rules are (at-least) weakly oriented:
                       append(@l1,@l2) =  [1] @l1 + [1] @l2 + [0]                 
                                       >= [1] @l1 + [1] @l2 + [0]                 
                                       =  append#1(@l1,@l2)                       
          
              append#1(::(@x,@xs),@l2) =  [1] @l2 + [1] @xs + [0]                 
                                       >= [1] @l2 + [1] @xs + [0]                 
                                       =  ::(@x,append(@xs,@l2))                  
          
                   append#1(nil(),@l2) =  [1] @l2 + [0]                           
                                       >= [1] @l2 + [0]                           
                                       =  @l2                                     
          
                          subtrees(@t) =  [0]                                     
                                       >= [0]                                     
                                       =  subtrees#1(@t)                          
          
                    subtrees#1(leaf()) =  [0]                                     
                                       >= [0]                                     
                                       =  nil()                                   
          
          subtrees#1(node(@x,@t1,@t2)) =  [0]                                     
                                       >= [0]                                     
                                       =  subtrees#2(subtrees(@t1),@t1,@t2,@x)    
          
            subtrees#2(@l1,@t1,@t2,@x) =  [1] @l1 + [0]                           
                                       >= [1] @l1 + [1]                           
                                       =  subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
        - Weak TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(::) = {2},
            uargs(subtrees#2) = {1},
            uargs(subtrees#3) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                    p(::) = [1] x2 + [0]         
                p(append) = [1] x2 + [0]         
              p(append#1) = [1] x2 + [0]         
                  p(leaf) = [0]                  
                   p(nil) = [0]                  
                  p(node) = [1] x3 + [1]         
              p(subtrees) = [8]                  
            p(subtrees#1) = [2]                  
            p(subtrees#2) = [1] x1 + [8]         
            p(subtrees#3) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
                subtrees(@t) = [8]           
                             > [2]           
                             = subtrees#1(@t)
          
          subtrees#1(leaf()) = [2]           
                             > [0]           
                             = nil()         
          
          
          Following rules are (at-least) weakly oriented:
                         append(@l1,@l2) =  [1] @l2 + [0]                           
                                         >= [1] @l2 + [0]                           
                                         =  append#1(@l1,@l2)                       
          
                append#1(::(@x,@xs),@l2) =  [1] @l2 + [0]                           
                                         >= [1] @l2 + [0]                           
                                         =  ::(@x,append(@xs,@l2))                  
          
                     append#1(nil(),@l2) =  [1] @l2 + [0]                           
                                         >= [1] @l2 + [0]                           
                                         =  @l2                                     
          
            subtrees#1(node(@x,@t1,@t2)) =  [2]                                     
                                         >= [16]                                    
                                         =  subtrees#2(subtrees(@t1),@t1,@t2,@x)    
          
              subtrees#2(@l1,@t1,@t2,@x) =  [1] @l1 + [8]                           
                                         >= [1] @l1 + [8]                           
                                         =  subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
          
          subtrees#3(@l2,@l1,@t1,@t2,@x) =  [1] @l1 + [1] @l2 + [0]                 
                                         >= [1] @l2 + [0]                           
                                         =  ::(node(@x,@t1,@t2),append(@l1,@l2))    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
        - Weak TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(::) = {2},
            uargs(subtrees#2) = {1},
            uargs(subtrees#3) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                    p(::) = [1] x2 + [0]         
                p(append) = [1] x1 + [1] x2 + [0]
              p(append#1) = [1] x1 + [1] x2 + [0]
                  p(leaf) = [0]                  
                   p(nil) = [0]                  
                  p(node) = [1] x2 + [1] x3 + [5]
              p(subtrees) = [1] x1 + [0]         
            p(subtrees#1) = [1] x1 + [0]         
            p(subtrees#2) = [1] x1 + [1] x3 + [1]
            p(subtrees#3) = [1] x1 + [1] x2 + [0]
          
          Following rules are strictly oriented:
          subtrees#1(node(@x,@t1,@t2)) = [1] @t1 + [1] @t2 + [5]                 
                                       > [1] @t1 + [1] @t2 + [1]                 
                                       = subtrees#2(subtrees(@t1),@t1,@t2,@x)    
          
            subtrees#2(@l1,@t1,@t2,@x) = [1] @l1 + [1] @t2 + [1]                 
                                       > [1] @l1 + [1] @t2 + [0]                 
                                       = subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
          
          
          Following rules are (at-least) weakly oriented:
                         append(@l1,@l2) =  [1] @l1 + [1] @l2 + [0]             
                                         >= [1] @l1 + [1] @l2 + [0]             
                                         =  append#1(@l1,@l2)                   
          
                append#1(::(@x,@xs),@l2) =  [1] @l2 + [1] @xs + [0]             
                                         >= [1] @l2 + [1] @xs + [0]             
                                         =  ::(@x,append(@xs,@l2))              
          
                     append#1(nil(),@l2) =  [1] @l2 + [0]                       
                                         >= [1] @l2 + [0]                       
                                         =  @l2                                 
          
                            subtrees(@t) =  [1] @t + [0]                        
                                         >= [1] @t + [0]                        
                                         =  subtrees#1(@t)                      
          
                      subtrees#1(leaf()) =  [0]                                 
                                         >= [0]                                 
                                         =  nil()                               
          
          subtrees#3(@l2,@l1,@t1,@t2,@x) =  [1] @l1 + [1] @l2 + [0]             
                                         >= [1] @l1 + [1] @l2 + [0]             
                                         =  ::(node(@x,@t1,@t2),append(@l1,@l2))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
        - Weak TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following nonconstant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(::) = {2},
            uargs(subtrees#2) = {1},
            uargs(subtrees#3) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                    p(::) = [1] x2 + [6]         
                p(append) = [1] x1 + [1] x2 + [0]
              p(append#1) = [1] x1 + [1] x2 + [0]
                  p(leaf) = [1]                  
                   p(nil) = [1]                  
                  p(node) = [1] x2 + [1] x3 + [6]
              p(subtrees) = [1] x1 + [0]         
            p(subtrees#1) = [1] x1 + [0]         
            p(subtrees#2) = [1] x1 + [1] x3 + [6]
            p(subtrees#3) = [1] x1 + [1] x2 + [6]
          
          Following rules are strictly oriented:
          append#1(nil(),@l2) = [1] @l2 + [1]
                              > [1] @l2 + [0]
                              = @l2          
          
          
          Following rules are (at-least) weakly oriented:
                         append(@l1,@l2) =  [1] @l1 + [1] @l2 + [0]                 
                                         >= [1] @l1 + [1] @l2 + [0]                 
                                         =  append#1(@l1,@l2)                       
          
                append#1(::(@x,@xs),@l2) =  [1] @l2 + [1] @xs + [6]                 
                                         >= [1] @l2 + [1] @xs + [6]                 
                                         =  ::(@x,append(@xs,@l2))                  
          
                            subtrees(@t) =  [1] @t + [0]                            
                                         >= [1] @t + [0]                            
                                         =  subtrees#1(@t)                          
          
                      subtrees#1(leaf()) =  [1]                                     
                                         >= [1]                                     
                                         =  nil()                                   
          
            subtrees#1(node(@x,@t1,@t2)) =  [1] @t1 + [1] @t2 + [6]                 
                                         >= [1] @t1 + [1] @t2 + [6]                 
                                         =  subtrees#2(subtrees(@t1),@t1,@t2,@x)    
          
              subtrees#2(@l1,@t1,@t2,@x) =  [1] @l1 + [1] @t2 + [6]                 
                                         >= [1] @l1 + [1] @t2 + [6]                 
                                         =  subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
          
          subtrees#3(@l2,@l1,@t1,@t2,@x) =  [1] @l1 + [1] @l2 + [6]                 
                                         >= [1] @l1 + [1] @l2 + [6]                 
                                         =  ::(node(@x,@t1,@t2),append(@l1,@l2))    
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: MI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
        - Weak TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            append#1(nil(),@l2) -> @l2
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):
        
        The following argument positions are considered usable:
          uargs(::) = {2},
          uargs(subtrees#2) = {1},
          uargs(subtrees#3) = {1}
        
        Following symbols are considered usable:
          {append,append#1,subtrees,subtrees#1,subtrees#2,subtrees#3}
        TcT has computed the following interpretation:
                  p(::) = [1 0] x_2 + [0]                        
                          [0 1]       [2]                        
              p(append) = [0 2] x_1 + [1 4] x_2 + [0]            
                          [0 1]       [0 1]       [0]            
            p(append#1) = [0 2] x_1 + [1 4] x_2 + [0]            
                          [0 1]       [0 1]       [0]            
                p(leaf) = [2]                                    
                          [4]                                    
                 p(nil) = [0]                                    
                          [4]                                    
                p(node) = [1 0] x_1 + [1 1] x_2 + [1 3] x_3 + [0]
                          [0 0]       [0 1]       [0 1]       [2]
            p(subtrees) = [4 0] x_1 + [0]                        
                          [0 1]       [0]                        
          p(subtrees#1) = [4 0] x_1 + [0]                        
                          [0 1]       [0]                        
          p(subtrees#2) = [1 4] x_1 + [4 5] x_3 + [4 0] x_4 + [0]
                          [0 1]       [0 1]       [0 0]       [2]
          p(subtrees#3) = [1 5] x_1 + [0 2] x_2 + [0]            
                          [0 1]       [0 1]       [2]            
        
        Following rules are strictly oriented:
        append#1(::(@x,@xs),@l2) = [1 4] @l2 + [0 2] @xs + [4]
                                   [0 1]       [0 1]       [2]
                                 > [1 4] @l2 + [0 2] @xs + [0]
                                   [0 1]       [0 1]       [2]
                                 = ::(@x,append(@xs,@l2))     
        
        
        Following rules are (at-least) weakly oriented:
                       append(@l1,@l2) =  [0 2] @l1 + [1 4] @l2 + [0]             
                                          [0 1]       [0 1]       [0]             
                                       >= [0 2] @l1 + [1 4] @l2 + [0]             
                                          [0 1]       [0 1]       [0]             
                                       =  append#1(@l1,@l2)                       
        
                   append#1(nil(),@l2) =  [1 4] @l2 + [8]                         
                                          [0 1]       [4]                         
                                       >= [1 0] @l2 + [0]                         
                                          [0 1]       [0]                         
                                       =  @l2                                     
        
                          subtrees(@t) =  [4 0] @t + [0]                          
                                          [0 1]      [0]                          
                                       >= [4 0] @t + [0]                          
                                          [0 1]      [0]                          
                                       =  subtrees#1(@t)                          
        
                    subtrees#1(leaf()) =  [8]                                     
                                          [4]                                     
                                       >= [0]                                     
                                          [4]                                     
                                       =  nil()                                   
        
          subtrees#1(node(@x,@t1,@t2)) =  [4 4] @t1 + [4 12] @t2 + [4 0] @x + [0] 
                                          [0 1]       [0  1]       [0 0]      [2] 
                                       >= [4 4] @t1 + [4 5] @t2 + [4 0] @x + [0]  
                                          [0 1]       [0 1]       [0 0]      [2]  
                                       =  subtrees#2(subtrees(@t1),@t1,@t2,@x)    
        
            subtrees#2(@l1,@t1,@t2,@x) =  [1 4] @l1 + [4 5] @t2 + [4 0] @x + [0]  
                                          [0 1]       [0 1]       [0 0]      [2]  
                                       >= [0 2] @l1 + [4 5] @t2 + [0]             
                                          [0 1]       [0 1]       [2]             
                                       =  subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
        
        subtrees#3(@l2,@l1,@t1,@t2,@x) =  [0 2] @l1 + [1 5] @l2 + [0]             
                                          [0 1]       [0 1]       [2]             
                                       >= [0 2] @l1 + [1 4] @l2 + [0]             
                                          [0 1]       [0 1]       [2]             
                                       =  ::(node(@x,@t1,@t2),append(@l1,@l2))    
        
* Step 8: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            append(@l1,@l2) -> append#1(@l1,@l2)
            append#1(::(@x,@xs),@l2) -> ::(@x,append(@xs,@l2))
            append#1(nil(),@l2) -> @l2
            subtrees(@t) -> subtrees#1(@t)
            subtrees#1(leaf()) -> nil()
            subtrees#1(node(@x,@t1,@t2)) -> subtrees#2(subtrees(@t1),@t1,@t2,@x)
            subtrees#2(@l1,@t1,@t2,@x) -> subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x)
            subtrees#3(@l2,@l1,@t1,@t2,@x) -> ::(node(@x,@t1,@t2),append(@l1,@l2))
        - Signature:
            {append/2,append#1/2,subtrees/1,subtrees#1/1,subtrees#2/4,subtrees#3/5} / {::/2,leaf/0,nil/0,node/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,append#1,subtrees,subtrees#1,subtrees#2
            ,subtrees#3} and constructors {::,leaf,nil,node}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))