WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Weak TRS:
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Weak TRS:
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          lt0(y,u){y -> Cons(x,y),u -> Cons(z,u)} =
            lt0(Cons(x,y),Cons(z,u)) ->^+ lt0(y,u)
              = C[lt0(y,u) = lt0(y,u){}]

** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Weak TRS:
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(f[Ite][False][Ite]) = {1},
          uargs(g[Ite][False][Ite]) = {1}
        
        Following symbols are considered usable:
          {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4}
        TcT has computed the following interpretation:
                        p(Cons) = x1 + x2
                       p(False) = 0      
                         p(Nil) = 0      
                        p(True) = 0      
                           p(f) = 6      
          p(f[Ite][False][Ite]) = 6 + x1 
                           p(g) = 0      
          p(g[Ite][False][Ite]) = x1     
                        p(goal) = 6 + x2 
                         p(lt0) = 0      
                    p(notEmpty) = 3      
                     p(number4) = 0      
        
        Following rules are strictly oriented:
                  f(x,Nil()) = 6                                                    
                             > 0                                                    
                             = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        
        notEmpty(Cons(x,xs)) = 3                                                    
                             > 0                                                    
                             = True()                                               
        
             notEmpty(Nil()) = 3                                                    
                             > 0                                                    
                             = False()                                              
        
        
        Following rules are (at-least) weakly oriented:
                                f(x,Cons(x',xs)) =  6                                                         
                                                 >= 6                                                         
                                                 =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  6                                                         
                                                 >= 6                                                         
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  6                                                         
                                                 >= 6                                                         
                                                 =  f(x',xs)                                                  
        
                                g(x,Cons(x',xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      g(x,Nil()) =  0                                                         
                                                 >= 0                                                         
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  0                                                         
                                                 >= 0                                                         
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  g(x',xs)                                                  
        
                                       goal(x,y) =  6 + y                                                     
                                                 >= 6                                                         
                                                 =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
        
                                    lt0(x,Nil()) =  0                                                         
                                                 >= 0                                                         
                                                 =  False()                                                   
        
                    lt0(Cons(x',xs'),Cons(x,xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  lt0(xs',xs)                                               
        
                          lt0(Nil(),Cons(x',xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  True()                                                    
        
                                      number4(n) =  0                                                         
                                                 >= 0                                                         
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Weak TRS:
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(f[Ite][False][Ite]) = {1},
          uargs(g[Ite][False][Ite]) = {1}
        
        Following symbols are considered usable:
          {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4}
        TcT has computed the following interpretation:
                        p(Cons) = x1 + x2      
                       p(False) = 0            
                         p(Nil) = 0            
                        p(True) = 0            
                           p(f) = 0            
          p(f[Ite][False][Ite]) = 2*x1         
                           p(g) = 2 + 6*x2     
          p(g[Ite][False][Ite]) = 2 + x1 + 6*x3
                        p(goal) = 6 + 6*x2     
                         p(lt0) = 0            
                    p(notEmpty) = 7 + x1       
                     p(number4) = 4            
        
        Following rules are strictly oriented:
        g(x,Nil()) = 2                                                    
                   > 0                                                    
                   = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        
         goal(x,y) = 6 + 6*y                                              
                   > 2 + 6*y                                              
                   = Cons(f(x,y),Cons(g(x,y),Nil()))                      
        
        number4(n) = 4                                                    
                   > 0                                                    
                   = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        
        
        Following rules are (at-least) weakly oriented:
                                f(x,Cons(x',xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      f(x,Nil()) =  0                                                         
                                                 >= 0                                                         
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  0                                                         
                                                 >= 0                                                         
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  f(x',xs)                                                  
        
                                g(x,Cons(x',xs)) =  2 + 6*x' + 6*xs                                           
                                                 >= 2 + 6*x' + 6*xs                                           
                                                 =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  2 + 6*y                                                   
                                                 >= 2 + 6*y                                                   
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  2 + 6*x + 6*xs                                            
                                                 >= 2 + 6*xs                                                  
                                                 =  g(x',xs)                                                  
        
                                    lt0(x,Nil()) =  0                                                         
                                                 >= 0                                                         
                                                 =  False()                                                   
        
                    lt0(Cons(x',xs'),Cons(x,xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  lt0(xs',xs)                                               
        
                          lt0(Nil(),Cons(x',xs)) =  0                                                         
                                                 >= 0                                                         
                                                 =  True()                                                    
        
                            notEmpty(Cons(x,xs)) =  7 + x + xs                                                
                                                 >= 0                                                         
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  7                                                         
                                                 >= 0                                                         
                                                 =  False()                                                   
        
** Step 1.b:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
        - Weak TRS:
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(f[Ite][False][Ite]) = {1},
          uargs(g[Ite][False][Ite]) = {1}
        
        Following symbols are considered usable:
          {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4}
        TcT has computed the following interpretation:
                        p(Cons) = [1] x1 + [1] x2 + [1]         
                       p(False) = [0]                           
                         p(Nil) = [0]                           
                        p(True) = [0]                           
                           p(f) = [4] x1 + [1] x2 + [4]         
          p(f[Ite][False][Ite]) = [8] x1 + [4] x2 + [1] x3 + [3]
                           p(g) = [4]                           
          p(g[Ite][False][Ite]) = [2] x1 + [4]                  
                        p(goal) = [5] x1 + [1] x2 + [10]        
                         p(lt0) = [0]                           
                    p(notEmpty) = [11] x1 + [8]                 
                     p(number4) = [1] x1 + [6]                  
        
        Following rules are strictly oriented:
        f(x,Cons(x',xs)) = [4] x + [1] x' + [1] xs + [5]                             
                         > [4] x + [1] x' + [1] xs + [4]                             
                         = f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
        
        Following rules are (at-least) weakly oriented:
                                      f(x,Nil()) =  [4] x + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  [4] x + [4] xs + [1] y + [7]                              
                                                 >= [4] xs + [1] y + [6]                                      
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [1] x + [4] x' + [1] xs + [4]                             
                                                 >= [4] x' + [1] xs + [4]                                     
                                                 =  f(x',xs)                                                  
        
                                g(x,Cons(x',xs)) =  [4]                                                       
                                                 >= [4]                                                       
                                                 =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      g(x,Nil()) =  [4]                                                       
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  [4]                                                       
                                                 >= [4]                                                       
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [4]                                                       
                                                 >= [4]                                                       
                                                 =  g(x',xs)                                                  
        
                                       goal(x,y) =  [5] x + [1] y + [10]                                      
                                                 >= [4] x + [1] y + [10]                                      
                                                 =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
        
                                    lt0(x,Nil()) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                    lt0(Cons(x',xs'),Cons(x,xs)) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  lt0(xs',xs)                                               
        
                          lt0(Nil(),Cons(x',xs)) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  True()                                                    
        
                            notEmpty(Cons(x,xs)) =  [11] x + [11] xs + [19]                                   
                                                 >= [0]                                                       
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  [8]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                                      number4(n) =  [1] n + [6]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
** Step 1.b:4: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
        - Weak TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(f[Ite][False][Ite]) = {1},
          uargs(g[Ite][False][Ite]) = {1}
        
        Following symbols are considered usable:
          {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4}
        TcT has computed the following interpretation:
                        p(Cons) = [1] x1 + [1] x2 + [1]         
                       p(False) = [0]                           
                         p(Nil) = [0]                           
                        p(True) = [0]                           
                           p(f) = [5] x1 + [4]                  
          p(f[Ite][False][Ite]) = [2] x1 + [5] x2 + [4]         
                           p(g) = [3] x1 + [1] x2 + [9]         
          p(g[Ite][False][Ite]) = [8] x1 + [3] x2 + [1] x3 + [8]
                        p(goal) = [8] x1 + [1] x2 + [15]        
                         p(lt0) = [0]                           
                    p(notEmpty) = [12] x1 + [10]                
                     p(number4) = [1] x1 + [4]                  
        
        Following rules are strictly oriented:
        g(x,Cons(x',xs)) = [3] x + [1] x' + [1] xs + [10]                            
                         > [3] x + [1] x' + [1] xs + [9]                             
                         = g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
        
        Following rules are (at-least) weakly oriented:
                                f(x,Cons(x',xs)) =  [5] x + [4]                                               
                                                 >= [5] x + [4]                                               
                                                 =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      f(x,Nil()) =  [5] x + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  [5] x + [5] xs + [9]                                      
                                                 >= [5] xs + [4]                                              
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [5] x' + [4]                                              
                                                 >= [5] x' + [4]                                              
                                                 =  f(x',xs)                                                  
        
                                      g(x,Nil()) =  [3] x + [9]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  [3] x + [3] xs + [1] y + [11]                             
                                                 >= [3] xs + [1] y + [11]                                     
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [1] x + [3] x' + [1] xs + [9]                             
                                                 >= [3] x' + [1] xs + [9]                                     
                                                 =  g(x',xs)                                                  
        
                                       goal(x,y) =  [8] x + [1] y + [15]                                      
                                                 >= [8] x + [1] y + [15]                                      
                                                 =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
        
                                    lt0(x,Nil()) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                    lt0(Cons(x',xs'),Cons(x,xs)) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  lt0(xs',xs)                                               
        
                          lt0(Nil(),Cons(x',xs)) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  True()                                                    
        
                            notEmpty(Cons(x,xs)) =  [12] x + [12] xs + [22]                                   
                                                 >= [0]                                                       
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  [10]                                                      
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                                      number4(n) =  [1] n + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
** Step 1.b:5: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
        - Weak TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(f[Ite][False][Ite]) = {1},
          uargs(g[Ite][False][Ite]) = {1}
        
        Following symbols are considered usable:
          {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4}
        TcT has computed the following interpretation:
                        p(Cons) = [1] x1 + [1] x2 + [1]  
                       p(False) = [0]                    
                         p(Nil) = [0]                    
                        p(True) = [1]                    
                           p(f) = [2] x1 + [4]           
          p(f[Ite][False][Ite]) = [2] x1 + [2] x2 + [2]  
                           p(g) = [8] x1 + [9]           
          p(g[Ite][False][Ite]) = [8] x1 + [8] x2 + [1]  
                        p(goal) = [10] x1 + [1] x2 + [15]
                         p(lt0) = [1]                    
                    p(notEmpty) = [1] x1 + [1]           
                     p(number4) = [4]                    
        
        Following rules are strictly oriented:
        lt0(x,Nil()) = [1]    
                     > [0]    
                     = False()
        
        
        Following rules are (at-least) weakly oriented:
                                f(x,Cons(x',xs)) =  [2] x + [4]                                               
                                                 >= [2] x + [4]                                               
                                                 =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      f(x,Nil()) =  [2] x + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  [2] x + [2] xs + [4]                                      
                                                 >= [2] xs + [4]                                              
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [2] x' + [4]                                              
                                                 >= [2] x' + [4]                                              
                                                 =  f(x',xs)                                                  
        
                                g(x,Cons(x',xs)) =  [8] x + [9]                                               
                                                 >= [8] x + [9]                                               
                                                 =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      g(x,Nil()) =  [8] x + [9]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  [8] x + [8] xs + [9]                                      
                                                 >= [8] xs + [9]                                              
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [8] x' + [9]                                              
                                                 >= [8] x' + [9]                                              
                                                 =  g(x',xs)                                                  
        
                                       goal(x,y) =  [10] x + [1] y + [15]                                     
                                                 >= [10] x + [15]                                             
                                                 =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
        
                    lt0(Cons(x',xs'),Cons(x,xs)) =  [1]                                                       
                                                 >= [1]                                                       
                                                 =  lt0(xs',xs)                                               
        
                          lt0(Nil(),Cons(x',xs)) =  [1]                                                       
                                                 >= [1]                                                       
                                                 =  True()                                                    
        
                            notEmpty(Cons(x,xs)) =  [1] x + [1] xs + [2]                                      
                                                 >= [1]                                                       
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  [1]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                                      number4(n) =  [4]                                                       
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
** Step 1.b:6: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
        - Weak TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            lt0(x,Nil()) -> False()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(Cons) = {1,2},
          uargs(f[Ite][False][Ite]) = {1},
          uargs(g[Ite][False][Ite]) = {1}
        
        Following symbols are considered usable:
          {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0,notEmpty,number4}
        TcT has computed the following interpretation:
                        p(Cons) = [1] x1 + [1] x2 + [1]         
                       p(False) = [0]                           
                         p(Nil) = [0]                           
                        p(True) = [1]                           
                           p(f) = [9] x1 + [2] x2 + [8]         
          p(f[Ite][False][Ite]) = [1] x1 + [9] x2 + [2] x3 + [5]
                           p(g) = [4] x1 + [1] x2 + [4]         
          p(g[Ite][False][Ite]) = [1] x1 + [4] x2 + [1] x3 + [2]
                        p(goal) = [13] x1 + [3] x2 + [14]       
                         p(lt0) = [2] x2 + [0]                  
                    p(notEmpty) = [1] x1 + [4]                  
                     p(number4) = [1] x1 + [4]                  
        
        Following rules are strictly oriented:
        lt0(Cons(x',xs'),Cons(x,xs)) = [2] x + [2] xs + [2] 
                                     > [2] xs + [0]         
                                     = lt0(xs',xs)          
        
              lt0(Nil(),Cons(x',xs)) = [2] x' + [2] xs + [2]
                                     > [1]                  
                                     = True()               
        
        
        Following rules are (at-least) weakly oriented:
                                f(x,Cons(x',xs)) =  [9] x + [2] x' + [2] xs + [10]                            
                                                 >= [9] x + [2] x' + [2] xs + [9]                             
                                                 =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      f(x,Nil()) =  [9] x + [8]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  [9] x + [9] xs + [2] y + [14]                             
                                                 >= [9] xs + [2] y + [12]                                     
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [2] x + [9] x' + [2] xs + [8]                             
                                                 >= [9] x' + [2] xs + [8]                                     
                                                 =  f(x',xs)                                                  
        
                                g(x,Cons(x',xs)) =  [4] x + [1] x' + [1] xs + [5]                             
                                                 >= [4] x + [1] x' + [1] xs + [5]                             
                                                 =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      g(x,Nil()) =  [4] x + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  [4] x + [4] xs + [1] y + [6]                              
                                                 >= [4] xs + [1] y + [6]                                      
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [1] x + [4] x' + [1] xs + [4]                             
                                                 >= [4] x' + [1] xs + [4]                                     
                                                 =  g(x',xs)                                                  
        
                                       goal(x,y) =  [13] x + [3] y + [14]                                     
                                                 >= [13] x + [3] y + [14]                                     
                                                 =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
        
                                    lt0(x,Nil()) =  [0]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                            notEmpty(Cons(x,xs)) =  [1] x + [1] xs + [5]                                      
                                                 >= [1]                                                       
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  [4]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                                      number4(n) =  [1] n + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
** Step 1.b:7: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            f(x,Cons(x',xs)) -> f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            f(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            f[Ite][False][Ite](False(),Cons(x,xs),y) -> f(xs,Cons(Cons(Nil(),Nil()),y))
            f[Ite][False][Ite](True(),x',Cons(x,xs)) -> f(x',xs)
            g(x,Cons(x',xs)) -> g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
            g(x,Nil()) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
            g[Ite][False][Ite](False(),Cons(x,xs),y) -> g(xs,Cons(Cons(Nil(),Nil()),y))
            g[Ite][False][Ite](True(),x',Cons(x,xs)) -> g(x',xs)
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            lt0(x,Nil()) -> False()
            lt0(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            lt0(Nil(),Cons(x',xs)) -> True()
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            number4(n) -> Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
        - Signature:
            {f/2,f[Ite][False][Ite]/3,g/2,g[Ite][False][Ite]/3,goal/2,lt0/2,notEmpty/1,number4/1} / {Cons/2,False/0
            ,Nil/0,True/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,f[Ite][False][Ite],g,g[Ite][False][Ite],goal,lt0
            ,notEmpty,number4} and constructors {Cons,False,Nil,True}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))