* Step 1: Sum WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            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 TRS:
            <=(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 runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
            ,Nil,S,True}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            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 TRS:
            <=(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 runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
            ,Nil,S,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) = {2},
            uargs(merge[Ite]) = {1}
          
          Following symbols are considered usable:
            all
          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(),xs',Cons(x,xs)) =  [4] xs + [4] xs' + [3]                      
                                             >= [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.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            goal(xs,ys) -> merge(xs,ys)
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
        - Weak TRS:
            <=(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 runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
            ,Nil,S,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) = {2},
            uargs(merge[Ite]) = {1}
          
          Following symbols are considered usable:
            all
          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(),xs',Cons(x,xs)) =  [4] xs + [4] xs' + [0]                      
                                             >= [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.
* Step 4: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            merge(Cons(x',xs'),Cons(x,xs)) -> merge[Ite](<=(x',x),Cons(x',xs'),Cons(x,xs))
        - Weak TRS:
            <=(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 runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
            ,Nil,S,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) = {2},
            uargs(merge[Ite]) = {1}
          
          Following symbols are considered usable:
            all
          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(),xs',Cons(x,xs)) =  [4] xs + [4] xs' + [6]
                                             >= [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.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            <=(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 runtime complexity wrt. defined symbols {<=,goal,merge,merge[Ite]} and constructors {0,Cons,False
            ,Nil,S,True}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))