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