*** 1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    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(a__adx) = {1},
          uargs(a__hd) = {1},
          uargs(a__incr) = {1},
          uargs(a__tl) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(0) = [0]         
            p(a__adx) = [1] x1 + [1]
             p(a__hd) = [1] x1 + [0]
           p(a__incr) = [1] x1 + [0]
           p(a__nats) = [0]         
             p(a__tl) = [1] x1 + [0]
          p(a__zeros) = [0]         
               p(adx) = [0]         
              p(cons) = [0]         
                p(hd) = [1] x1 + [0]
              p(incr) = [1] x1 + [0]
              p(mark) = [0]         
              p(nats) = [0]         
                 p(s) = [0]         
                p(tl) = [1] x1 + [0]
             p(zeros) = [0]         
        
        Following rules are strictly oriented:
                a__adx(X) = [1] X + [1]            
                          > [0]                    
                          = adx(X)                 
        
        a__adx(cons(X,Y)) = [1]                    
                          > [0]                    
                          = a__incr(cons(X,adx(Y)))
        
        
        Following rules are (at-least) weakly oriented:
                  a__hd(X) =  [1] X + [0]       
                           >= [1] X + [0]       
                           =  hd(X)             
        
          a__hd(cons(X,Y)) =  [0]               
                           >= [0]               
                           =  mark(X)           
        
                a__incr(X) =  [1] X + [0]       
                           >= [1] X + [0]       
                           =  incr(X)           
        
        a__incr(cons(X,Y)) =  [0]               
                           >= [0]               
                           =  cons(s(X),incr(Y))
        
                 a__nats() =  [0]               
                           >= [1]               
                           =  a__adx(a__zeros())
        
                 a__nats() =  [0]               
                           >= [0]               
                           =  nats()            
        
                  a__tl(X) =  [1] X + [0]       
                           >= [1] X + [0]       
                           =  tl(X)             
        
          a__tl(cons(X,Y)) =  [0]               
                           >= [0]               
                           =  mark(Y)           
        
                a__zeros() =  [0]               
                           >= [0]               
                           =  cons(0(),zeros()) 
        
                a__zeros() =  [0]               
                           >= [0]               
                           =  zeros()           
        
                 mark(0()) =  [0]               
                           >= [0]               
                           =  0()               
        
              mark(adx(X)) =  [0]               
                           >= [1]               
                           =  a__adx(mark(X))   
        
         mark(cons(X1,X2)) =  [0]               
                           >= [0]               
                           =  cons(X1,X2)       
        
               mark(hd(X)) =  [0]               
                           >= [0]               
                           =  a__hd(mark(X))    
        
             mark(incr(X)) =  [0]               
                           >= [0]               
                           =  a__incr(mark(X))  
        
              mark(nats()) =  [0]               
                           >= [0]               
                           =  a__nats()         
        
                mark(s(X)) =  [0]               
                           >= [0]               
                           =  s(X)              
        
               mark(tl(X)) =  [0]               
                           >= [0]               
                           =  a__tl(mark(X))    
        
             mark(zeros()) =  [0]               
                           >= [0]               
                           =  a__zeros()        
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    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(a__adx) = {1},
          uargs(a__hd) = {1},
          uargs(a__incr) = {1},
          uargs(a__tl) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(0) = [0]                  
            p(a__adx) = [1] x1 + [15]        
             p(a__hd) = [1] x1 + [0]         
           p(a__incr) = [1] x1 + [0]         
           p(a__nats) = [0]                  
             p(a__tl) = [1] x1 + [0]         
          p(a__zeros) = [0]                  
               p(adx) = [1] x1 + [15]        
              p(cons) = [1] x1 + [1] x2 + [9]
                p(hd) = [1] x1 + [0]         
              p(incr) = [1] x1 + [0]         
              p(mark) = [1] x1 + [0]         
              p(nats) = [0]                  
                 p(s) = [1] x1 + [0]         
                p(tl) = [1] x1 + [0]         
             p(zeros) = [9]                  
        
        Following rules are strictly oriented:
        a__hd(cons(X,Y)) = [1] X + [1] Y + [9]
                         > [1] X + [0]        
                         = mark(X)            
        
        a__tl(cons(X,Y)) = [1] X + [1] Y + [9]
                         > [1] Y + [0]        
                         = mark(Y)            
        
           mark(zeros()) = [9]                
                         > [0]                
                         = a__zeros()         
        
        
        Following rules are (at-least) weakly oriented:
                 a__adx(X) =  [1] X + [15]           
                           >= [1] X + [15]           
                           =  adx(X)                 
        
         a__adx(cons(X,Y)) =  [1] X + [1] Y + [24]   
                           >= [1] X + [1] Y + [24]   
                           =  a__incr(cons(X,adx(Y)))
        
                  a__hd(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  hd(X)                  
        
                a__incr(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  incr(X)                
        
        a__incr(cons(X,Y)) =  [1] X + [1] Y + [9]    
                           >= [1] X + [1] Y + [9]    
                           =  cons(s(X),incr(Y))     
        
                 a__nats() =  [0]                    
                           >= [15]                   
                           =  a__adx(a__zeros())     
        
                 a__nats() =  [0]                    
                           >= [0]                    
                           =  nats()                 
        
                  a__tl(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  tl(X)                  
        
                a__zeros() =  [0]                    
                           >= [18]                   
                           =  cons(0(),zeros())      
        
                a__zeros() =  [0]                    
                           >= [9]                    
                           =  zeros()                
        
                 mark(0()) =  [0]                    
                           >= [0]                    
                           =  0()                    
        
              mark(adx(X)) =  [1] X + [15]           
                           >= [1] X + [15]           
                           =  a__adx(mark(X))        
        
         mark(cons(X1,X2)) =  [1] X1 + [1] X2 + [9]  
                           >= [1] X1 + [1] X2 + [9]  
                           =  cons(X1,X2)            
        
               mark(hd(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  a__hd(mark(X))         
        
             mark(incr(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  a__incr(mark(X))       
        
              mark(nats()) =  [0]                    
                           >= [0]                    
                           =  a__nats()              
        
                mark(s(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  s(X)                   
        
               mark(tl(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  a__tl(mark(X))         
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__hd(X) -> hd(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(cons(X,Y)) -> mark(X)
        a__tl(cons(X,Y)) -> mark(Y)
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    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(a__adx) = {1},
          uargs(a__hd) = {1},
          uargs(a__incr) = {1},
          uargs(a__tl) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(0) = [0]         
            p(a__adx) = [1] x1 + [0]
             p(a__hd) = [1] x1 + [6]
           p(a__incr) = [1] x1 + [0]
           p(a__nats) = [0]         
             p(a__tl) = [1] x1 + [0]
          p(a__zeros) = [0]         
               p(adx) = [1] x1 + [0]
              p(cons) = [0]         
                p(hd) = [0]         
              p(incr) = [0]         
              p(mark) = [0]         
              p(nats) = [0]         
                 p(s) = [0]         
                p(tl) = [1] x1 + [0]
             p(zeros) = [0]         
        
        Following rules are strictly oriented:
        a__hd(X) = [1] X + [6]
                 > [0]        
                 = hd(X)      
        
        
        Following rules are (at-least) weakly oriented:
                 a__adx(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  adx(X)                 
        
         a__adx(cons(X,Y)) =  [0]                    
                           >= [0]                    
                           =  a__incr(cons(X,adx(Y)))
        
          a__hd(cons(X,Y)) =  [6]                    
                           >= [0]                    
                           =  mark(X)                
        
                a__incr(X) =  [1] X + [0]            
                           >= [0]                    
                           =  incr(X)                
        
        a__incr(cons(X,Y)) =  [0]                    
                           >= [0]                    
                           =  cons(s(X),incr(Y))     
        
                 a__nats() =  [0]                    
                           >= [0]                    
                           =  a__adx(a__zeros())     
        
                 a__nats() =  [0]                    
                           >= [0]                    
                           =  nats()                 
        
                  a__tl(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  tl(X)                  
        
          a__tl(cons(X,Y)) =  [0]                    
                           >= [0]                    
                           =  mark(Y)                
        
                a__zeros() =  [0]                    
                           >= [0]                    
                           =  cons(0(),zeros())      
        
                a__zeros() =  [0]                    
                           >= [0]                    
                           =  zeros()                
        
                 mark(0()) =  [0]                    
                           >= [0]                    
                           =  0()                    
        
              mark(adx(X)) =  [0]                    
                           >= [0]                    
                           =  a__adx(mark(X))        
        
         mark(cons(X1,X2)) =  [0]                    
                           >= [0]                    
                           =  cons(X1,X2)            
        
               mark(hd(X)) =  [0]                    
                           >= [6]                    
                           =  a__hd(mark(X))         
        
             mark(incr(X)) =  [0]                    
                           >= [0]                    
                           =  a__incr(mark(X))       
        
              mark(nats()) =  [0]                    
                           >= [0]                    
                           =  a__nats()              
        
                mark(s(X)) =  [0]                    
                           >= [0]                    
                           =  s(X)                   
        
               mark(tl(X)) =  [0]                    
                           >= [0]                    
                           =  a__tl(mark(X))         
        
             mark(zeros()) =  [0]                    
                           >= [0]                    
                           =  a__zeros()             
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__tl(cons(X,Y)) -> mark(Y)
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    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(a__adx) = {1},
          uargs(a__hd) = {1},
          uargs(a__incr) = {1},
          uargs(a__tl) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(0) = [0]         
            p(a__adx) = [1] x1 + [1]
             p(a__hd) = [1] x1 + [0]
           p(a__incr) = [1] x1 + [1]
           p(a__nats) = [0]         
             p(a__tl) = [1] x1 + [0]
          p(a__zeros) = [1]         
               p(adx) = [0]         
              p(cons) = [1]         
                p(hd) = [0]         
              p(incr) = [1] x1 + [0]
              p(mark) = [1]         
              p(nats) = [0]         
                 p(s) = [0]         
                p(tl) = [1] x1 + [0]
             p(zeros) = [1]         
        
        Following rules are strictly oriented:
                a__incr(X) = [1] X + [1]       
                           > [1] X + [0]       
                           = incr(X)           
        
        a__incr(cons(X,Y)) = [2]               
                           > [1]               
                           = cons(s(X),incr(Y))
        
                 mark(0()) = [1]               
                           > [0]               
                           = 0()               
        
              mark(nats()) = [1]               
                           > [0]               
                           = a__nats()         
        
                mark(s(X)) = [1]               
                           > [0]               
                           = s(X)              
        
        
        Following rules are (at-least) weakly oriented:
                a__adx(X) =  [1] X + [1]            
                          >= [0]                    
                          =  adx(X)                 
        
        a__adx(cons(X,Y)) =  [2]                    
                          >= [2]                    
                          =  a__incr(cons(X,adx(Y)))
        
                 a__hd(X) =  [1] X + [0]            
                          >= [0]                    
                          =  hd(X)                  
        
         a__hd(cons(X,Y)) =  [1]                    
                          >= [1]                    
                          =  mark(X)                
        
                a__nats() =  [0]                    
                          >= [2]                    
                          =  a__adx(a__zeros())     
        
                a__nats() =  [0]                    
                          >= [0]                    
                          =  nats()                 
        
                 a__tl(X) =  [1] X + [0]            
                          >= [1] X + [0]            
                          =  tl(X)                  
        
         a__tl(cons(X,Y)) =  [1]                    
                          >= [1]                    
                          =  mark(Y)                
        
               a__zeros() =  [1]                    
                          >= [1]                    
                          =  cons(0(),zeros())      
        
               a__zeros() =  [1]                    
                          >= [1]                    
                          =  zeros()                
        
             mark(adx(X)) =  [1]                    
                          >= [2]                    
                          =  a__adx(mark(X))        
        
        mark(cons(X1,X2)) =  [1]                    
                          >= [1]                    
                          =  cons(X1,X2)            
        
              mark(hd(X)) =  [1]                    
                          >= [1]                    
                          =  a__hd(mark(X))         
        
            mark(incr(X)) =  [1]                    
                          >= [2]                    
                          =  a__incr(mark(X))       
        
              mark(tl(X)) =  [1]                    
                          >= [1]                    
                          =  a__tl(mark(X))         
        
            mark(zeros()) =  [1]                    
                          >= [1]                    
                          =  a__zeros()             
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
        mark(tl(X)) -> a__tl(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__tl(cons(X,Y)) -> mark(Y)
        mark(0()) -> 0()
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    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(a__adx) = {1},
          uargs(a__hd) = {1},
          uargs(a__incr) = {1},
          uargs(a__tl) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(0) = [5]                  
            p(a__adx) = [1] x1 + [0]         
             p(a__hd) = [1] x1 + [0]         
           p(a__incr) = [1] x1 + [0]         
           p(a__nats) = [0]                  
             p(a__tl) = [1] x1 + [0]         
          p(a__zeros) = [0]                  
               p(adx) = [1] x1 + [0]         
              p(cons) = [1] x1 + [1] x2 + [0]
                p(hd) = [1] x1 + [0]         
              p(incr) = [1] x1 + [0]         
              p(mark) = [1] x1 + [0]         
              p(nats) = [0]                  
                 p(s) = [1] x1 + [0]         
                p(tl) = [1] x1 + [1]         
             p(zeros) = [0]                  
        
        Following rules are strictly oriented:
        mark(tl(X)) = [1] X + [1]   
                    > [1] X + [0]   
                    = a__tl(mark(X))
        
        
        Following rules are (at-least) weakly oriented:
                 a__adx(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  adx(X)                 
        
         a__adx(cons(X,Y)) =  [1] X + [1] Y + [0]    
                           >= [1] X + [1] Y + [0]    
                           =  a__incr(cons(X,adx(Y)))
        
                  a__hd(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  hd(X)                  
        
          a__hd(cons(X,Y)) =  [1] X + [1] Y + [0]    
                           >= [1] X + [0]            
                           =  mark(X)                
        
                a__incr(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  incr(X)                
        
        a__incr(cons(X,Y)) =  [1] X + [1] Y + [0]    
                           >= [1] X + [1] Y + [0]    
                           =  cons(s(X),incr(Y))     
        
                 a__nats() =  [0]                    
                           >= [0]                    
                           =  a__adx(a__zeros())     
        
                 a__nats() =  [0]                    
                           >= [0]                    
                           =  nats()                 
        
                  a__tl(X) =  [1] X + [0]            
                           >= [1] X + [1]            
                           =  tl(X)                  
        
          a__tl(cons(X,Y)) =  [1] X + [1] Y + [0]    
                           >= [1] Y + [0]            
                           =  mark(Y)                
        
                a__zeros() =  [0]                    
                           >= [5]                    
                           =  cons(0(),zeros())      
        
                a__zeros() =  [0]                    
                           >= [0]                    
                           =  zeros()                
        
                 mark(0()) =  [5]                    
                           >= [5]                    
                           =  0()                    
        
              mark(adx(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  a__adx(mark(X))        
        
         mark(cons(X1,X2)) =  [1] X1 + [1] X2 + [0]  
                           >= [1] X1 + [1] X2 + [0]  
                           =  cons(X1,X2)            
        
               mark(hd(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  a__hd(mark(X))         
        
             mark(incr(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  a__incr(mark(X))       
        
              mark(nats()) =  [0]                    
                           >= [0]                    
                           =  a__nats()              
        
                mark(s(X)) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  s(X)                   
        
             mark(zeros()) =  [0]                    
                           >= [0]                    
                           =  a__zeros()             
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__tl(cons(X,Y)) -> mark(Y)
        mark(0()) -> 0()
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    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(a__adx) = {1},
          uargs(a__hd) = {1},
          uargs(a__incr) = {1},
          uargs(a__tl) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                 p(0) = [0]                  
            p(a__adx) = [1] x1 + [0]         
             p(a__hd) = [1] x1 + [4]         
           p(a__incr) = [1] x1 + [0]         
           p(a__nats) = [5]                  
             p(a__tl) = [1] x1 + [4]         
          p(a__zeros) = [3]                  
               p(adx) = [1] x1 + [0]         
              p(cons) = [1] x1 + [1] x2 + [1]
                p(hd) = [1] x1 + [4]         
              p(incr) = [1] x1 + [0]         
              p(mark) = [1] x1 + [5]         
              p(nats) = [0]                  
                 p(s) = [1] x1 + [0]         
                p(tl) = [1] x1 + [4]         
             p(zeros) = [0]                  
        
        Following rules are strictly oriented:
                a__nats() = [5]                  
                          > [3]                  
                          = a__adx(a__zeros())   
        
                a__nats() = [5]                  
                          > [0]                  
                          = nats()               
        
               a__zeros() = [3]                  
                          > [1]                  
                          = cons(0(),zeros())    
        
               a__zeros() = [3]                  
                          > [0]                  
                          = zeros()              
        
        mark(cons(X1,X2)) = [1] X1 + [1] X2 + [6]
                          > [1] X1 + [1] X2 + [1]
                          = cons(X1,X2)          
        
        
        Following rules are (at-least) weakly oriented:
                 a__adx(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  adx(X)                 
        
         a__adx(cons(X,Y)) =  [1] X + [1] Y + [1]    
                           >= [1] X + [1] Y + [1]    
                           =  a__incr(cons(X,adx(Y)))
        
                  a__hd(X) =  [1] X + [4]            
                           >= [1] X + [4]            
                           =  hd(X)                  
        
          a__hd(cons(X,Y)) =  [1] X + [1] Y + [5]    
                           >= [1] X + [5]            
                           =  mark(X)                
        
                a__incr(X) =  [1] X + [0]            
                           >= [1] X + [0]            
                           =  incr(X)                
        
        a__incr(cons(X,Y)) =  [1] X + [1] Y + [1]    
                           >= [1] X + [1] Y + [1]    
                           =  cons(s(X),incr(Y))     
        
                  a__tl(X) =  [1] X + [4]            
                           >= [1] X + [4]            
                           =  tl(X)                  
        
          a__tl(cons(X,Y)) =  [1] X + [1] Y + [5]    
                           >= [1] Y + [5]            
                           =  mark(Y)                
        
                 mark(0()) =  [5]                    
                           >= [0]                    
                           =  0()                    
        
              mark(adx(X)) =  [1] X + [5]            
                           >= [1] X + [5]            
                           =  a__adx(mark(X))        
        
               mark(hd(X)) =  [1] X + [9]            
                           >= [1] X + [9]            
                           =  a__hd(mark(X))         
        
             mark(incr(X)) =  [1] X + [5]            
                           >= [1] X + [5]            
                           =  a__incr(mark(X))       
        
              mark(nats()) =  [5]                    
                           >= [5]                    
                           =  a__nats()              
        
                mark(s(X)) =  [1] X + [5]            
                           >= [1] X + [0]            
                           =  s(X)                   
        
               mark(tl(X)) =  [1] X + [9]            
                           >= [1] X + [9]            
                           =  a__tl(mark(X))         
        
             mark(zeros()) =  [5]                    
                           >= [3]                    
                           =  a__zeros()             
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        a__tl(X) -> tl(X)
        mark(adx(X)) -> a__adx(mark(X))
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    Applied Processor:
      NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(a__adx) = {1},
        uargs(a__hd) = {1},
        uargs(a__incr) = {1},
        uargs(a__tl) = {1}
      
      Following symbols are considered usable:
        {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}
      TcT has computed the following interpretation:
               p(0) = [0]                      
                      [0]                      
          p(a__adx) = [1 0] x1 + [0]           
                      [0 1]      [0]           
           p(a__hd) = [1 0] x1 + [0]           
                      [0 1]      [0]           
         p(a__incr) = [1 0] x1 + [0]           
                      [0 1]      [0]           
         p(a__nats) = [0]                      
                      [0]                      
           p(a__tl) = [1 0] x1 + [1]           
                      [0 1]      [2]           
        p(a__zeros) = [0]                      
                      [0]                      
             p(adx) = [1 0] x1 + [0]           
                      [0 1]      [0]           
            p(cons) = [0 4] x1 + [0 4] x2 + [0]
                      [0 1]      [0 1]      [0]
              p(hd) = [0 0] x1 + [0]           
                      [0 1]      [0]           
            p(incr) = [1 0] x1 + [0]           
                      [0 1]      [0]           
            p(mark) = [0 4] x1 + [0]           
                      [0 1]      [0]           
            p(nats) = [0]                      
                      [0]                      
               p(s) = [0]                      
                      [0]                      
              p(tl) = [0 0] x1 + [0]           
                      [0 1]      [2]           
           p(zeros) = [0]                      
                      [0]                      
      
      Following rules are strictly oriented:
      a__tl(X) = [1 0] X + [1]
                 [0 1]     [2]
               > [0 0] X + [0]
                 [0 1]     [2]
               = tl(X)        
      
      
      Following rules are (at-least) weakly oriented:
               a__adx(X) =  [1 0] X + [0]            
                            [0 1]     [0]            
                         >= [1 0] X + [0]            
                            [0 1]     [0]            
                         =  adx(X)                   
      
       a__adx(cons(X,Y)) =  [0 4] X + [0 4] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         >= [0 4] X + [0 4] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         =  a__incr(cons(X,adx(Y)))  
      
                a__hd(X) =  [1 0] X + [0]            
                            [0 1]     [0]            
                         >= [0 0] X + [0]            
                            [0 1]     [0]            
                         =  hd(X)                    
      
        a__hd(cons(X,Y)) =  [0 4] X + [0 4] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         >= [0 4] X + [0]            
                            [0 1]     [0]            
                         =  mark(X)                  
      
              a__incr(X) =  [1 0] X + [0]            
                            [0 1]     [0]            
                         >= [1 0] X + [0]            
                            [0 1]     [0]            
                         =  incr(X)                  
      
      a__incr(cons(X,Y)) =  [0 4] X + [0 4] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         >= [0 4] Y + [0]            
                            [0 1]     [0]            
                         =  cons(s(X),incr(Y))       
      
               a__nats() =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  a__adx(a__zeros())       
      
               a__nats() =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  nats()                   
      
        a__tl(cons(X,Y)) =  [0 4] X + [0 4] Y + [1]  
                            [0 1]     [0 1]     [2]  
                         >= [0 4] Y + [0]            
                            [0 1]     [0]            
                         =  mark(Y)                  
      
              a__zeros() =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  cons(0(),zeros())        
      
              a__zeros() =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  zeros()                  
      
               mark(0()) =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  0()                      
      
            mark(adx(X)) =  [0 4] X + [0]            
                            [0 1]     [0]            
                         >= [0 4] X + [0]            
                            [0 1]     [0]            
                         =  a__adx(mark(X))          
      
       mark(cons(X1,X2)) =  [0 4] X1 + [0 4] X2 + [0]
                            [0 1]      [0 1]      [0]
                         >= [0 4] X1 + [0 4] X2 + [0]
                            [0 1]      [0 1]      [0]
                         =  cons(X1,X2)              
      
             mark(hd(X)) =  [0 4] X + [0]            
                            [0 1]     [0]            
                         >= [0 4] X + [0]            
                            [0 1]     [0]            
                         =  a__hd(mark(X))           
      
           mark(incr(X)) =  [0 4] X + [0]            
                            [0 1]     [0]            
                         >= [0 4] X + [0]            
                            [0 1]     [0]            
                         =  a__incr(mark(X))         
      
            mark(nats()) =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  a__nats()                
      
              mark(s(X)) =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  s(X)                     
      
             mark(tl(X)) =  [0 4] X + [8]            
                            [0 1]     [2]            
                         >= [0 4] X + [1]            
                            [0 1]     [2]            
                         =  a__tl(mark(X))           
      
           mark(zeros()) =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  a__zeros()               
      
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        mark(adx(X)) -> a__adx(mark(X))
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    Applied Processor:
      NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(a__adx) = {1},
        uargs(a__hd) = {1},
        uargs(a__incr) = {1},
        uargs(a__tl) = {1}
      
      Following symbols are considered usable:
        {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}
      TcT has computed the following interpretation:
               p(0) = [0]                      
                      [0]                      
          p(a__adx) = [1 0] x1 + [0]           
                      [0 1]      [0]           
           p(a__hd) = [1 0] x1 + [2]           
                      [0 1]      [2]           
         p(a__incr) = [1 0] x1 + [0]           
                      [0 1]      [0]           
         p(a__nats) = [4]                      
                      [2]                      
           p(a__tl) = [1 0] x1 + [4]           
                      [0 1]      [2]           
        p(a__zeros) = [0]                      
                      [0]                      
             p(adx) = [0 0] x1 + [0]           
                      [0 1]      [0]           
            p(cons) = [0 2] x1 + [0 2] x2 + [0]
                      [0 1]      [0 1]      [0]
              p(hd) = [0 0] x1 + [2]           
                      [0 1]      [2]           
            p(incr) = [1 0] x1 + [0]           
                      [0 1]      [0]           
            p(mark) = [0 2] x1 + [0]           
                      [0 1]      [0]           
            p(nats) = [0]                      
                      [2]                      
               p(s) = [0 0] x1 + [0]           
                      [0 1]      [0]           
              p(tl) = [0 0] x1 + [0]           
                      [0 1]      [2]           
           p(zeros) = [0]                      
                      [0]                      
      
      Following rules are strictly oriented:
      mark(hd(X)) = [0 2] X + [4] 
                    [0 1]     [2] 
                  > [0 2] X + [2] 
                    [0 1]     [2] 
                  = a__hd(mark(X))
      
      
      Following rules are (at-least) weakly oriented:
               a__adx(X) =  [1 0] X + [0]            
                            [0 1]     [0]            
                         >= [0 0] X + [0]            
                            [0 1]     [0]            
                         =  adx(X)                   
      
       a__adx(cons(X,Y)) =  [0 2] X + [0 2] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         >= [0 2] X + [0 2] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         =  a__incr(cons(X,adx(Y)))  
      
                a__hd(X) =  [1 0] X + [2]            
                            [0 1]     [2]            
                         >= [0 0] X + [2]            
                            [0 1]     [2]            
                         =  hd(X)                    
      
        a__hd(cons(X,Y)) =  [0 2] X + [0 2] Y + [2]  
                            [0 1]     [0 1]     [2]  
                         >= [0 2] X + [0]            
                            [0 1]     [0]            
                         =  mark(X)                  
      
              a__incr(X) =  [1 0] X + [0]            
                            [0 1]     [0]            
                         >= [1 0] X + [0]            
                            [0 1]     [0]            
                         =  incr(X)                  
      
      a__incr(cons(X,Y)) =  [0 2] X + [0 2] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         >= [0 2] X + [0 2] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         =  cons(s(X),incr(Y))       
      
               a__nats() =  [4]                      
                            [2]                      
                         >= [0]                      
                            [0]                      
                         =  a__adx(a__zeros())       
      
               a__nats() =  [4]                      
                            [2]                      
                         >= [0]                      
                            [2]                      
                         =  nats()                   
      
                a__tl(X) =  [1 0] X + [4]            
                            [0 1]     [2]            
                         >= [0 0] X + [0]            
                            [0 1]     [2]            
                         =  tl(X)                    
      
        a__tl(cons(X,Y)) =  [0 2] X + [0 2] Y + [4]  
                            [0 1]     [0 1]     [2]  
                         >= [0 2] Y + [0]            
                            [0 1]     [0]            
                         =  mark(Y)                  
      
              a__zeros() =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  cons(0(),zeros())        
      
              a__zeros() =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  zeros()                  
      
               mark(0()) =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  0()                      
      
            mark(adx(X)) =  [0 2] X + [0]            
                            [0 1]     [0]            
                         >= [0 2] X + [0]            
                            [0 1]     [0]            
                         =  a__adx(mark(X))          
      
       mark(cons(X1,X2)) =  [0 2] X1 + [0 2] X2 + [0]
                            [0 1]      [0 1]      [0]
                         >= [0 2] X1 + [0 2] X2 + [0]
                            [0 1]      [0 1]      [0]
                         =  cons(X1,X2)              
      
           mark(incr(X)) =  [0 2] X + [0]            
                            [0 1]     [0]            
                         >= [0 2] X + [0]            
                            [0 1]     [0]            
                         =  a__incr(mark(X))         
      
            mark(nats()) =  [4]                      
                            [2]                      
                         >= [4]                      
                            [2]                      
                         =  a__nats()                
      
              mark(s(X)) =  [0 2] X + [0]            
                            [0 1]     [0]            
                         >= [0 0] X + [0]            
                            [0 1]     [0]            
                         =  s(X)                     
      
             mark(tl(X)) =  [0 2] X + [4]            
                            [0 1]     [2]            
                         >= [0 2] X + [4]            
                            [0 1]     [2]            
                         =  a__tl(mark(X))           
      
           mark(zeros()) =  [0]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  a__zeros()               
      
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        mark(adx(X)) -> a__adx(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    Applied Processor:
      NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(a__adx) = {1},
        uargs(a__hd) = {1},
        uargs(a__incr) = {1},
        uargs(a__tl) = {1}
      
      Following symbols are considered usable:
        {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}
      TcT has computed the following interpretation:
               p(0) = [1]                      
                      [0]                      
          p(a__adx) = [1 0] x1 + [1]           
                      [0 1]      [1]           
           p(a__hd) = [1 3] x1 + [7]           
                      [0 1]      [2]           
         p(a__incr) = [1 0] x1 + [0]           
                      [0 1]      [0]           
         p(a__nats) = [3]                      
                      [1]                      
           p(a__tl) = [1 3] x1 + [6]           
                      [0 1]      [2]           
        p(a__zeros) = [1]                      
                      [0]                      
             p(adx) = [1 0] x1 + [0]           
                      [0 1]      [1]           
            p(cons) = [1 1] x1 + [1 1] x2 + [0]
                      [0 1]      [0 1]      [0]
              p(hd) = [1 3] x1 + [2]           
                      [0 1]      [2]           
            p(incr) = [1 0] x1 + [0]           
                      [0 1]      [0]           
            p(mark) = [1 4] x1 + [1]           
                      [0 1]      [0]           
            p(nats) = [3]                      
                      [1]                      
               p(s) = [1 1] x1 + [0]           
                      [0 0]      [0]           
              p(tl) = [1 3] x1 + [0]           
                      [0 1]      [2]           
           p(zeros) = [0]                      
                      [0]                      
      
      Following rules are strictly oriented:
      mark(adx(X)) = [1 4] X + [5]  
                     [0 1]     [1]  
                   > [1 4] X + [2]  
                     [0 1]     [1]  
                   = a__adx(mark(X))
      
      
      Following rules are (at-least) weakly oriented:
               a__adx(X) =  [1 0] X + [1]            
                            [0 1]     [1]            
                         >= [1 0] X + [0]            
                            [0 1]     [1]            
                         =  adx(X)                   
      
       a__adx(cons(X,Y)) =  [1 1] X + [1 1] Y + [1]  
                            [0 1]     [0 1]     [1]  
                         >= [1 1] X + [1 1] Y + [1]  
                            [0 1]     [0 1]     [1]  
                         =  a__incr(cons(X,adx(Y)))  
      
                a__hd(X) =  [1 3] X + [7]            
                            [0 1]     [2]            
                         >= [1 3] X + [2]            
                            [0 1]     [2]            
                         =  hd(X)                    
      
        a__hd(cons(X,Y)) =  [1 4] X + [1 4] Y + [7]  
                            [0 1]     [0 1]     [2]  
                         >= [1 4] X + [1]            
                            [0 1]     [0]            
                         =  mark(X)                  
      
              a__incr(X) =  [1 0] X + [0]            
                            [0 1]     [0]            
                         >= [1 0] X + [0]            
                            [0 1]     [0]            
                         =  incr(X)                  
      
      a__incr(cons(X,Y)) =  [1 1] X + [1 1] Y + [0]  
                            [0 1]     [0 1]     [0]  
                         >= [1 1] X + [1 1] Y + [0]  
                            [0 0]     [0 1]     [0]  
                         =  cons(s(X),incr(Y))       
      
               a__nats() =  [3]                      
                            [1]                      
                         >= [2]                      
                            [1]                      
                         =  a__adx(a__zeros())       
      
               a__nats() =  [3]                      
                            [1]                      
                         >= [3]                      
                            [1]                      
                         =  nats()                   
      
                a__tl(X) =  [1 3] X + [6]            
                            [0 1]     [2]            
                         >= [1 3] X + [0]            
                            [0 1]     [2]            
                         =  tl(X)                    
      
        a__tl(cons(X,Y)) =  [1 4] X + [1 4] Y + [6]  
                            [0 1]     [0 1]     [2]  
                         >= [1 4] Y + [1]            
                            [0 1]     [0]            
                         =  mark(Y)                  
      
              a__zeros() =  [1]                      
                            [0]                      
                         >= [1]                      
                            [0]                      
                         =  cons(0(),zeros())        
      
              a__zeros() =  [1]                      
                            [0]                      
                         >= [0]                      
                            [0]                      
                         =  zeros()                  
      
               mark(0()) =  [2]                      
                            [0]                      
                         >= [1]                      
                            [0]                      
                         =  0()                      
      
       mark(cons(X1,X2)) =  [1 5] X1 + [1 5] X2 + [1]
                            [0 1]      [0 1]      [0]
                         >= [1 1] X1 + [1 1] X2 + [0]
                            [0 1]      [0 1]      [0]
                         =  cons(X1,X2)              
      
             mark(hd(X)) =  [1 7] X + [11]           
                            [0 1]     [2]            
                         >= [1 7] X + [8]            
                            [0 1]     [2]            
                         =  a__hd(mark(X))           
      
           mark(incr(X)) =  [1 4] X + [1]            
                            [0 1]     [0]            
                         >= [1 4] X + [1]            
                            [0 1]     [0]            
                         =  a__incr(mark(X))         
      
            mark(nats()) =  [8]                      
                            [1]                      
                         >= [3]                      
                            [1]                      
                         =  a__nats()                
      
              mark(s(X)) =  [1 1] X + [1]            
                            [0 0]     [0]            
                         >= [1 1] X + [0]            
                            [0 0]     [0]            
                         =  s(X)                     
      
             mark(tl(X)) =  [1 7] X + [9]            
                            [0 1]     [2]            
                         >= [1 7] X + [7]            
                            [0 1]     [2]            
                         =  a__tl(mark(X))           
      
           mark(zeros()) =  [1]                      
                            [0]                      
                         >= [1]                      
                            [0]                      
                         =  a__zeros()               
      
*** 1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        mark(incr(X)) -> a__incr(mark(X))
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(a__adx) = {1},
        uargs(a__hd) = {1},
        uargs(a__incr) = {1},
        uargs(a__tl) = {1}
      
      Following symbols are considered usable:
        {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}
      TcT has computed the following interpretation:
               p(0) = [0]                          
                      [0]                          
                      [0]                          
          p(a__adx) = [1 0 0]      [0]             
                      [0 1 0] x1 + [1]             
                      [0 0 1]      [2]             
           p(a__hd) = [1 0 0]      [0]             
                      [0 1 0] x1 + [0]             
                      [0 0 1]      [0]             
         p(a__incr) = [1 0 0]      [0]             
                      [0 1 0] x1 + [1]             
                      [0 0 1]      [0]             
         p(a__nats) = [1]                          
                      [2]                          
                      [3]                          
           p(a__tl) = [1 2 1]      [0]             
                      [0 1 1] x1 + [0]             
                      [0 0 1]      [1]             
        p(a__zeros) = [1]                          
                      [0]                          
                      [0]                          
             p(adx) = [1 0 0]      [0]             
                      [0 1 0] x1 + [0]             
                      [0 0 1]      [2]             
            p(cons) = [1 2 1]      [1 0 0]      [0]
                      [0 1 1] x1 + [0 1 0] x2 + [0]
                      [0 0 1]      [0 0 1]      [0]
              p(hd) = [1 0 0]      [0]             
                      [0 1 0] x1 + [0]             
                      [0 0 1]      [0]             
            p(incr) = [1 0 0]      [0]             
                      [0 1 0] x1 + [1]             
                      [0 0 1]      [0]             
            p(mark) = [1 2 0]      [0]             
                      [0 1 1] x1 + [0]             
                      [0 0 1]      [0]             
            p(nats) = [1]                          
                      [0]                          
                      [3]                          
               p(s) = [1 0 0]      [0]             
                      [0 1 0] x1 + [0]             
                      [0 0 1]      [0]             
              p(tl) = [1 2 1]      [0]             
                      [0 1 1] x1 + [0]             
                      [0 0 1]      [1]             
           p(zeros) = [1]                          
                      [0]                          
                      [0]                          
      
      Following rules are strictly oriented:
      mark(incr(X)) = [1 2 0]     [2] 
                      [0 1 1] X + [1] 
                      [0 0 1]     [0] 
                    > [1 2 0]     [0] 
                      [0 1 1] X + [1] 
                      [0 0 1]     [0] 
                    = a__incr(mark(X))
      
      
      Following rules are (at-least) weakly oriented:
               a__adx(X) =  [1 0 0]     [0]              
                            [0 1 0] X + [1]              
                            [0 0 1]     [2]              
                         >= [1 0 0]     [0]              
                            [0 1 0] X + [0]              
                            [0 0 1]     [2]              
                         =  adx(X)                       
      
       a__adx(cons(X,Y)) =  [1 2 1]     [1 0 0]     [0]  
                            [0 1 1] X + [0 1 0] Y + [1]  
                            [0 0 1]     [0 0 1]     [2]  
                         >= [1 2 1]     [1 0 0]     [0]  
                            [0 1 1] X + [0 1 0] Y + [1]  
                            [0 0 1]     [0 0 1]     [2]  
                         =  a__incr(cons(X,adx(Y)))      
      
                a__hd(X) =  [1 0 0]     [0]              
                            [0 1 0] X + [0]              
                            [0 0 1]     [0]              
                         >= [1 0 0]     [0]              
                            [0 1 0] X + [0]              
                            [0 0 1]     [0]              
                         =  hd(X)                        
      
        a__hd(cons(X,Y)) =  [1 2 1]     [1 0 0]     [0]  
                            [0 1 1] X + [0 1 0] Y + [0]  
                            [0 0 1]     [0 0 1]     [0]  
                         >= [1 2 0]     [0]              
                            [0 1 1] X + [0]              
                            [0 0 1]     [0]              
                         =  mark(X)                      
      
              a__incr(X) =  [1 0 0]     [0]              
                            [0 1 0] X + [1]              
                            [0 0 1]     [0]              
                         >= [1 0 0]     [0]              
                            [0 1 0] X + [1]              
                            [0 0 1]     [0]              
                         =  incr(X)                      
      
      a__incr(cons(X,Y)) =  [1 2 1]     [1 0 0]     [0]  
                            [0 1 1] X + [0 1 0] Y + [1]  
                            [0 0 1]     [0 0 1]     [0]  
                         >= [1 2 1]     [1 0 0]     [0]  
                            [0 1 1] X + [0 1 0] Y + [1]  
                            [0 0 1]     [0 0 1]     [0]  
                         =  cons(s(X),incr(Y))           
      
               a__nats() =  [1]                          
                            [2]                          
                            [3]                          
                         >= [1]                          
                            [1]                          
                            [2]                          
                         =  a__adx(a__zeros())           
      
               a__nats() =  [1]                          
                            [2]                          
                            [3]                          
                         >= [1]                          
                            [0]                          
                            [3]                          
                         =  nats()                       
      
                a__tl(X) =  [1 2 1]     [0]              
                            [0 1 1] X + [0]              
                            [0 0 1]     [1]              
                         >= [1 2 1]     [0]              
                            [0 1 1] X + [0]              
                            [0 0 1]     [1]              
                         =  tl(X)                        
      
        a__tl(cons(X,Y)) =  [1 4 4]     [1 2 1]     [0]  
                            [0 1 2] X + [0 1 1] Y + [0]  
                            [0 0 1]     [0 0 1]     [1]  
                         >= [1 2 0]     [0]              
                            [0 1 1] Y + [0]              
                            [0 0 1]     [0]              
                         =  mark(Y)                      
      
              a__zeros() =  [1]                          
                            [0]                          
                            [0]                          
                         >= [1]                          
                            [0]                          
                            [0]                          
                         =  cons(0(),zeros())            
      
              a__zeros() =  [1]                          
                            [0]                          
                            [0]                          
                         >= [1]                          
                            [0]                          
                            [0]                          
                         =  zeros()                      
      
               mark(0()) =  [0]                          
                            [0]                          
                            [0]                          
                         >= [0]                          
                            [0]                          
                            [0]                          
                         =  0()                          
      
            mark(adx(X)) =  [1 2 0]     [0]              
                            [0 1 1] X + [2]              
                            [0 0 1]     [2]              
                         >= [1 2 0]     [0]              
                            [0 1 1] X + [1]              
                            [0 0 1]     [2]              
                         =  a__adx(mark(X))              
      
       mark(cons(X1,X2)) =  [1 4 3]      [1 2 0]      [0]
                            [0 1 2] X1 + [0 1 1] X2 + [0]
                            [0 0 1]      [0 0 1]      [0]
                         >= [1 2 1]      [1 0 0]      [0]
                            [0 1 1] X1 + [0 1 0] X2 + [0]
                            [0 0 1]      [0 0 1]      [0]
                         =  cons(X1,X2)                  
      
             mark(hd(X)) =  [1 2 0]     [0]              
                            [0 1 1] X + [0]              
                            [0 0 1]     [0]              
                         >= [1 2 0]     [0]              
                            [0 1 1] X + [0]              
                            [0 0 1]     [0]              
                         =  a__hd(mark(X))               
      
            mark(nats()) =  [1]                          
                            [3]                          
                            [3]                          
                         >= [1]                          
                            [2]                          
                            [3]                          
                         =  a__nats()                    
      
              mark(s(X)) =  [1 2 0]     [0]              
                            [0 1 1] X + [0]              
                            [0 0 1]     [0]              
                         >= [1 0 0]     [0]              
                            [0 1 0] X + [0]              
                            [0 0 1]     [0]              
                         =  s(X)                         
      
             mark(tl(X)) =  [1 4 3]     [0]              
                            [0 1 2] X + [1]              
                            [0 0 1]     [1]              
                         >= [1 4 3]     [0]              
                            [0 1 2] X + [0]              
                            [0 0 1]     [1]              
                         =  a__tl(mark(X))               
      
           mark(zeros()) =  [1]                          
                            [0]                          
                            [0]                          
                         >= [1]                          
                            [0]                          
                            [0]                          
                         =  a__zeros()                   
      
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        a__adx(X) -> adx(X)
        a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
        a__hd(X) -> hd(X)
        a__hd(cons(X,Y)) -> mark(X)
        a__incr(X) -> incr(X)
        a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
        a__nats() -> a__adx(a__zeros())
        a__nats() -> nats()
        a__tl(X) -> tl(X)
        a__tl(cons(X,Y)) -> mark(Y)
        a__zeros() -> cons(0(),zeros())
        a__zeros() -> zeros()
        mark(0()) -> 0()
        mark(adx(X)) -> a__adx(mark(X))
        mark(cons(X1,X2)) -> cons(X1,X2)
        mark(hd(X)) -> a__hd(mark(X))
        mark(incr(X)) -> a__incr(mark(X))
        mark(nats()) -> a__nats()
        mark(s(X)) -> s(X)
        mark(tl(X)) -> a__tl(mark(X))
        mark(zeros()) -> a__zeros()
      Signature:
        {a__adx/1,a__hd/1,a__incr/1,a__nats/0,a__tl/1,a__zeros/0,mark/1} / {0/0,adx/1,cons/2,hd/1,incr/1,nats/0,s/1,tl/1,zeros/0}
      Obligation:
        Innermost
        basic terms: {a__adx,a__hd,a__incr,a__nats,a__tl,a__zeros,mark}/{0,adx,cons,hd,incr,nats,s,tl,zeros}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).