YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
  , first(0(), Z) -> nil()
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__first(X1, X2)) -> first(X1, X2)
  , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
  , sel(0(), cons(X, Z)) -> X }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add following weak dependency pairs:

Strict DPs:
  { from^#(X) -> c_1()
  , from^#(X) -> c_2()
  , first^#(X1, X2) -> c_3()
  , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z))
  , first^#(0(), Z) -> c_5()
  , activate^#(X) -> c_6()
  , activate^#(n__from(X)) -> c_7(from^#(X))
  , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2))
  , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z)))
  , sel^#(0(), cons(X, Z)) -> c_10() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { from^#(X) -> c_1()
  , from^#(X) -> c_2()
  , first^#(X1, X2) -> c_3()
  , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z))
  , first^#(0(), Z) -> c_5()
  , activate^#(X) -> c_6()
  , activate^#(n__from(X)) -> c_7(from^#(X))
  , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2))
  , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z)))
  , sel^#(0(), cons(X, Z)) -> c_10() }
Strict Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
  , first(0(), Z) -> nil()
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__first(X1, X2)) -> first(X1, X2)
  , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
  , sel(0(), cons(X, Z)) -> X }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We replace rewrite rules by usable rules:

  Strict Usable Rules:
    { from(X) -> cons(X, n__from(s(X)))
    , from(X) -> n__from(X)
    , first(X1, X2) -> n__first(X1, X2)
    , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
    , first(0(), Z) -> nil()
    , activate(X) -> X
    , activate(n__from(X)) -> from(X)
    , activate(n__first(X1, X2)) -> first(X1, X2) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { from^#(X) -> c_1()
  , from^#(X) -> c_2()
  , first^#(X1, X2) -> c_3()
  , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z))
  , first^#(0(), Z) -> c_5()
  , activate^#(X) -> c_6()
  , activate^#(n__from(X)) -> c_7(from^#(X))
  , activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2))
  , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z)))
  , sel^#(0(), cons(X, Z)) -> c_10() }
Strict Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
  , first(0(), Z) -> nil()
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__first(X1, X2)) -> first(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(cons) = {2}, Uargs(n__first) = {2}, Uargs(c_4) = {1},
  Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(sel^#) = {2},
  Uargs(c_9) = {1}

TcT has computed following constructor-restricted matrix
interpretation.

          [from](x1) = [2]                  
                                            
      [cons](x1, x2) = [1] x2 + [0]         
                                            
       [n__from](x1) = [1]                  
                                            
             [s](x1) = [1] x1 + [2]         
                                            
     [first](x1, x2) = [1] x1 + [1] x2 + [1]
                                            
                 [0] = [1]                  
                                            
               [nil] = [1]                  
                                            
  [n__first](x1, x2) = [1] x1 + [1] x2 + [0]
                                            
      [activate](x1) = [1] x1 + [2]         
                                            
        [from^#](x1) = [2]                  
                                            
               [c_1] = [1]                  
                                            
               [c_2] = [1]                  
                                            
   [first^#](x1, x2) = [1] x1 + [2] x2 + [2]
                                            
               [c_3] = [1]                  
                                            
           [c_4](x1) = [1] x1 + [1]         
                                            
    [activate^#](x1) = [2] x1 + [2]         
                                            
               [c_5] = [2]                  
                                            
               [c_6] = [1]                  
                                            
           [c_7](x1) = [1] x1 + [1]         
                                            
           [c_8](x1) = [1] x1 + [1]         
                                            
     [sel^#](x1, x2) = [1] x1 + [2] x2 + [2]
                                            
           [c_9](x1) = [1] x1 + [1]         
                                            
              [c_10] = [2]                  

This order satisfies following ordering constraints:

                     [from(X)] = [2]                                
                               > [1]                                
                               = [cons(X, n__from(s(X)))]           
                                                                    
                     [from(X)] = [2]                                
                               > [1]                                
                               = [n__from(X)]                       
                                                                    
               [first(X1, X2)] = [1] X1 + [1] X2 + [1]              
                               > [1] X1 + [1] X2 + [0]              
                               = [n__first(X1, X2)]                 
                                                                    
     [first(s(X), cons(Y, Z))] = [1] X + [1] Z + [3]                
                               > [1] X + [1] Z + [2]                
                               = [cons(Y, n__first(X, activate(Z)))]
                                                                    
               [first(0(), Z)] = [1] Z + [2]                        
                               > [1]                                
                               = [nil()]                            
                                                                    
                 [activate(X)] = [1] X + [2]                        
                               > [1] X + [0]                        
                               = [X]                                
                                                                    
        [activate(n__from(X))] = [3]                                
                               > [2]                                
                               = [from(X)]                          
                                                                    
  [activate(n__first(X1, X2))] = [1] X1 + [1] X2 + [2]              
                               > [1] X1 + [1] X2 + [1]              
                               = [first(X1, X2)]                    
                                                                    

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2))
  , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) }
Weak DPs:
  { from^#(X) -> c_1()
  , from^#(X) -> c_2()
  , first^#(X1, X2) -> c_3()
  , first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z))
  , first^#(0(), Z) -> c_5()
  , activate^#(X) -> c_6()
  , activate^#(n__from(X)) -> c_7(from^#(X))
  , sel^#(0(), cons(X, Z)) -> c_10() }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
  , first(0(), Z) -> nil()
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__first(X1, X2)) -> first(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ from^#(X) -> c_1()
, from^#(X) -> c_2()
, first^#(X1, X2) -> c_3()
, first^#(0(), Z) -> c_5()
, activate^#(X) -> c_6()
, activate^#(n__from(X)) -> c_7(from^#(X))
, sel^#(0(), cons(X, Z)) -> c_10() }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { activate^#(n__first(X1, X2)) -> c_8(first^#(X1, X2))
  , sel^#(s(X), cons(Y, Z)) -> c_9(sel^#(X, activate(Z))) }
Weak DPs: { first^#(s(X), cons(Y, Z)) -> c_4(activate^#(Z)) }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , first(X1, X2) -> n__first(X1, X2)
  , first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z)))
  , first(0(), Z) -> nil()
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__first(X1, X2)) -> first(X1, X2) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS)' as induced by the safe mapping

 safe(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1},
 safe(s) = {1}, safe(first) = {}, safe(0) = {}, safe(nil) = {},
 safe(n__first) = {1, 2}, safe(activate) = {}, safe(first^#) = {1},
 safe(c_4) = {}, safe(activate^#) = {}, safe(c_8) = {},
 safe(sel^#) = {2}, safe(c_9) = {}

and precedence

 from ~ first, from ~ activate, from ~ first^#, from ~ activate^#,
 from ~ sel^#, first ~ first^#, first ~ activate^#, first ~ sel^#,
 activate ~ first^#, activate ~ activate^#, activate ~ sel^#,
 first^# ~ activate^#, first^# ~ sel^#, activate^# ~ sel^# .

Following symbols are considered recursive:

 {from, first, activate, first^#, activate^#, sel^#}

The recursion depth is 1.

Further, following argument filtering is employed:

 pi(from) = [], pi(cons) = [2], pi(n__from) = [], pi(s) = [1],
 pi(first) = [], pi(0) = [], pi(nil) = [], pi(n__first) = [2],
 pi(activate) = [], pi(first^#) = [2], pi(c_4) = [1],
 pi(activate^#) = [1], pi(c_8) = [1], pi(sel^#) = [1], pi(c_9) = [1]

Usable defined function symbols are a subset of:

 {first^#, activate^#, sel^#}

For your convenience, here are the satisfied ordering constraints:

     pi(first^#(s(X), cons(Y, Z))) = first^#(cons(; Z);)           
                                   > c_4(activate^#(Z;);)          
                                   = pi(c_4(activate^#(Z)))        
                                                                   
  pi(activate^#(n__first(X1, X2))) = activate^#(n__first(; X2);)   
                                   > c_8(first^#(X2;);)            
                                   = pi(c_8(first^#(X1, X2)))      
                                                                   
       pi(sel^#(s(X), cons(Y, Z))) = sel^#(s(; X);)                
                                   > c_9(sel^#(X;);)               
                                   = pi(c_9(sel^#(X, activate(Z))))
                                                                   

Hurray, we answered YES(O(1),O(n^1))