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