*** 1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        loop(Cons(x,xs),Nil(),pp,ss) -> False()
        loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
        loop(Nil(),s,pp,ss) -> True()
        match1(p,s) -> loop(p,s,p,s)
      Weak DP Rules:
        
      Weak TRS Rules:
        !EQ(0(),0()) -> True()
        !EQ(0(),S(y)) -> False()
        !EQ(S(x),0()) -> False()
        !EQ(S(x),S(y)) -> !EQ(x,y)
        loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
        loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
      Signature:
        {!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {!EQ,loop,loop[Ite],match1}/{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(loop[Ite]) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                p(!EQ) = [1]                           
                  p(0) = [0]                           
               p(Cons) = [1]                           
              p(False) = [1]                           
                p(Nil) = [0]                           
                  p(S) = [0]                           
               p(True) = [0]                           
               p(loop) = [1]                           
          p(loop[Ite]) = [1] x1 + [2] x2 + [2] x3 + [4]
             p(match1) = [1]                           
        
        Following rules are strictly oriented:
        loop(Nil(),s,pp,ss) = [1]   
                            > [0]   
                            = True()
        
        
        Following rules are (at-least) weakly oriented:
                        !EQ(0(),0()) =  [1]                   
                                     >= [0]                   
                                     =  True()                
        
                       !EQ(0(),S(y)) =  [1]                   
                                     >= [1]                   
                                     =  False()               
        
                       !EQ(S(x),0()) =  [1]                   
                                     >= [1]                   
                                     =  False()               
        
                      !EQ(S(x),S(y)) =  [1]                   
                                     >= [1]                   
                                     =  !EQ(x,y)              
        
        loop(Cons(x,xs),Nil(),pp,ss) =  [1]                   
                                     >= [1]                   
                                     =  False()               
        
                   loop(Cons(x',xs') =  [1]                   
                         ,Cons(x,xs)                          
                                 ,pp                          
                                ,ss)                          
                                     >= [9]                   
                                     =  loop[Ite](!EQ(x',x)   
                                                 ,Cons(x',xs')
                                                 ,Cons(x,xs)  
                                                 ,pp          
                                                 ,ss)         
        
                   loop[Ite](False() =  [2] p + [2] s + [5]   
                                  ,p                          
                                  ,s                          
                                 ,pp                          
                        ,Cons(x,xs))                          
                                     >= [1]                   
                                     =  loop(pp,xs,pp,xs)     
        
                    loop[Ite](True() =  [8]                   
                       ,Cons(x',xs')                          
                         ,Cons(x,xs)                          
                                 ,pp                          
                                ,ss)                          
                                     >= [1]                   
                                     =  loop(xs',xs,pp,ss)    
        
                         match1(p,s) =  [1]                   
                                     >= [1]                   
                                     =  loop(p,s,p,s)         
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        loop(Cons(x,xs),Nil(),pp,ss) -> False()
        loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
        match1(p,s) -> loop(p,s,p,s)
      Weak DP Rules:
        
      Weak TRS Rules:
        !EQ(0(),0()) -> True()
        !EQ(0(),S(y)) -> False()
        !EQ(S(x),0()) -> False()
        !EQ(S(x),S(y)) -> !EQ(x,y)
        loop(Nil(),s,pp,ss) -> True()
        loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
        loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
      Signature:
        {!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {!EQ,loop,loop[Ite],match1}/{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(loop[Ite]) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                p(!EQ) = [2]                           
                  p(0) = [0]                           
               p(Cons) = [2]                           
              p(False) = [1]                           
                p(Nil) = [0]                           
                  p(S) = [1] x1 + [0]                  
               p(True) = [2]                           
               p(loop) = [2]                           
          p(loop[Ite]) = [1] x1 + [1] x2 + [5] x3 + [1]
             p(match1) = [5]                           
        
        Following rules are strictly oriented:
        loop(Cons(x,xs),Nil(),pp,ss) = [2]          
                                     > [1]          
                                     = False()      
        
                         match1(p,s) = [5]          
                                     > [2]          
                                     = loop(p,s,p,s)
        
        
        Following rules are (at-least) weakly oriented:
                  !EQ(0(),0()) =  [2]                   
                               >= [2]                   
                               =  True()                
        
                 !EQ(0(),S(y)) =  [2]                   
                               >= [1]                   
                               =  False()               
        
                 !EQ(S(x),0()) =  [2]                   
                               >= [1]                   
                               =  False()               
        
                !EQ(S(x),S(y)) =  [2]                   
                               >= [2]                   
                               =  !EQ(x,y)              
        
             loop(Cons(x',xs') =  [2]                   
                   ,Cons(x,xs)                          
                           ,pp                          
                          ,ss)                          
                               >= [15]                  
                               =  loop[Ite](!EQ(x',x)   
                                           ,Cons(x',xs')
                                           ,Cons(x,xs)  
                                           ,pp          
                                           ,ss)         
        
           loop(Nil(),s,pp,ss) =  [2]                   
                               >= [2]                   
                               =  True()                
        
             loop[Ite](False() =  [1] p + [5] s + [2]   
                            ,p                          
                            ,s                          
                           ,pp                          
                  ,Cons(x,xs))                          
                               >= [2]                   
                               =  loop(pp,xs,pp,xs)     
        
              loop[Ite](True() =  [15]                  
                 ,Cons(x',xs')                          
                   ,Cons(x,xs)                          
                           ,pp                          
                          ,ss)                          
                               >= [2]                   
                               =  loop(xs',xs,pp,ss)    
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^2))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
      Weak DP Rules:
        
      Weak TRS Rules:
        !EQ(0(),0()) -> True()
        !EQ(0(),S(y)) -> False()
        !EQ(S(x),0()) -> False()
        !EQ(S(x),S(y)) -> !EQ(x,y)
        loop(Cons(x,xs),Nil(),pp,ss) -> False()
        loop(Nil(),s,pp,ss) -> True()
        loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
        loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
        match1(p,s) -> loop(p,s,p,s)
      Signature:
        {!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {!EQ,loop,loop[Ite],match1}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a polynomial interpretation of kind constructor-based(mixed(2)):
      The following argument positions are considered usable:
        uargs(loop[Ite]) = {1}
      
      Following symbols are considered usable:
        {!EQ,loop,loop[Ite],match1}
      TcT has computed the following interpretation:
              p(!EQ) = 0                                                       
                p(0) = 0                                                       
             p(Cons) = 1 + x2                                                  
            p(False) = 0                                                       
              p(Nil) = 1                                                       
                p(S) = 0                                                       
             p(True) = 0                                                       
             p(loop) = 3 + x1 + 3*x2 + 2*x3 + 2*x3*x4 + 2*x4^2                 
        p(loop[Ite]) = 2 + 2*x1 + 2*x1*x4 + x2 + 3*x3 + 2*x4 + 2*x4*x5 + 2*x5^2
           p(match1) = 3 + 3*x1 + 3*x1*x2 + 2*x1^2 + 3*x2 + 2*x2^2             
      
      Following rules are strictly oriented:
      loop(Cons(x',xs') = 7 + 2*pp + 2*pp*ss + 2*ss^2 + 3*xs + xs'
            ,Cons(x,xs)                                           
                    ,pp                                           
                   ,ss)                                           
                        > 6 + 2*pp + 2*pp*ss + 2*ss^2 + 3*xs + xs'
                        = loop[Ite](!EQ(x',x)                     
                                   ,Cons(x',xs')                  
                                   ,Cons(x,xs)                    
                                   ,pp                            
                                   ,ss)                           
      
      
      Following rules are (at-least) weakly oriented:
                      !EQ(0(),0()) =  0                                           
                                   >= 0                                           
                                   =  True()                                      
      
                     !EQ(0(),S(y)) =  0                                           
                                   >= 0                                           
                                   =  False()                                     
      
                     !EQ(S(x),0()) =  0                                           
                                   >= 0                                           
                                   =  False()                                     
      
                    !EQ(S(x),S(y)) =  0                                           
                                   >= 0                                           
                                   =  !EQ(x,y)                                    
      
      loop(Cons(x,xs),Nil(),pp,ss) =  7 + 2*pp + 2*pp*ss + 2*ss^2 + xs            
                                   >= 0                                           
                                   =  False()                                     
      
               loop(Nil(),s,pp,ss) =  4 + 2*pp + 2*pp*ss + 3*s + 2*ss^2           
                                   >= 0                                           
                                   =  True()                                      
      
                 loop[Ite](False() =  4 + p + 4*pp + 2*pp*xs + 3*s + 4*xs + 2*xs^2
                                ,p                                                
                                ,s                                                
                               ,pp                                                
                      ,Cons(x,xs))                                                
                                   >= 3 + 3*pp + 2*pp*xs + 3*xs + 2*xs^2          
                                   =  loop(pp,xs,pp,xs)                           
      
                  loop[Ite](True() =  6 + 2*pp + 2*pp*ss + 2*ss^2 + 3*xs + xs'    
                     ,Cons(x',xs')                                                
                       ,Cons(x,xs)                                                
                               ,pp                                                
                              ,ss)                                                
                                   >= 3 + 2*pp + 2*pp*ss + 2*ss^2 + 3*xs + xs'    
                                   =  loop(xs',xs,pp,ss)                          
      
                       match1(p,s) =  3 + 3*p + 3*p*s + 2*p^2 + 3*s + 2*s^2       
                                   >= 3 + 3*p + 2*p*s + 3*s + 2*s^2               
                                   =  loop(p,s,p,s)                               
      
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        !EQ(0(),0()) -> True()
        !EQ(0(),S(y)) -> False()
        !EQ(S(x),0()) -> False()
        !EQ(S(x),S(y)) -> !EQ(x,y)
        loop(Cons(x,xs),Nil(),pp,ss) -> False()
        loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)
        loop(Nil(),s,pp,ss) -> True()
        loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs)
        loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss)
        match1(p,s) -> loop(p,s,p,s)
      Signature:
        {!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0}
      Obligation:
        Innermost
        basic terms: {!EQ,loop,loop[Ite],match1}/{0,Cons,False,Nil,S,True}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).