WORST_CASE(?,O(n^1))
* Step 1: WeightGap 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:
        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(Cons) = {1,2},
            uargs(f[Ite][False][Ite]) = {1},
            uargs(g[Ite][False][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p(Cons) = [1] x1 + [1] x2 + [0]
                         p(False) = [0]                  
                           p(Nil) = [0]                  
                          p(True) = [0]                  
                             p(f) = [0]                  
            p(f[Ite][False][Ite]) = [1] x1 + [0]         
                             p(g) = [0]                  
            p(g[Ite][False][Ite]) = [1] x1 + [0]         
                          p(goal) = [0]                  
                           p(lt0) = [3]                  
                      p(notEmpty) = [0]                  
                       p(number4) = [1]                  
          
          Following rules are strictly oriented:
                    lt0(x,Nil()) = [3]                                                  
                                 > [0]                                                  
                                 = False()                                              
          
          lt0(Nil(),Cons(x',xs)) = [3]                                                  
                                 > [0]                                                  
                                 = True()                                               
          
                      number4(n) = [1]                                                  
                                 > [0]                                                  
                                 = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
          
          
          Following rules are (at-least) weakly oriented:
                                  f(x,Cons(x',xs)) =  [0]                                                       
                                                   >= [3]                                                       
                                                   =  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)) =  [0]                                                       
                                                   >= [3]                                                       
                                                   =  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) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
          
                      lt0(Cons(x',xs'),Cons(x,xs)) =  [3]                                                       
                                                   >= [3]                                                       
                                                   =  lt0(xs',xs)                                               
          
                              notEmpty(Cons(x,xs)) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  True()                                                    
          
                                   notEmpty(Nil()) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  False()                                                   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap 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(Cons(x',xs'),Cons(x,xs)) -> lt0(xs',xs)
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
        - 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)
            lt0(x,Nil()) -> False()
            lt0(Nil(),Cons(x',xs)) -> True()
            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:
        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(Cons) = {1,2},
            uargs(f[Ite][False][Ite]) = {1},
            uargs(g[Ite][False][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p(Cons) = [1] x1 + [1] x2 + [1]         
                         p(False) = [4]                           
                           p(Nil) = [0]                           
                          p(True) = [3]                           
                             p(f) = [2] x2 + [1]                  
            p(f[Ite][False][Ite]) = [1] x1 + [2] x3 + [5]         
                             p(g) = [1] x1 + [1] x2 + [4]         
            p(g[Ite][False][Ite]) = [1] x1 + [1] x2 + [1] x3 + [4]
                          p(goal) = [5] x1 + [4] x2 + [2]         
                           p(lt0) = [2] x2 + [6]                  
                      p(notEmpty) = [1] x1 + [3]                  
                       p(number4) = [1] x1 + [4]                  
          
          Following rules are strictly oriented:
          lt0(Cons(x',xs'),Cons(x,xs)) = [2] x + [2] xs + [8]
                                       > [2] xs + [6]        
                                       = lt0(xs',xs)         
          
                  notEmpty(Cons(x,xs)) = [1] x + [1] xs + [4]
                                       > [3]                 
                                       = True()              
          
          
          Following rules are (at-least) weakly oriented:
                                  f(x,Cons(x',xs)) =  [2] x' + [2] xs + [3]                                     
                                                   >= [2] x' + [2] xs + [15]                                    
                                                   =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
          
                                        f(x,Nil()) =  [1]                                                       
                                                   >= [4]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
          f[Ite][False][Ite](False(),Cons(x,xs),y) =  [2] y + [9]                                               
                                                   >= [2] y + [5]                                               
                                                   =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [2] x + [2] xs + [10]                                     
                                                   >= [2] xs + [1]                                              
                                                   =  f(x',xs)                                                  
          
                                  g(x,Cons(x',xs)) =  [1] x + [1] x' + [1] xs + [5]                             
                                                   >= [1] x + [1] x' + [1] xs + [13]                            
                                                   =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
          
                                        g(x,Nil()) =  [1] x + [4]                                               
                                                   >= [4]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
          g[Ite][False][Ite](False(),Cons(x,xs),y) =  [1] x + [1] xs + [1] y + [9]                              
                                                   >= [1] xs + [1] y + [6]                                      
                                                   =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [1] x + [1] x' + [1] xs + [8]                             
                                                   >= [1] x' + [1] xs + [4]                                     
                                                   =  g(x',xs)                                                  
          
                                         goal(x,y) =  [5] x + [4] y + [2]                                       
                                                   >= [1] x + [3] y + [7]                                       
                                                   =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
          
                                      lt0(x,Nil()) =  [6]                                                       
                                                   >= [4]                                                       
                                                   =  False()                                                   
          
                            lt0(Nil(),Cons(x',xs)) =  [2] x' + [2] xs + [8]                                     
                                                   >= [3]                                                       
                                                   =  True()                                                    
          
                                   notEmpty(Nil()) =  [3]                                                       
                                                   >= [4]                                                       
                                                   =  False()                                                   
          
                                        number4(n) =  [1] n + [4]                                               
                                                   >= [4]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap 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()))
            notEmpty(Nil()) -> False()
        - 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)
            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()
            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:
        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(Cons) = {1,2},
            uargs(f[Ite][False][Ite]) = {1},
            uargs(g[Ite][False][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p(Cons) = [1] x1 + [1] x2 + [0]
                         p(False) = [1]                  
                           p(Nil) = [0]                  
                          p(True) = [1]                  
                             p(f) = [0]                  
            p(f[Ite][False][Ite]) = [1] x1 + [5]         
                             p(g) = [1]                  
            p(g[Ite][False][Ite]) = [1] x1 + [0]         
                          p(goal) = [3] x2 + [0]         
                           p(lt0) = [1]                  
                      p(notEmpty) = [1]                  
                       p(number4) = [4]                  
          
          Following rules are strictly oriented:
          g(x,Nil()) = [1]                                                  
                     > [0]                                                  
                     = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
          
          
          Following rules are (at-least) weakly oriented:
                                  f(x,Cons(x',xs)) =  [0]                                                       
                                                   >= [6]                                                       
                                                   =  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) =  [6]                                                       
                                                   >= [0]                                                       
                                                   =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [6]                                                       
                                                   >= [0]                                                       
                                                   =  f(x',xs)                                                  
          
                                  g(x,Cons(x',xs)) =  [1]                                                       
                                                   >= [1]                                                       
                                                   =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
          
          g[Ite][False][Ite](False(),Cons(x,xs),y) =  [1]                                                       
                                                   >= [1]                                                       
                                                   =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [1]                                                       
                                                   >= [1]                                                       
                                                   =  g(x',xs)                                                  
          
                                         goal(x,y) =  [3] y + [0]                                               
                                                   >= [1]                                                       
                                                   =  Cons(f(x,y),Cons(g(x,y),Nil()))                           
          
                                      lt0(x,Nil()) =  [1]                                                       
                                                   >= [1]                                                       
                                                   =  False()                                                   
          
                      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]                                                       
                                                   >= [1]                                                       
                                                   =  True()                                                    
          
                                   notEmpty(Nil()) =  [1]                                                       
                                                   >= [1]                                                       
                                                   =  False()                                                   
          
                                        number4(n) =  [4]                                                       
                                                   >= [0]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap 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))
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),Nil()))
            notEmpty(Nil()) -> False()
        - 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(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)
            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()
            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:
        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(Cons) = {1,2},
            uargs(f[Ite][False][Ite]) = {1},
            uargs(g[Ite][False][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p(Cons) = [1] x1 + [1] x2 + [0]
                         p(False) = [0]                  
                           p(Nil) = [0]                  
                          p(True) = [0]                  
                             p(f) = [4]                  
            p(f[Ite][False][Ite]) = [1] x1 + [4]         
                             p(g) = [2]                  
            p(g[Ite][False][Ite]) = [1] x1 + [3]         
                          p(goal) = [1]                  
                           p(lt0) = [0]                  
                      p(notEmpty) = [4] x1 + [5]         
                       p(number4) = [0]                  
          
          Following rules are strictly oriented:
               f(x,Nil()) = [4]                                                  
                          > [0]                                                  
                          = Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))
          
          notEmpty(Nil()) = [5]                                                  
                          > [0]                                                  
                          = False()                                              
          
          
          Following rules are (at-least) weakly oriented:
                                  f(x,Cons(x',xs)) =  [4]                                                       
                                                   >= [4]                                                       
                                                   =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
          
          f[Ite][False][Ite](False(),Cons(x,xs),y) =  [4]                                                       
                                                   >= [4]                                                       
                                                   =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [4]                                                       
                                                   >= [4]                                                       
                                                   =  f(x',xs)                                                  
          
                                  g(x,Cons(x',xs)) =  [2]                                                       
                                                   >= [3]                                                       
                                                   =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
          
                                        g(x,Nil()) =  [2]                                                       
                                                   >= [0]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
          g[Ite][False][Ite](False(),Cons(x,xs),y) =  [3]                                                       
                                                   >= [2]                                                       
                                                   =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [3]                                                       
                                                   >= [2]                                                       
                                                   =  g(x',xs)                                                  
          
                                         goal(x,y) =  [1]                                                       
                                                   >= [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()                                                    
          
                              notEmpty(Cons(x,xs)) =  [4] x + [4] xs + [5]                                      
                                                   >= [0]                                                       
                                                   =  True()                                                    
          
                                        number4(n) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap 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))
            goal(x,y) -> Cons(f(x,y),Cons(g(x,y),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(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)
            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:
        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(Cons) = {1,2},
            uargs(f[Ite][False][Ite]) = {1},
            uargs(g[Ite][False][Ite]) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                          p(Cons) = [1] x1 + [1] x2 + [0]
                         p(False) = [0]                  
                           p(Nil) = [0]                  
                          p(True) = [0]                  
                             p(f) = [0]                  
            p(f[Ite][False][Ite]) = [1] x1 + [0]         
                             p(g) = [5] x1 + [0]         
            p(g[Ite][False][Ite]) = [1] x1 + [5] x2 + [0]
                          p(goal) = [5] x1 + [1]         
                           p(lt0) = [0]                  
                      p(notEmpty) = [0]                  
                       p(number4) = [0]                  
          
          Following rules are strictly oriented:
          goal(x,y) = [5] x + [1]                    
                    > [5] x + [0]                    
                    = Cons(f(x,y),Cons(g(x,y),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)) =  [5] x + [0]                                               
                                                   >= [5] x + [0]                                               
                                                   =  g[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
          
                                        g(x,Nil()) =  [5] x + [0]                                               
                                                   >= [0]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
          g[Ite][False][Ite](False(),Cons(x,xs),y) =  [5] x + [5] xs + [0]                                      
                                                   >= [5] xs + [0]                                              
                                                   =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
          
          g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [5] x' + [0]                                              
                                                   >= [5] x' + [0]                                              
                                                   =  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)) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  True()                                                    
          
                                   notEmpty(Nil()) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  False()                                                   
          
                                        number4(n) =  [0]                                                       
                                                   >= [0]                                                       
                                                   =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: 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))
        - 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()))
            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:
        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) = [8]                            
          p(f[Ite][False][Ite]) = [8] x1 + [8]                   
                           p(g) = [11] x1 + [4] x2 + [4]         
          p(g[Ite][False][Ite]) = [8] x1 + [11] x2 + [4] x3 + [1]
                        p(goal) = [11] x1 + [4] x2 + [14]        
                         p(lt0) = [0]                            
                    p(notEmpty) = [1] x1 + [3]                   
                     p(number4) = [1] x1 + [4]                   
        
        Following rules are strictly oriented:
        g(x,Cons(x',xs)) = [11] x + [4] x' + [4] xs + [8]                            
                         > [11] x + [4] x' + [4] xs + [5]                            
                         = 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)) =  [8]                                                       
                                                 >= [8]                                                       
                                                 =  f[Ite][False][Ite](lt0(x,Cons(Nil(),Nil())),x,Cons(x',xs))
        
                                      f(x,Nil()) =  [8]                                                       
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  [8]                                                       
                                                 >= [8]                                                       
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [8]                                                       
                                                 >= [8]                                                       
                                                 =  f(x',xs)                                                  
        
                                      g(x,Nil()) =  [11] x + [4]                                              
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        g[Ite][False][Ite](False(),Cons(x,xs),y) =  [11] x + [11] xs + [4] y + [12]                           
                                                 >= [11] xs + [4] y + [12]                                    
                                                 =  g(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        g[Ite][False][Ite](True(),x',Cons(x,xs)) =  [4] x + [11] x' + [4] xs + [5]                            
                                                 >= [11] x' + [4] xs + [4]                                    
                                                 =  g(x',xs)                                                  
        
                                       goal(x,y) =  [11] x + [4] y + [14]                                     
                                                 >= [11] x + [4] y + [14]                                     
                                                 =  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)) =  [1] x + [1] xs + [4]                                      
                                                 >= [0]                                                       
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  [3]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                                      number4(n) =  [1] n + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
* Step 7: 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))
        - 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,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:
        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) = [8] x1 + [2] x2 + [4]         
          p(f[Ite][False][Ite]) = [8] x1 + [8] x2 + [2] x3 + [2]
                           p(g) = [4]                           
          p(g[Ite][False][Ite]) = [1] x1 + [4]                  
                        p(goal) = [8] x1 + [8] x2 + [10]        
                         p(lt0) = [0]                           
                    p(notEmpty) = [8] x1 + [6]                  
                     p(number4) = [2] x1 + [4]                  
        
        Following rules are strictly oriented:
        f(x,Cons(x',xs)) = [8] x + [2] x' + [2] xs + [6]                             
                         > [8] x + [2] x' + [2] 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()) =  [8] x + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
        f[Ite][False][Ite](False(),Cons(x,xs),y) =  [8] x + [8] xs + [2] y + [10]                             
                                                 >= [8] xs + [2] y + [8]                                      
                                                 =  f(xs,Cons(Cons(Nil(),Nil()),y))                           
        
        f[Ite][False][Ite](True(),x',Cons(x,xs)) =  [2] x + [8] x' + [2] xs + [4]                             
                                                 >= [8] x' + [2] 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) =  [8] x + [8] y + [10]                                      
                                                 >= [8] x + [2] 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)) =  [8] x + [8] xs + [14]                                     
                                                 >= [0]                                                       
                                                 =  True()                                                    
        
                                 notEmpty(Nil()) =  [6]                                                       
                                                 >= [0]                                                       
                                                 =  False()                                                   
        
                                      number4(n) =  [2] n + [4]                                               
                                                 >= [4]                                                       
                                                 =  Cons(Nil(),Cons(Nil(),Cons(Nil(),Cons(Nil(),Nil()))))     
        
* Step 8: 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(?,O(n^1))