YES(O(1),O(n^1))
0.00/0.32	YES(O(1),O(n^1))
0.00/0.32	
0.00/0.32	We are left with following problem, upon which TcT provides the
0.00/0.32	certificate YES(O(1),O(n^1)).
0.00/0.32	
0.00/0.32	Strict Trs:
0.00/0.32	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.32	  , from(X) -> n__from(X)
0.00/0.32	  , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
0.00/0.32	  , sel(0(), cons(X, Y)) -> X
0.00/0.32	  , activate(X) -> X
0.00/0.32	  , activate(n__from(X)) -> from(X) }
0.00/0.32	Obligation:
0.00/0.32	  innermost runtime complexity
0.00/0.32	Answer:
0.00/0.32	  YES(O(1),O(n^1))
0.00/0.32	
0.00/0.32	We add the following weak dependency pairs:
0.00/0.32	
0.00/0.32	Strict DPs:
0.00/0.32	  { from^#(X) -> c_1()
0.00/0.32	  , from^#(X) -> c_2()
0.00/0.32	  , sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.32	  , sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.32	  , activate^#(X) -> c_5()
0.00/0.32	  , activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.32	
0.00/0.32	and mark the set of starting terms.
0.00/0.32	
0.00/0.32	We are left with following problem, upon which TcT provides the
0.00/0.32	certificate YES(O(1),O(n^1)).
0.00/0.32	
0.00/0.32	Strict DPs:
0.00/0.32	  { from^#(X) -> c_1()
0.00/0.32	  , from^#(X) -> c_2()
0.00/0.32	  , sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.32	  , sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.32	  , activate^#(X) -> c_5()
0.00/0.32	  , activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.32	Strict Trs:
0.00/0.32	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.32	  , from(X) -> n__from(X)
0.00/0.32	  , sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
0.00/0.32	  , sel(0(), cons(X, Y)) -> X
0.00/0.32	  , activate(X) -> X
0.00/0.32	  , activate(n__from(X)) -> from(X) }
0.00/0.32	Obligation:
0.00/0.32	  innermost runtime complexity
0.00/0.32	Answer:
0.00/0.32	  YES(O(1),O(n^1))
0.00/0.32	
0.00/0.32	We replace rewrite rules by usable rules:
0.00/0.32	
0.00/0.32	  Strict Usable Rules:
0.00/0.32	    { from(X) -> cons(X, n__from(s(X)))
0.00/0.32	    , from(X) -> n__from(X)
0.00/0.32	    , activate(X) -> X
0.00/0.32	    , activate(n__from(X)) -> from(X) }
0.00/0.32	
0.00/0.32	We are left with following problem, upon which TcT provides the
0.00/0.32	certificate YES(O(1),O(n^1)).
0.00/0.32	
0.00/0.32	Strict DPs:
0.00/0.32	  { from^#(X) -> c_1()
0.00/0.32	  , from^#(X) -> c_2()
0.00/0.32	  , sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.32	  , sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.32	  , activate^#(X) -> c_5()
0.00/0.32	  , activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.32	Strict Trs:
0.00/0.32	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.32	  , from(X) -> n__from(X)
0.00/0.32	  , activate(X) -> X
0.00/0.32	  , activate(n__from(X)) -> from(X) }
0.00/0.32	Obligation:
0.00/0.32	  innermost runtime complexity
0.00/0.32	Answer:
0.00/0.32	  YES(O(1),O(n^1))
0.00/0.32	
0.00/0.32	The weightgap principle applies (using the following constant
0.00/0.32	growth matrix-interpretation)
0.00/0.32	
0.00/0.32	The following argument positions are usable:
0.00/0.32	  Uargs(sel^#) = {2}, Uargs(c_3) = {1}, Uargs(c_6) = {1}
0.00/0.32	
0.00/0.32	TcT has computed the following constructor-restricted matrix
0.00/0.32	interpretation.
0.00/0.32	
0.00/0.32	        [from](x1) = [1]           
0.00/0.32	                     [0]           
0.00/0.32	                                   
0.00/0.32	    [cons](x1, x2) = [1 0] x2 + [0]
0.00/0.32	                     [0 0]      [0]
0.00/0.32	                                   
0.00/0.32	     [n__from](x1) = [0]           
0.00/0.32	                     [0]           
0.00/0.32	                                   
0.00/0.32	           [s](x1) = [1 2] x1 + [0]
0.00/0.32	                     [0 0]      [0]
0.00/0.32	                                   
0.00/0.32	               [0] = [0]           
0.00/0.32	                     [0]           
0.00/0.32	                                   
0.00/0.32	    [activate](x1) = [1 0] x1 + [2]
0.00/0.32	                     [0 2]      [0]
0.00/0.32	                                   
0.00/0.32	      [from^#](x1) = [0 0] x1 + [1]
0.00/0.32	                     [2 2]      [1]
0.00/0.32	                                   
0.00/0.32	             [c_1] = [1]           
0.00/0.32	                     [1]           
0.00/0.32	                                   
0.00/0.32	             [c_2] = [0]           
0.00/0.32	                     [1]           
0.00/0.32	                                   
0.00/0.32	   [sel^#](x1, x2) = [1 0] x2 + [0]
0.00/0.32	                     [0 0]      [0]
0.00/0.32	                                   
0.00/0.32	         [c_3](x1) = [1 0] x1 + [2]
0.00/0.32	                     [0 1]      [2]
0.00/0.32	                                   
0.00/0.32	             [c_4] = [1]           
0.00/0.32	                     [0]           
0.00/0.32	                                   
0.00/0.32	  [activate^#](x1) = [1 1] x1 + [2]
0.00/0.32	                     [1 1]      [2]
0.00/0.32	                                   
0.00/0.32	             [c_5] = [1]           
0.00/0.32	                     [1]           
0.00/0.32	                                   
0.00/0.32	         [c_6](x1) = [1 0] x1 + [2]
0.00/0.32	                     [0 1]      [2]
0.00/0.32	
0.00/0.32	The order satisfies the following ordering constraints:
0.00/0.32	
0.00/0.32	                  [from(X)] =  [1]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            >  [0]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            =  [cons(X, n__from(s(X)))]    
0.00/0.32	                                                           
0.00/0.32	                  [from(X)] =  [1]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            >  [0]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            =  [n__from(X)]                
0.00/0.32	                                                           
0.00/0.32	              [activate(X)] =  [1 0] X + [2]               
0.00/0.32	                               [0 2]     [0]               
0.00/0.32	                            >  [1 0] X + [0]               
0.00/0.32	                               [0 1]     [0]               
0.00/0.32	                            =  [X]                         
0.00/0.32	                                                           
0.00/0.32	     [activate(n__from(X))] =  [2]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            >  [1]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            =  [from(X)]                   
0.00/0.32	                                                           
0.00/0.32	                [from^#(X)] =  [0 0] X + [1]               
0.00/0.32	                               [2 2]     [1]               
0.00/0.32	                            >= [1]                         
0.00/0.32	                               [1]                         
0.00/0.32	                            =  [c_1()]                     
0.00/0.32	                                                           
0.00/0.32	                [from^#(X)] =  [0 0] X + [1]               
0.00/0.32	                               [2 2]     [1]               
0.00/0.32	                            >  [0]                         
0.00/0.32	                               [1]                         
0.00/0.32	                            =  [c_2()]                     
0.00/0.32	                                                           
0.00/0.32	  [sel^#(s(X), cons(Y, Z))] =  [1 0] Z + [0]               
0.00/0.32	                               [0 0]     [0]               
0.00/0.32	                            ?  [1 0] Z + [4]               
0.00/0.32	                               [0 0]     [2]               
0.00/0.32	                            =  [c_3(sel^#(X, activate(Z)))]
0.00/0.32	                                                           
0.00/0.32	   [sel^#(0(), cons(X, Y))] =  [1 0] Y + [0]               
0.00/0.32	                               [0 0]     [0]               
0.00/0.32	                            ?  [1]                         
0.00/0.32	                               [0]                         
0.00/0.32	                            =  [c_4()]                     
0.00/0.32	                                                           
0.00/0.32	            [activate^#(X)] =  [1 1] X + [2]               
0.00/0.32	                               [1 1]     [2]               
0.00/0.32	                            >  [1]                         
0.00/0.32	                               [1]                         
0.00/0.32	                            =  [c_5()]                     
0.00/0.32	                                                           
0.00/0.33	   [activate^#(n__from(X))] =  [2]                         
0.00/0.33	                               [2]                         
0.00/0.33	                            ?  [0 0] X + [3]               
0.00/0.33	                               [2 2]     [3]               
0.00/0.33	                            =  [c_6(from^#(X))]            
0.00/0.33	                                                           
0.00/0.33	
0.00/0.33	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(n^1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { from^#(X) -> c_1()
0.00/0.33	  , sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.33	  , sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.33	  , activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.33	Weak DPs:
0.00/0.33	  { from^#(X) -> c_2()
0.00/0.33	  , activate^#(X) -> c_5() }
0.00/0.33	Weak Trs:
0.00/0.33	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.33	  , from(X) -> n__from(X)
0.00/0.33	  , activate(X) -> X
0.00/0.33	  , activate(n__from(X)) -> from(X) }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(n^1))
0.00/0.33	
0.00/0.33	We estimate the number of application of {1,3} by applications of
0.00/0.33	Pre({1,3}) = {2,4}. Here rules are labeled as follows:
0.00/0.33	
0.00/0.33	  DPs:
0.00/0.33	    { 1: from^#(X) -> c_1()
0.00/0.33	    , 2: sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.33	    , 3: sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.33	    , 4: activate^#(n__from(X)) -> c_6(from^#(X))
0.00/0.33	    , 5: from^#(X) -> c_2()
0.00/0.33	    , 6: activate^#(X) -> c_5() }
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(n^1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.33	  , activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.33	Weak DPs:
0.00/0.33	  { from^#(X) -> c_1()
0.00/0.33	  , from^#(X) -> c_2()
0.00/0.33	  , sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.33	  , activate^#(X) -> c_5() }
0.00/0.33	Weak Trs:
0.00/0.33	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.33	  , from(X) -> n__from(X)
0.00/0.33	  , activate(X) -> X
0.00/0.33	  , activate(n__from(X)) -> from(X) }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(n^1))
0.00/0.33	
0.00/0.33	We estimate the number of application of {2} by applications of
0.00/0.33	Pre({2}) = {}. Here rules are labeled as follows:
0.00/0.33	
0.00/0.33	  DPs:
0.00/0.33	    { 1: sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z)))
0.00/0.33	    , 2: activate^#(n__from(X)) -> c_6(from^#(X))
0.00/0.33	    , 3: from^#(X) -> c_1()
0.00/0.33	    , 4: from^#(X) -> c_2()
0.00/0.33	    , 5: sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.33	    , 6: activate^#(X) -> c_5() }
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(n^1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z))) }
0.00/0.33	Weak DPs:
0.00/0.33	  { from^#(X) -> c_1()
0.00/0.33	  , from^#(X) -> c_2()
0.00/0.33	  , sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.33	  , activate^#(X) -> c_5()
0.00/0.33	  , activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.33	Weak Trs:
0.00/0.33	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.33	  , from(X) -> n__from(X)
0.00/0.33	  , activate(X) -> X
0.00/0.33	  , activate(n__from(X)) -> from(X) }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(n^1))
0.00/0.33	
0.00/0.33	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.33	closed under successors. The DPs are removed.
0.00/0.33	
0.00/0.33	{ from^#(X) -> c_1()
0.00/0.33	, from^#(X) -> c_2()
0.00/0.33	, sel^#(0(), cons(X, Y)) -> c_4()
0.00/0.33	, activate^#(X) -> c_5()
0.00/0.33	, activate^#(n__from(X)) -> c_6(from^#(X)) }
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(n^1)).
0.00/0.33	
0.00/0.33	Strict DPs:
0.00/0.33	  { sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z))) }
0.00/0.33	Weak Trs:
0.00/0.33	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.33	  , from(X) -> n__from(X)
0.00/0.33	  , activate(X) -> X
0.00/0.33	  , activate(n__from(X)) -> from(X) }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(n^1))
0.00/0.33	
0.00/0.33	We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
0.00/0.33	to orient following rules strictly.
0.00/0.33	
0.00/0.33	DPs:
0.00/0.33	  { 1: sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z))) }
0.00/0.33	Trs: { from(X) -> n__from(X) }
0.00/0.33	
0.00/0.33	Sub-proof:
0.00/0.33	----------
0.00/0.33	  The input was oriented with the instance of 'Small Polynomial Path
0.00/0.33	  Order (PS,1-bounded)' as induced by the safe mapping
0.00/0.33	  
0.00/0.33	   safe(from) = {1}, safe(cons) = {1, 2}, safe(n__from) = {1},
0.00/0.33	   safe(s) = {1}, safe(activate) = {}, safe(sel^#) = {2},
0.00/0.33	   safe(c_3) = {}
0.00/0.33	  
0.00/0.33	  and precedence
0.00/0.33	  
0.00/0.33	   from ~ activate, from ~ sel^#, activate ~ sel^# .
0.00/0.33	  
0.00/0.33	  Following symbols are considered recursive:
0.00/0.33	  
0.00/0.33	   {from, activate, sel^#}
0.00/0.33	  
0.00/0.33	  The recursion depth is 1.
0.00/0.33	  
0.00/0.33	  Further, following argument filtering is employed:
0.00/0.33	  
0.00/0.33	   pi(from) = [], pi(cons) = [], pi(n__from) = [], pi(s) = [1],
0.00/0.33	   pi(activate) = [], pi(sel^#) = [1], pi(c_3) = [1]
0.00/0.33	  
0.00/0.33	  Usable defined function symbols are a subset of:
0.00/0.33	  
0.00/0.33	   {sel^#}
0.00/0.33	  
0.00/0.33	  For your convenience, here are the satisfied ordering constraints:
0.00/0.33	  
0.00/0.33	    pi(sel^#(s(X), cons(Y, Z))) = sel^#(s(; X);)                
0.00/0.33	                                > c_3(sel^#(X;);)               
0.00/0.33	                                = pi(c_3(sel^#(X, activate(Z))))
0.00/0.33	                                                                
0.00/0.33	
0.00/0.33	The strictly oriented rules are moved into the weak component.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Weak DPs: { sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z))) }
0.00/0.33	Weak Trs:
0.00/0.33	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.33	  , from(X) -> n__from(X)
0.00/0.33	  , activate(X) -> X
0.00/0.33	  , activate(n__from(X)) -> from(X) }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.33	closed under successors. The DPs are removed.
0.00/0.33	
0.00/0.33	{ sel^#(s(X), cons(Y, Z)) -> c_3(sel^#(X, activate(Z))) }
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Weak Trs:
0.00/0.33	  { from(X) -> cons(X, n__from(s(X)))
0.00/0.33	  , from(X) -> n__from(X)
0.00/0.33	  , activate(X) -> X
0.00/0.33	  , activate(n__from(X)) -> from(X) }
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	No rule is usable, rules are removed from the input problem.
0.00/0.33	
0.00/0.33	We are left with following problem, upon which TcT provides the
0.00/0.33	certificate YES(O(1),O(1)).
0.00/0.33	
0.00/0.33	Rules: Empty
0.00/0.33	Obligation:
0.00/0.33	  innermost runtime complexity
0.00/0.33	Answer:
0.00/0.33	  YES(O(1),O(1))
0.00/0.33	
0.00/0.33	Empty rules are trivially bounded
0.00/0.33	
0.00/0.33	Hurray, we answered YES(O(1),O(n^1))
0.00/0.33	EOF