YES(O(1),O(n^1))
67.11/31.68	YES(O(1),O(n^1))
67.11/31.68	
67.11/31.68	We are left with following problem, upon which TcT provides the
67.11/31.68	certificate YES(O(1),O(n^1)).
67.11/31.68	
67.11/31.68	Strict Trs:
67.11/31.68	  { 2nd(cons1(X, cons(Y, Z))) -> Y
67.11/31.68	  , 2nd(cons(X, X1)) -> 2nd(cons1(X, activate(X1)))
67.11/31.68	  , activate(X) -> X
67.11/31.68	  , activate(n__from(X)) -> from(activate(X))
67.11/31.68	  , activate(n__s(X)) -> s(activate(X))
67.11/31.68	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.68	  , from(X) -> n__from(X)
67.11/31.68	  , s(X) -> n__s(X) }
67.11/31.68	Obligation:
67.11/31.68	  innermost runtime complexity
67.11/31.68	Answer:
67.11/31.68	  YES(O(1),O(n^1))
67.11/31.68	
67.11/31.68	We add the following weak dependency pairs:
67.11/31.68	
67.11/31.68	Strict DPs:
67.11/31.68	  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.68	  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.68	  , activate^#(X) -> c_3()
67.11/31.68	  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.68	  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.68	  , from^#(X) -> c_6()
67.11/31.68	  , from^#(X) -> c_7()
67.11/31.68	  , s^#(X) -> c_8() }
67.11/31.68	
67.11/31.68	and mark the set of starting terms.
67.11/31.68	
67.11/31.68	We are left with following problem, upon which TcT provides the
67.11/31.68	certificate YES(O(1),O(n^1)).
67.11/31.68	
67.11/31.68	Strict DPs:
67.11/31.68	  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.68	  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	  , activate^#(X) -> c_3()
67.11/31.69	  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	  , from^#(X) -> c_6()
67.11/31.69	  , from^#(X) -> c_7()
67.11/31.69	  , s^#(X) -> c_8() }
67.11/31.69	Strict Trs:
67.11/31.69	  { 2nd(cons1(X, cons(Y, Z))) -> Y
67.11/31.69	  , 2nd(cons(X, X1)) -> 2nd(cons1(X, activate(X1)))
67.11/31.69	  , activate(X) -> X
67.11/31.69	  , activate(n__from(X)) -> from(activate(X))
67.11/31.69	  , activate(n__s(X)) -> s(activate(X))
67.11/31.69	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	  , from(X) -> n__from(X)
67.11/31.69	  , s(X) -> n__s(X) }
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(n^1))
67.11/31.69	
67.11/31.69	We replace rewrite rules by usable rules:
67.11/31.69	
67.11/31.69	  Strict Usable Rules:
67.11/31.69	    { activate(X) -> X
67.11/31.69	    , activate(n__from(X)) -> from(activate(X))
67.11/31.69	    , activate(n__s(X)) -> s(activate(X))
67.11/31.69	    , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	    , from(X) -> n__from(X)
67.11/31.69	    , s(X) -> n__s(X) }
67.11/31.69	
67.11/31.69	We are left with following problem, upon which TcT provides the
67.11/31.69	certificate YES(O(1),O(n^1)).
67.11/31.69	
67.11/31.69	Strict DPs:
67.11/31.69	  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	  , activate^#(X) -> c_3()
67.11/31.69	  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	  , from^#(X) -> c_6()
67.11/31.69	  , from^#(X) -> c_7()
67.11/31.69	  , s^#(X) -> c_8() }
67.11/31.69	Strict Trs:
67.11/31.69	  { activate(X) -> X
67.11/31.69	  , activate(n__from(X)) -> from(activate(X))
67.11/31.69	  , activate(n__s(X)) -> s(activate(X))
67.11/31.69	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	  , from(X) -> n__from(X)
67.11/31.69	  , s(X) -> n__s(X) }
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(n^1))
67.11/31.69	
67.11/31.69	The weightgap principle applies (using the following constant
67.11/31.69	growth matrix-interpretation)
67.11/31.69	
67.11/31.69	The following argument positions are usable:
67.11/31.69	  Uargs(cons1) = {2}, Uargs(from) = {1}, Uargs(s) = {1},
67.11/31.69	  Uargs(2nd^#) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1},
67.11/31.69	  Uargs(from^#) = {1}, Uargs(c_5) = {1}, Uargs(s^#) = {1}
67.11/31.69	
67.11/31.69	TcT has computed the following constructor-restricted matrix
67.11/31.69	interpretation.
67.11/31.69	
67.11/31.69	   [cons1](x1, x2) = [1 0] x2 + [0]
67.11/31.69	                     [0 0]      [0]
67.11/31.69	                                   
67.11/31.69	    [cons](x1, x2) = [1 0] x2 + [0]
67.11/31.69	                     [0 1]      [0]
67.11/31.69	                                   
67.11/31.69	    [activate](x1) = [1 2] x1 + [1]
67.11/31.69	                     [0 2]      [0]
67.11/31.69	                                   
67.11/31.69	        [from](x1) = [1 0] x1 + [1]
67.11/31.69	                     [0 1]      [2]
67.11/31.69	                                   
67.11/31.69	     [n__from](x1) = [1 0] x1 + [0]
67.11/31.69	                     [0 1]      [1]
67.11/31.69	                                   
67.11/31.69	        [n__s](x1) = [1 0] x1 + [0]
67.11/31.69	                     [0 1]      [1]
67.11/31.69	                                   
67.11/31.69	           [s](x1) = [1 0] x1 + [1]
67.11/31.69	                     [0 1]      [1]
67.11/31.69	                                   
67.11/31.69	       [2nd^#](x1) = [1 2] x1 + [0]
67.11/31.69	                     [0 0]      [0]
67.11/31.69	                                   
67.11/31.69	             [c_1] = [1]           
67.11/31.69	                     [1]           
67.11/31.69	                                   
67.11/31.69	         [c_2](x1) = [1 0] x1 + [1]
67.11/31.69	                     [0 1]      [2]
67.11/31.69	                                   
67.11/31.69	  [activate^#](x1) = [1 2] x1 + [2]
67.11/31.69	                     [1 2]      [2]
67.11/31.69	                                   
67.11/31.69	             [c_3] = [1]           
67.11/31.69	                     [1]           
67.11/31.69	                                   
67.11/31.69	         [c_4](x1) = [1 0] x1 + [2]
67.11/31.69	                     [0 1]      [2]
67.11/31.69	                                   
67.11/31.69	      [from^#](x1) = [1 0] x1 + [1]
67.11/31.69	                     [0 0]      [2]
67.11/31.69	                                   
67.11/31.69	         [c_5](x1) = [1 0] x1 + [2]
67.11/31.69	                     [0 1]      [2]
67.11/31.69	                                   
67.11/31.69	         [s^#](x1) = [1 0] x1 + [1]
67.11/31.69	                     [0 0]      [2]
67.11/31.69	                                   
67.11/31.69	             [c_6] = [1]           
67.11/31.69	                     [1]           
67.11/31.69	                                   
67.11/31.69	             [c_7] = [1]           
67.11/31.69	                     [1]           
67.11/31.69	                                   
67.11/31.69	             [c_8] = [1]           
67.11/31.69	                     [1]           
67.11/31.69	
67.11/31.69	The order satisfies the following ordering constraints:
67.11/31.69	
67.11/31.69	                  [activate(X)] =  [1 2] X + [1]                       
67.11/31.69	                                   [0 2]     [0]                       
67.11/31.69	                                >  [1 0] X + [0]                       
67.11/31.69	                                   [0 1]     [0]                       
67.11/31.69	                                =  [X]                                 
67.11/31.69	                                                                       
67.11/31.69	         [activate(n__from(X))] =  [1 2] X + [3]                       
67.11/31.69	                                   [0 2]     [2]                       
67.11/31.69	                                >  [1 2] X + [2]                       
67.11/31.69	                                   [0 2]     [2]                       
67.11/31.69	                                =  [from(activate(X))]                 
67.11/31.69	                                                                       
67.11/31.69	            [activate(n__s(X))] =  [1 2] X + [3]                       
67.11/31.69	                                   [0 2]     [2]                       
67.11/31.69	                                >  [1 2] X + [2]                       
67.11/31.69	                                   [0 2]     [1]                       
67.11/31.69	                                =  [s(activate(X))]                    
67.11/31.69	                                                                       
67.11/31.69	                      [from(X)] =  [1 0] X + [1]                       
67.11/31.69	                                   [0 1]     [2]                       
67.11/31.69	                                >  [1 0] X + [0]                       
67.11/31.69	                                   [0 1]     [2]                       
67.11/31.69	                                =  [cons(X, n__from(n__s(X)))]         
67.11/31.69	                                                                       
67.11/31.69	                      [from(X)] =  [1 0] X + [1]                       
67.11/31.69	                                   [0 1]     [2]                       
67.11/31.69	                                >  [1 0] X + [0]                       
67.11/31.69	                                   [0 1]     [1]                       
67.11/31.69	                                =  [n__from(X)]                        
67.11/31.69	                                                                       
67.11/31.69	                         [s(X)] =  [1 0] X + [1]                       
67.11/31.69	                                   [0 1]     [1]                       
67.11/31.69	                                >  [1 0] X + [0]                       
67.11/31.69	                                   [0 1]     [1]                       
67.11/31.69	                                =  [n__s(X)]                           
67.11/31.69	                                                                       
67.11/31.69	  [2nd^#(cons1(X, cons(Y, Z)))] =  [1 0] Z + [0]                       
67.11/31.69	                                   [0 0]     [0]                       
67.11/31.69	                                ?  [1]                                 
67.11/31.69	                                   [1]                                 
67.11/31.69	                                =  [c_1()]                             
67.11/31.69	                                                                       
67.11/31.69	           [2nd^#(cons(X, X1))] =  [1 2] X1 + [0]                      
67.11/31.69	                                   [0 0]      [0]                      
67.11/31.69	                                ?  [1 2] X1 + [2]                      
67.11/31.69	                                   [0 0]      [2]                      
67.11/31.69	                                =  [c_2(2nd^#(cons1(X, activate(X1))))]
67.11/31.69	                                                                       
67.11/31.69	                [activate^#(X)] =  [1 2] X + [2]                       
67.11/31.69	                                   [1 2]     [2]                       
67.11/31.69	                                >  [1]                                 
67.11/31.69	                                   [1]                                 
67.11/31.69	                                =  [c_3()]                             
67.11/31.69	                                                                       
67.11/31.69	       [activate^#(n__from(X))] =  [1 2] X + [4]                       
67.11/31.69	                                   [1 2]     [4]                       
67.11/31.69	                                >= [1 2] X + [4]                       
67.11/31.69	                                   [0 0]     [4]                       
67.11/31.69	                                =  [c_4(from^#(activate(X)))]          
67.11/31.69	                                                                       
67.11/31.69	          [activate^#(n__s(X))] =  [1 2] X + [4]                       
67.11/31.69	                                   [1 2]     [4]                       
67.11/31.69	                                >= [1 2] X + [4]                       
67.11/31.69	                                   [0 0]     [4]                       
67.11/31.69	                                =  [c_5(s^#(activate(X)))]             
67.11/31.69	                                                                       
67.11/31.69	                    [from^#(X)] =  [1 0] X + [1]                       
67.11/31.69	                                   [0 0]     [2]                       
67.11/31.69	                                >= [1]                                 
67.11/31.69	                                   [1]                                 
67.11/31.69	                                =  [c_6()]                             
67.11/31.69	                                                                       
67.11/31.69	                    [from^#(X)] =  [1 0] X + [1]                       
67.11/31.69	                                   [0 0]     [2]                       
67.11/31.69	                                >= [1]                                 
67.11/31.69	                                   [1]                                 
67.11/31.69	                                =  [c_7()]                             
67.11/31.69	                                                                       
67.11/31.69	                       [s^#(X)] =  [1 0] X + [1]                       
67.11/31.69	                                   [0 0]     [2]                       
67.11/31.69	                                >= [1]                                 
67.11/31.69	                                   [1]                                 
67.11/31.69	                                =  [c_8()]                             
67.11/31.69	                                                                       
67.11/31.69	
67.11/31.69	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
67.11/31.69	
67.11/31.69	We are left with following problem, upon which TcT provides the
67.11/31.69	certificate YES(O(1),O(1)).
67.11/31.69	
67.11/31.69	Strict DPs:
67.11/31.69	  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	  , from^#(X) -> c_6()
67.11/31.69	  , from^#(X) -> c_7()
67.11/31.69	  , s^#(X) -> c_8() }
67.11/31.69	Weak DPs: { activate^#(X) -> c_3() }
67.11/31.69	Weak Trs:
67.11/31.69	  { activate(X) -> X
67.11/31.69	  , activate(n__from(X)) -> from(activate(X))
67.11/31.69	  , activate(n__s(X)) -> s(activate(X))
67.11/31.69	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	  , from(X) -> n__from(X)
67.11/31.69	  , s(X) -> n__s(X) }
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(1))
67.11/31.69	
67.11/31.69	We estimate the number of application of {1,5,6,7} by applications
67.11/31.69	of Pre({1,5,6,7}) = {2,3,4}. Here rules are labeled as follows:
67.11/31.69	
67.11/31.69	  DPs:
67.11/31.69	    { 1: 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	    , 2: 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	    , 3: activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	    , 4: activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	    , 5: from^#(X) -> c_6()
67.11/31.69	    , 6: from^#(X) -> c_7()
67.11/31.69	    , 7: s^#(X) -> c_8()
67.11/31.69	    , 8: activate^#(X) -> c_3() }
67.11/31.69	
67.11/31.69	We are left with following problem, upon which TcT provides the
67.11/31.69	certificate YES(O(1),O(1)).
67.11/31.69	
67.11/31.69	Strict DPs:
67.11/31.69	  { 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	  , activate^#(n__s(X)) -> c_5(s^#(activate(X))) }
67.11/31.69	Weak DPs:
67.11/31.69	  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	  , activate^#(X) -> c_3()
67.11/31.69	  , from^#(X) -> c_6()
67.11/31.69	  , from^#(X) -> c_7()
67.11/31.69	  , s^#(X) -> c_8() }
67.11/31.69	Weak Trs:
67.11/31.69	  { activate(X) -> X
67.11/31.69	  , activate(n__from(X)) -> from(activate(X))
67.11/31.69	  , activate(n__s(X)) -> s(activate(X))
67.11/31.69	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	  , from(X) -> n__from(X)
67.11/31.69	  , s(X) -> n__s(X) }
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(1))
67.11/31.69	
67.11/31.69	We estimate the number of application of {1,2,3} by applications of
67.11/31.69	Pre({1,2,3}) = {}. Here rules are labeled as follows:
67.11/31.69	
67.11/31.69	  DPs:
67.11/31.69	    { 1: 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	    , 2: activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	    , 3: activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	    , 4: 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	    , 5: activate^#(X) -> c_3()
67.11/31.69	    , 6: from^#(X) -> c_6()
67.11/31.69	    , 7: from^#(X) -> c_7()
67.11/31.69	    , 8: s^#(X) -> c_8() }
67.11/31.69	
67.11/31.69	We are left with following problem, upon which TcT provides the
67.11/31.69	certificate YES(O(1),O(1)).
67.11/31.69	
67.11/31.69	Weak DPs:
67.11/31.69	  { 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	  , 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	  , activate^#(X) -> c_3()
67.11/31.69	  , activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	  , activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	  , from^#(X) -> c_6()
67.11/31.69	  , from^#(X) -> c_7()
67.11/31.69	  , s^#(X) -> c_8() }
67.11/31.69	Weak Trs:
67.11/31.69	  { activate(X) -> X
67.11/31.69	  , activate(n__from(X)) -> from(activate(X))
67.11/31.69	  , activate(n__s(X)) -> s(activate(X))
67.11/31.69	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	  , from(X) -> n__from(X)
67.11/31.69	  , s(X) -> n__s(X) }
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(1))
67.11/31.69	
67.11/31.69	The following weak DPs constitute a sub-graph of the DG that is
67.11/31.69	closed under successors. The DPs are removed.
67.11/31.69	
67.11/31.69	{ 2nd^#(cons1(X, cons(Y, Z))) -> c_1()
67.11/31.69	, 2nd^#(cons(X, X1)) -> c_2(2nd^#(cons1(X, activate(X1))))
67.11/31.69	, activate^#(X) -> c_3()
67.11/31.69	, activate^#(n__from(X)) -> c_4(from^#(activate(X)))
67.11/31.69	, activate^#(n__s(X)) -> c_5(s^#(activate(X)))
67.11/31.69	, from^#(X) -> c_6()
67.11/31.69	, from^#(X) -> c_7()
67.11/31.69	, s^#(X) -> c_8() }
67.11/31.69	
67.11/31.69	We are left with following problem, upon which TcT provides the
67.11/31.69	certificate YES(O(1),O(1)).
67.11/31.69	
67.11/31.69	Weak Trs:
67.11/31.69	  { activate(X) -> X
67.11/31.69	  , activate(n__from(X)) -> from(activate(X))
67.11/31.69	  , activate(n__s(X)) -> s(activate(X))
67.11/31.69	  , from(X) -> cons(X, n__from(n__s(X)))
67.11/31.69	  , from(X) -> n__from(X)
67.11/31.69	  , s(X) -> n__s(X) }
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(1))
67.11/31.69	
67.11/31.69	No rule is usable, rules are removed from the input problem.
67.11/31.69	
67.11/31.69	We are left with following problem, upon which TcT provides the
67.11/31.69	certificate YES(O(1),O(1)).
67.11/31.69	
67.11/31.69	Rules: Empty
67.11/31.69	Obligation:
67.11/31.69	  innermost runtime complexity
67.11/31.69	Answer:
67.11/31.69	  YES(O(1),O(1))
67.11/31.69	
67.11/31.69	Empty rules are trivially bounded
67.11/31.69	
67.11/31.69	Hurray, we answered YES(O(1),O(n^1))
67.34/31.71	EOF