*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        goal(xs,ys) -> merge(xs,ys)
        merge(Cons(x,xs),Nil()) -> Cons(x,xs)
        merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
        merge(Nil(),ys) -> ys
      Weak DP Rules:
        
      Weak TRS Rules:
        <=(0(),y) -> True()
        <=(S(x),0()) -> False()
        <=(S(x),S(y)) -> <=(x,y)
        merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
        merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
      Signature:
        {<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {<=,goal,merge,merge[Ite]}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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) = {2},
          uargs(merge[Ite]) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                   p(0) = [0]                           
                  p(<=) = [3]                           
                p(Cons) = [1] x2 + [0]                  
               p(False) = [3]                           
                 p(Nil) = [3]                           
                   p(S) = [1]                           
                p(True) = [3]                           
                p(goal) = [4] x1 + [4] x2 + [0]         
               p(merge) = [4] x1 + [4] x2 + [3]         
          p(merge[Ite]) = [1] x1 + [4] x2 + [4] x3 + [0]
        
        Following rules are strictly oriented:
        merge(Cons(x,xs),Nil()) = [4] xs + [15]
                                > [1] xs + [0] 
                                = Cons(x,xs)   
        
                merge(Nil(),ys) = [4] ys + [15]
                                > [1] ys + [0] 
                                = ys           
        
        
        Following rules are (at-least) weakly oriented:
                               <=(0(),y) =  [3]                    
                                         >= [3]                    
                                         =  True()                 
        
                            <=(S(x),0()) =  [3]                    
                                         >= [3]                    
                                         =  False()                
        
                           <=(S(x),S(y)) =  [3]                    
                                         >= [3]                    
                                         =  <=(x,y)                
        
                             goal(xs,ys) =  [4] xs + [4] ys + [0]  
                                         >= [4] xs + [4] ys + [3]  
                                         =  merge(xs,ys)           
        
          merge(Cons(x',xs'),Cons(x,xs)) =  [4] xs + [4] xs' + [3] 
                                         >= [4] xs + [4] xs' + [3] 
                                         =  merge[Ite](<=(x',x)    
                                                      ,Cons(x',xs')
                                                      ,Cons(x,xs)) 
        
                      merge[Ite](False() =  [4] xs + [4] xs' + [3] 
                                    ,xs'                           
                            ,Cons(x,xs))                           
                                         >= [4] xs + [4] xs' + [3] 
                                         =  Cons(x,merge(xs',xs))  
        
        merge[Ite](True(),Cons(x,xs),ys) =  [4] xs + [4] ys + [3]  
                                         >= [4] xs + [4] ys + [3]  
                                         =  Cons(x,merge(xs,ys))   
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        goal(xs,ys) -> merge(xs,ys)
        merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
      Weak DP Rules:
        
      Weak TRS Rules:
        <=(0(),y) -> True()
        <=(S(x),0()) -> False()
        <=(S(x),S(y)) -> <=(x,y)
        merge(Cons(x,xs),Nil()) -> Cons(x,xs)
        merge(Nil(),ys) -> ys
        merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
        merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
      Signature:
        {<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {<=,goal,merge,merge[Ite]}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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) = {2},
          uargs(merge[Ite]) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                   p(0) = [0]                           
                  p(<=) = [3]                           
                p(Cons) = [1] x2 + [0]                  
               p(False) = [0]                           
                 p(Nil) = [2]                           
                   p(S) = [0]                           
                p(True) = [0]                           
                p(goal) = [4] x1 + [6] x2 + [1]         
               p(merge) = [4] x1 + [4] x2 + [0]         
          p(merge[Ite]) = [1] x1 + [4] x2 + [4] x3 + [0]
        
        Following rules are strictly oriented:
        goal(xs,ys) = [4] xs + [6] ys + [1]
                    > [4] xs + [4] ys + [0]
                    = merge(xs,ys)         
        
        
        Following rules are (at-least) weakly oriented:
                               <=(0(),y) =  [3]                    
                                         >= [0]                    
                                         =  True()                 
        
                            <=(S(x),0()) =  [3]                    
                                         >= [0]                    
                                         =  False()                
        
                           <=(S(x),S(y)) =  [3]                    
                                         >= [3]                    
                                         =  <=(x,y)                
        
                 merge(Cons(x,xs),Nil()) =  [4] xs + [8]           
                                         >= [1] xs + [0]           
                                         =  Cons(x,xs)             
        
          merge(Cons(x',xs'),Cons(x,xs)) =  [4] xs + [4] xs' + [0] 
                                         >= [4] xs + [4] xs' + [3] 
                                         =  merge[Ite](<=(x',x)    
                                                      ,Cons(x',xs')
                                                      ,Cons(x,xs)) 
        
                         merge(Nil(),ys) =  [4] ys + [8]           
                                         >= [1] ys + [0]           
                                         =  ys                     
        
                      merge[Ite](False() =  [4] xs + [4] xs' + [0] 
                                    ,xs'                           
                            ,Cons(x,xs))                           
                                         >= [4] xs + [4] xs' + [0] 
                                         =  Cons(x,merge(xs',xs))  
        
        merge[Ite](True(),Cons(x,xs),ys) =  [4] xs + [4] ys + [0]  
                                         >= [4] xs + [4] ys + [0]  
                                         =  Cons(x,merge(xs,ys))   
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
      Weak DP Rules:
        
      Weak TRS Rules:
        <=(0(),y) -> True()
        <=(S(x),0()) -> False()
        <=(S(x),S(y)) -> <=(x,y)
        goal(xs,ys) -> merge(xs,ys)
        merge(Cons(x,xs),Nil()) -> Cons(x,xs)
        merge(Nil(),ys) -> ys
        merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
        merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
      Signature:
        {<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {<=,goal,merge,merge[Ite]}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      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) = {2},
          uargs(merge[Ite]) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                   p(0) = [1]                           
                  p(<=) = [4]                           
                p(Cons) = [1] x2 + [1]                  
               p(False) = [2]                           
                 p(Nil) = [0]                           
                   p(S) = [1] x1 + [2]                  
                p(True) = [4]                           
                p(goal) = [6] x1 + [4] x2 + [5]         
               p(merge) = [4] x1 + [4] x2 + [5]         
          p(merge[Ite]) = [1] x1 + [4] x2 + [4] x3 + [0]
        
        Following rules are strictly oriented:
        merge(Cons(x',xs'),Cons(x,xs)) = [4] xs + [4] xs' + [13]
                                       > [4] xs + [4] xs' + [12]
                                       = merge[Ite](<=(x',x)    
                                                   ,Cons(x',xs')
                                                   ,Cons(x,xs)) 
        
        
        Following rules are (at-least) weakly oriented:
                               <=(0(),y) =  [4]                   
                                         >= [4]                   
                                         =  True()                
        
                            <=(S(x),0()) =  [4]                   
                                         >= [2]                   
                                         =  False()               
        
                           <=(S(x),S(y)) =  [4]                   
                                         >= [4]                   
                                         =  <=(x,y)               
        
                             goal(xs,ys) =  [6] xs + [4] ys + [5] 
                                         >= [4] xs + [4] ys + [5] 
                                         =  merge(xs,ys)          
        
                 merge(Cons(x,xs),Nil()) =  [4] xs + [9]          
                                         >= [1] xs + [1]          
                                         =  Cons(x,xs)            
        
                         merge(Nil(),ys) =  [4] ys + [5]          
                                         >= [1] ys + [0]          
                                         =  ys                    
        
                      merge[Ite](False() =  [4] xs + [4] xs' + [6]
                                    ,xs'                          
                            ,Cons(x,xs))                          
                                         >= [4] xs + [4] xs' + [6]
                                         =  Cons(x,merge(xs',xs)) 
        
        merge[Ite](True(),Cons(x,xs),ys) =  [4] xs + [4] ys + [8] 
                                         >= [4] xs + [4] ys + [6] 
                                         =  Cons(x,merge(xs,ys))  
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        <=(0(),y) -> True()
        <=(S(x),0()) -> False()
        <=(S(x),S(y)) -> <=(x,y)
        goal(xs,ys) -> merge(xs,ys)
        merge(Cons(x,xs),Nil()) -> Cons(x,xs)
        merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
        merge(Nil(),ys) -> ys
        merge[Ite](False(),xs',Cons(x,xs)) -> Cons(x,merge(xs',xs))
        merge[Ite](True(),Cons(x,xs),ys) -> Cons(x,merge(xs,ys))
      Signature:
        {<=/2,goal/2,merge/2,merge[Ite]/3} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {<=,goal,merge,merge[Ite]}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).