YES(O(1),O(n^1))
15.47/8.51	YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(n^1)).
15.47/8.51	
15.47/8.51	Strict Trs:
15.47/8.51	  { div(x, y) -> quot(x, y, y)
15.47/8.51	  , div(0(), y) -> 0()
15.47/8.51	  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
15.47/8.51	  , quot(0(), s(y), z) -> 0()
15.47/8.51	  , quot(s(x), s(y), z) -> quot(x, y, z) }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	We add the following weak dependency pairs:
15.47/8.51	
15.47/8.51	Strict DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , div^#(0(), y) -> c_2()
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(0(), s(y), z) -> c_4()
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	
15.47/8.51	and mark the set of starting terms.
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(n^1)).
15.47/8.51	
15.47/8.51	Strict DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , div^#(0(), y) -> c_2()
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(0(), s(y), z) -> c_4()
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	Strict Trs:
15.47/8.51	  { div(x, y) -> quot(x, y, y)
15.47/8.51	  , div(0(), y) -> 0()
15.47/8.51	  , quot(x, 0(), s(z)) -> s(div(x, s(z)))
15.47/8.51	  , quot(0(), s(y), z) -> 0()
15.47/8.51	  , quot(s(x), s(y), z) -> quot(x, y, z) }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	No rule is usable, rules are removed from the input problem.
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(n^1)).
15.47/8.51	
15.47/8.51	Strict DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , div^#(0(), y) -> c_2()
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(0(), s(y), z) -> c_4()
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	The weightgap principle applies (using the following constant
15.47/8.51	growth matrix-interpretation)
15.47/8.51	
15.47/8.51	The following argument positions are usable:
15.47/8.51	  Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1}
15.47/8.51	
15.47/8.51	TcT has computed the following constructor-restricted matrix
15.47/8.51	interpretation.
15.47/8.51	
15.47/8.51	                   [0] = [0]           
15.47/8.51	                         [0]           
15.47/8.51	                                       
15.47/8.51	               [s](x1) = [0]           
15.47/8.51	                         [0]           
15.47/8.51	                                       
15.47/8.51	       [div^#](x1, x2) = [1]           
15.47/8.51	                         [0]           
15.47/8.51	                                       
15.47/8.51	             [c_1](x1) = [1 0] x1 + [2]
15.47/8.51	                         [0 1]      [2]
15.47/8.51	                                       
15.47/8.51	  [quot^#](x1, x2, x3) = [0]           
15.47/8.51	                         [0]           
15.47/8.51	                                       
15.47/8.51	                 [c_2] = [0]           
15.47/8.51	                         [0]           
15.47/8.51	                                       
15.47/8.51	             [c_3](x1) = [1 0] x1 + [0]
15.47/8.51	                         [0 1]      [1]
15.47/8.51	                                       
15.47/8.51	                 [c_4] = [1]           
15.47/8.51	                         [0]           
15.47/8.51	                                       
15.47/8.51	             [c_5](x1) = [1 0] x1 + [2]
15.47/8.51	                         [0 1]      [0]
15.47/8.51	
15.47/8.51	The order satisfies the following ordering constraints:
15.47/8.51	
15.47/8.51	            [div^#(x, y)] = [1]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          ? [2]                   
15.47/8.51	                            [2]                   
15.47/8.51	                          = [c_1(quot^#(x, y, y))]
15.47/8.51	                                                  
15.47/8.51	          [div^#(0(), y)] = [1]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          > [0]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          = [c_2()]               
15.47/8.51	                                                  
15.47/8.51	   [quot^#(x, 0(), s(z))] = [0]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          ? [1]                   
15.47/8.51	                            [1]                   
15.47/8.51	                          = [c_3(div^#(x, s(z)))] 
15.47/8.51	                                                  
15.47/8.51	   [quot^#(0(), s(y), z)] = [0]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          ? [1]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          = [c_4()]               
15.47/8.51	                                                  
15.47/8.51	  [quot^#(s(x), s(y), z)] = [0]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          ? [2]                   
15.47/8.51	                            [0]                   
15.47/8.51	                          = [c_5(quot^#(x, y, z))]
15.47/8.51	                                                  
15.47/8.51	
15.47/8.51	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(n^1)).
15.47/8.51	
15.47/8.51	Strict DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(0(), s(y), z) -> c_4()
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	Weak DPs: { div^#(0(), y) -> c_2() }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	We estimate the number of application of {3} by applications of
15.47/8.51	Pre({3}) = {1,4}. Here rules are labeled as follows:
15.47/8.51	
15.47/8.51	  DPs:
15.47/8.51	    { 1: div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	    , 2: quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	    , 3: quot^#(0(), s(y), z) -> c_4()
15.47/8.51	    , 4: quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z))
15.47/8.51	    , 5: div^#(0(), y) -> c_2() }
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(n^1)).
15.47/8.51	
15.47/8.51	Strict DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	Weak DPs:
15.47/8.51	  { div^#(0(), y) -> c_2()
15.47/8.51	  , quot^#(0(), s(y), z) -> c_4() }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	The following weak DPs constitute a sub-graph of the DG that is
15.47/8.51	closed under successors. The DPs are removed.
15.47/8.51	
15.47/8.51	{ div^#(0(), y) -> c_2()
15.47/8.51	, quot^#(0(), s(y), z) -> c_4() }
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(n^1)).
15.47/8.51	
15.47/8.51	Strict DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(n^1))
15.47/8.51	
15.47/8.51	We use the processor 'matrix interpretation of dimension 1' to
15.47/8.51	orient following rules strictly.
15.47/8.51	
15.47/8.51	DPs:
15.47/8.51	  { 3: quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	
15.47/8.51	Sub-proof:
15.47/8.51	----------
15.47/8.51	  The following argument positions are usable:
15.47/8.51	    Uargs(c_1) = {1}, Uargs(c_3) = {1}, Uargs(c_5) = {1}
15.47/8.51	  
15.47/8.51	  TcT has computed the following constructor-based matrix
15.47/8.51	  interpretation satisfying not(EDA).
15.47/8.51	  
15.47/8.51	                     [0] = [7]         
15.47/8.51	                                       
15.47/8.51	                 [s](x1) = [1] x1 + [4]
15.47/8.51	                                       
15.47/8.51	         [div^#](x1, x2) = [2] x1 + [0]
15.47/8.51	                                       
15.47/8.51	               [c_1](x1) = [1] x1 + [0]
15.47/8.51	                                       
15.47/8.51	    [quot^#](x1, x2, x3) = [2] x1 + [0]
15.47/8.51	                                       
15.47/8.51	               [c_3](x1) = [1] x1 + [0]
15.47/8.51	                                       
15.47/8.51	               [c_5](x1) = [1] x1 + [5]
15.47/8.51	  
15.47/8.51	  The order satisfies the following ordering constraints:
15.47/8.51	  
15.47/8.51	              [div^#(x, y)] =  [2] x + [0]           
15.47/8.51	                            >= [2] x + [0]           
15.47/8.51	                            =  [c_1(quot^#(x, y, y))]
15.47/8.51	                                                     
15.47/8.51	     [quot^#(x, 0(), s(z))] =  [2] x + [0]           
15.47/8.51	                            >= [2] x + [0]           
15.47/8.51	                            =  [c_3(div^#(x, s(z)))] 
15.47/8.51	                                                     
15.47/8.51	    [quot^#(s(x), s(y), z)] =  [2] x + [8]           
15.47/8.51	                            >  [2] x + [5]           
15.47/8.51	                            =  [c_5(quot^#(x, y, z))]
15.47/8.51	                                                     
15.47/8.51	
15.47/8.51	We return to the main proof. Consider the set of all dependency
15.47/8.51	pairs
15.47/8.51	
15.47/8.51	:
15.47/8.51	  { 1: div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , 2: quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , 3: quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	
15.47/8.51	Processor 'matrix interpretation of dimension 1' induces the
15.47/8.51	complexity certificate YES(?,O(n^1)) on application of dependency
15.47/8.51	pairs {3}. These cover all (indirect) predecessors of dependency
15.47/8.51	pairs {1,2,3}, their number of application is equally bounded. The
15.47/8.51	dependency pairs are shifted into the weak component.
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(1)).
15.47/8.51	
15.47/8.51	Weak DPs:
15.47/8.51	  { div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	  , quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	  , quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(1))
15.47/8.51	
15.47/8.51	The following weak DPs constitute a sub-graph of the DG that is
15.47/8.51	closed under successors. The DPs are removed.
15.47/8.51	
15.47/8.51	{ div^#(x, y) -> c_1(quot^#(x, y, y))
15.47/8.51	, quot^#(x, 0(), s(z)) -> c_3(div^#(x, s(z)))
15.47/8.51	, quot^#(s(x), s(y), z) -> c_5(quot^#(x, y, z)) }
15.47/8.51	
15.47/8.51	We are left with following problem, upon which TcT provides the
15.47/8.51	certificate YES(O(1),O(1)).
15.47/8.51	
15.47/8.51	Rules: Empty
15.47/8.51	Obligation:
15.47/8.51	  runtime complexity
15.47/8.51	Answer:
15.47/8.51	  YES(O(1),O(1))
15.47/8.51	
15.47/8.51	Empty rules are trivially bounded
15.47/8.51	
15.47/8.51	Hurray, we answered YES(O(1),O(n^1))
15.47/8.52	EOF