YES(O(1),O(n^1))
0.00/0.36	YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict Trs:
0.00/0.36	  { f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z)
0.00/0.36	  , f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	Arguments of following rules are not normal-forms:
0.00/0.36	
0.00/0.36	{ f(cons(f(cons(nil(), y)), z)) -> copy(n(), y, z) }
0.00/0.36	
0.00/0.36	All above mentioned rules can be savely removed.
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict Trs:
0.00/0.36	  { f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	We add the following dependency tuples:
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { f^#(cons(nil(), y)) -> c_1()
0.00/0.36	  , copy^#(0(), y, z) -> c_2(f^#(z))
0.00/0.36	  , copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	
0.00/0.36	and mark the set of starting terms.
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { f^#(cons(nil(), y)) -> c_1()
0.00/0.36	  , copy^#(0(), y, z) -> c_2(f^#(z))
0.00/0.36	  , copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	Weak Trs:
0.00/0.36	  { f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	We estimate the number of application of {1} by applications of
0.00/0.36	Pre({1}) = {2,3}. Here rules are labeled as follows:
0.00/0.36	
0.00/0.36	  DPs:
0.00/0.36	    { 1: f^#(cons(nil(), y)) -> c_1()
0.00/0.36	    , 2: copy^#(0(), y, z) -> c_2(f^#(z))
0.00/0.36	    , 3: copy^#(s(x), y, z) ->
0.00/0.36	         c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { copy^#(0(), y, z) -> c_2(f^#(z))
0.00/0.36	  , copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	Weak DPs: { f^#(cons(nil(), y)) -> c_1() }
0.00/0.36	Weak Trs:
0.00/0.36	  { f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	We estimate the number of application of {1} by applications of
0.00/0.36	Pre({1}) = {2}. Here rules are labeled as follows:
0.00/0.36	
0.00/0.36	  DPs:
0.00/0.36	    { 1: copy^#(0(), y, z) -> c_2(f^#(z))
0.00/0.36	    , 2: copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y))
0.00/0.36	    , 3: f^#(cons(nil(), y)) -> c_1() }
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	Weak DPs:
0.00/0.36	  { f^#(cons(nil(), y)) -> c_1()
0.00/0.36	  , copy^#(0(), y, z) -> c_2(f^#(z)) }
0.00/0.36	Weak Trs:
0.00/0.36	  { f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.36	closed under successors. The DPs are removed.
0.00/0.36	
0.00/0.36	{ f^#(cons(nil(), y)) -> c_1()
0.00/0.36	, copy^#(0(), y, z) -> c_2(f^#(z)) }
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	Weak Trs:
0.00/0.36	  { f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	Due to missing edges in the dependency-graph, the right-hand sides
0.00/0.36	of following rules could be simplified:
0.00/0.36	
0.00/0.36	  { copy^#(s(x), y, z) -> c_3(copy^#(x, y, cons(f(y), z)), f^#(y)) }
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
0.00/0.36	Weak Trs:
0.00/0.36	  { f(cons(nil(), y)) -> y
0.00/0.36	  , copy(0(), y, z) -> f(z)
0.00/0.36	  , copy(s(x), y, z) -> copy(x, y, cons(f(y), z)) }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	We replace rewrite rules by usable rules:
0.00/0.36	
0.00/0.36	  Weak Usable Rules: { f(cons(nil(), y)) -> y }
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(n^1)).
0.00/0.36	
0.00/0.36	Strict DPs:
0.00/0.36	  { copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
0.00/0.36	Weak Trs: { f(cons(nil(), y)) -> y }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(n^1))
0.00/0.36	
0.00/0.36	We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
0.00/0.36	to orient following rules strictly.
0.00/0.36	
0.00/0.36	DPs:
0.00/0.36	  { 1: copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
0.00/0.36	
0.00/0.36	Sub-proof:
0.00/0.36	----------
0.00/0.36	  The input was oriented with the instance of 'Small Polynomial Path
0.00/0.36	  Order (PS,1-bounded)' as induced by the safe mapping
0.00/0.36	  
0.00/0.36	   safe(f) = {1}, safe(cons) = {1, 2}, safe(nil) = {}, safe(s) = {1},
0.00/0.36	   safe(copy^#) = {3}, safe(c_1) = {}
0.00/0.36	  
0.00/0.36	  and precedence
0.00/0.36	  
0.00/0.36	   copy^# > f .
0.00/0.36	  
0.00/0.36	  Following symbols are considered recursive:
0.00/0.36	  
0.00/0.36	   {copy^#}
0.00/0.36	  
0.00/0.36	  The recursion depth is 1.
0.00/0.36	  
0.00/0.36	  Further, following argument filtering is employed:
0.00/0.36	  
0.00/0.36	   pi(f) = 1, pi(cons) = 1, pi(nil) = [], pi(s) = [1],
0.00/0.36	   pi(copy^#) = [1, 2], pi(c_1) = [1]
0.00/0.36	  
0.00/0.36	  Usable defined function symbols are a subset of:
0.00/0.36	  
0.00/0.36	   {copy^#}
0.00/0.36	  
0.00/0.36	  For your convenience, here are the satisfied ordering constraints:
0.00/0.36	  
0.00/0.36	    pi(copy^#(s(x), y, z)) = copy^#(s(; x),  y;)                 
0.00/0.36	                           > c_1(copy^#(x,  y;);)                
0.00/0.36	                           = pi(c_1(copy^#(x, y, cons(f(y), z))))
0.00/0.36	                                                                 
0.00/0.36	
0.00/0.36	The strictly oriented rules are moved into the weak component.
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(1)).
0.00/0.36	
0.00/0.36	Weak DPs:
0.00/0.36	  { copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
0.00/0.36	Weak Trs: { f(cons(nil(), y)) -> y }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(1))
0.00/0.36	
0.00/0.36	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.36	closed under successors. The DPs are removed.
0.00/0.36	
0.00/0.36	{ copy^#(s(x), y, z) -> c_1(copy^#(x, y, cons(f(y), z))) }
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(1)).
0.00/0.36	
0.00/0.36	Weak Trs: { f(cons(nil(), y)) -> y }
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(1))
0.00/0.36	
0.00/0.36	No rule is usable, rules are removed from the input problem.
0.00/0.36	
0.00/0.36	We are left with following problem, upon which TcT provides the
0.00/0.36	certificate YES(O(1),O(1)).
0.00/0.36	
0.00/0.36	Rules: Empty
0.00/0.36	Obligation:
0.00/0.36	  innermost runtime complexity
0.00/0.36	Answer:
0.00/0.36	  YES(O(1),O(1))
0.00/0.36	
0.00/0.36	Empty rules are trivially bounded
0.00/0.36	
0.00/0.36	Hurray, we answered YES(O(1),O(n^1))
0.00/0.36	EOF