*** 1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
        sel(0(),cons(X,Y)) -> X
        sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {activate/1,from/1,sel/2} / {0/0,cons/2,n__from/1,s/1}
      Obligation:
        Innermost
        basic terms: {activate,from,sel}/{0,cons,n__from,s}
    Applied Processor:
      DependencyPairs {dpKind_ = WIDP}
    Proof:
      We add the following weak innermost dependency pairs:
      
      Strict DPs
        activate#(X) -> c_1()
        activate#(n__from(X)) -> c_2(from#(X))
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        activate#(X) -> c_1()
        activate#(n__from(X)) -> c_2(from#(X))
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Strict TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
        sel(0(),cons(X,Y)) -> X
        sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
        activate#(X) -> c_1()
        activate#(n__from(X)) -> c_2(from#(X))
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
*** 1.1.1 Progress [(?,O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        activate#(X) -> c_1()
        activate#(n__from(X)) -> c_2(from#(X))
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Strict TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnTrs}
    Proof:
      The weightgap principle applies using the following constant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(sel#) = {2},
          uargs(c_2) = {1},
          uargs(c_6) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
                  p(0) = [0]                  
           p(activate) = [1] x1 + [7]         
               p(cons) = [1] x2 + [0]         
               p(from) = [1] x1 + [7]         
            p(n__from) = [1] x1 + [1]         
                  p(s) = [1] x1 + [3]         
                p(sel) = [0]                  
          p(activate#) = [3] x1 + [0]         
              p(from#) = [3] x1 + [0]         
               p(sel#) = [8] x1 + [1] x2 + [0]
                p(c_1) = [0]                  
                p(c_2) = [1] x1 + [0]         
                p(c_3) = [0]                  
                p(c_4) = [0]                  
                p(c_5) = [0]                  
                p(c_6) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        activate#(n__from(X)) = [3] X + [3]             
                              > [3] X + [0]             
                              = c_2(from#(X))           
        
         sel#(s(X),cons(Y,Z)) = [8] X + [1] Z + [24]    
                              > [8] X + [1] Z + [7]     
                              = c_6(sel#(X,activate(Z)))
        
                  activate(X) = [1] X + [7]             
                              > [1] X + [0]             
                              = X                       
        
         activate(n__from(X)) = [1] X + [8]             
                              > [1] X + [7]             
                              = from(X)                 
        
                      from(X) = [1] X + [7]             
                              > [1] X + [4]             
                              = cons(X,n__from(s(X)))   
        
                      from(X) = [1] X + [7]             
                              > [1] X + [1]             
                              = n__from(X)              
        
        
        Following rules are (at-least) weakly oriented:
               activate#(X) =  [3] X + [0]
                            >= [0]        
                            =  c_1()      
        
                   from#(X) =  [3] X + [0]
                            >= [0]        
                            =  c_3()      
        
                   from#(X) =  [3] X + [0]
                            >= [0]        
                            =  c_4()      
        
        sel#(0(),cons(X,Y)) =  [1] Y + [0]
                            >= [0]        
                            =  c_5()      
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(?,O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        activate#(X) -> c_1()
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        activate#(n__from(X)) -> c_2(from#(X))
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Weak TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {1}
      by application of
        Pre({1}) = {}.
      Here rules are labelled as follows:
        1: activate#(X) -> c_1()       
        2: from#(X) -> c_3()           
        3: from#(X) -> c_4()           
        4: sel#(0(),cons(X,Y)) -> c_5()
        5: activate#(n__from(X)) ->    
             c_2(from#(X))             
        6: sel#(s(X),cons(Y,Z)) ->     
             c_6(sel#(X,activate(Z)))  
*** 1.1.1.1.1 Progress [(?,O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        activate#(X) -> c_1()
        activate#(n__from(X)) -> c_2(from#(X))
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Weak TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:from#(X) -> c_3()
           
        
        2:S:from#(X) -> c_4()
           
        
        3:S:sel#(0(),cons(X,Y)) -> c_5()
           
        
        4:W:activate#(X) -> c_1()
           
        
        5:W:activate#(n__from(X)) -> c_2(from#(X))
           -->_1 from#(X) -> c_4():2
           -->_1 from#(X) -> c_3():1
        
        6:W:sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
           -->_1 sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z))):6
           -->_1 sel#(0(),cons(X,Y)) -> c_5():3
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        4: activate#(X) -> c_1()
*** 1.1.1.1.1.1 Progress [(?,O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        activate#(n__from(X)) -> c_2(from#(X))
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Weak TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      RemoveHeads
    Proof:
      Consider the dependency graph
      
      1:S:from#(X) -> c_3()
         
      
      2:S:from#(X) -> c_4()
         
      
      3:S:sel#(0(),cons(X,Y)) -> c_5()
         
      
      5:W:activate#(n__from(X)) -> c_2(from#(X))
         -->_1 from#(X) -> c_4():2
         -->_1 from#(X) -> c_3():1
      
      6:W:sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
         -->_1 sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z))):6
         -->_1 sel#(0(),cons(X,Y)) -> c_5():3
      
      
      Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
      
      [(5,activate#(n__from(X)) -> c_2(from#(X)))]
*** 1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        from#(X) -> c_3()
        from#(X) -> c_4()
        sel#(0(),cons(X,Y)) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Weak TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      RemoveHeads
    Proof:
      Consider the dependency graph
      
      1:S:from#(X) -> c_3()
         
      
      2:S:from#(X) -> c_4()
         
      
      3:S:sel#(0(),cons(X,Y)) -> c_5()
         
      
      6:W:sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
         -->_1 sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z))):6
         -->_1 sel#(0(),cons(X,Y)) -> c_5():3
      
      
      Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
      
      [(1,from#(X) -> c_3()),(2,from#(X) -> c_4())]
*** 1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        sel#(0(),cons(X,Y)) -> c_5()
      Strict TRS Rules:
        
      Weak DP Rules:
        sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
      Weak TRS Rules:
        activate(X) -> X
        activate(n__from(X)) -> from(X)
        from(X) -> cons(X,n__from(s(X)))
        from(X) -> n__from(X)
      Signature:
        {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
      Obligation:
        Innermost
        basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
    Applied Processor:
      PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
    Proof:
      We first use the processor NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
        3: sel#(0(),cons(X,Y)) -> c_5()
        
      The strictly oriented rules are moved into the weak component.
  *** 1.1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          sel#(0(),cons(X,Y)) -> c_5()
        Strict TRS Rules:
          
        Weak DP Rules:
          sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
        Weak TRS Rules:
          activate(X) -> X
          activate(n__from(X)) -> from(X)
          from(X) -> cons(X,n__from(s(X)))
          from(X) -> n__from(X)
        Signature:
          {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
        Obligation:
          Innermost
          basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
      Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
      Proof:
        We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
        The following argument positions are considered usable:
          uargs(c_6) = {1}
        
        Following symbols are considered usable:
          {activate#,from#,sel#}
        TcT has computed the following interpretation:
                  p(0) = [0]         
           p(activate) = [1]         
               p(cons) = [0]         
               p(from) = [1] x1 + [1]
            p(n__from) = [2]         
                  p(s) = [0]         
                p(sel) = [1] x1 + [1]
          p(activate#) = [1]         
              p(from#) = [0]         
               p(sel#) = [1]         
                p(c_1) = [8]         
                p(c_2) = [2]         
                p(c_3) = [1]         
                p(c_4) = [1]         
                p(c_5) = [0]         
                p(c_6) = [1] x1 + [0]
        
        Following rules are strictly oriented:
        sel#(0(),cons(X,Y)) = [1]  
                            > [0]  
                            = c_5()
        
        
        Following rules are (at-least) weakly oriented:
        sel#(s(X),cons(Y,Z)) =  [1]                     
                             >= [1]                     
                             =  c_6(sel#(X,activate(Z)))
        
  *** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          
        Strict TRS Rules:
          
        Weak DP Rules:
          sel#(0(),cons(X,Y)) -> c_5()
          sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
        Weak TRS Rules:
          activate(X) -> X
          activate(n__from(X)) -> from(X)
          from(X) -> cons(X,n__from(s(X)))
          from(X) -> n__from(X)
        Signature:
          {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
        Obligation:
          Innermost
          basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
      Applied Processor:
        Assumption
      Proof:
        ()
  
  *** 1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          
        Strict TRS Rules:
          
        Weak DP Rules:
          sel#(0(),cons(X,Y)) -> c_5()
          sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
        Weak TRS Rules:
          activate(X) -> X
          activate(n__from(X)) -> from(X)
          from(X) -> cons(X,n__from(s(X)))
          from(X) -> n__from(X)
        Signature:
          {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
        Obligation:
          Innermost
          basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
      Applied Processor:
        RemoveWeakSuffixes
      Proof:
        Consider the dependency graph
          1:W:sel#(0(),cons(X,Y)) -> c_5()
             
          
          2:W:sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z)))
             -->_1 sel#(s(X),cons(Y,Z)) -> c_6(sel#(X,activate(Z))):2
             -->_1 sel#(0(),cons(X,Y)) -> c_5():1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          2: sel#(s(X),cons(Y,Z)) ->     
               c_6(sel#(X,activate(Z)))  
          1: sel#(0(),cons(X,Y)) -> c_5()
  *** 1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))]  ***
      Considered Problem:
        Strict DP Rules:
          
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          activate(X) -> X
          activate(n__from(X)) -> from(X)
          from(X) -> cons(X,n__from(s(X)))
          from(X) -> n__from(X)
        Signature:
          {activate/1,from/1,sel/2,activate#/1,from#/1,sel#/2} / {0/0,cons/2,n__from/1,s/1,c_1/0,c_2/1,c_3/0,c_4/0,c_5/0,c_6/1}
        Obligation:
          Innermost
          basic terms: {activate#,from#,sel#}/{0,cons,n__from,s}
      Applied Processor:
        EmptyProcessor
      Proof:
        The problem is already closed. The intended complexity is O(1).