YES(O(1),O(n^1))
0.00/0.59	YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y)
0.00/0.59	  , quot(0(), s(y)) -> 0()
0.00/0.59	  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	We add the following weak dependency pairs:
0.00/0.59	
0.00/0.59	Strict DPs:
0.00/0.59	  { minus^#(x, 0()) -> c_1(x)
0.00/0.59	  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
0.00/0.59	  , quot^#(0(), s(y)) -> c_3()
0.00/0.59	  , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	
0.00/0.59	and mark the set of starting terms.
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs:
0.00/0.59	  { minus^#(x, 0()) -> c_1(x)
0.00/0.59	  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
0.00/0.59	  , quot^#(0(), s(y)) -> c_3()
0.00/0.59	  , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	Strict Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y)
0.00/0.59	  , quot(0(), s(y)) -> 0()
0.00/0.59	  , quot(s(x), s(y)) -> s(quot(minus(x, y), s(y))) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	We replace rewrite rules by usable rules:
0.00/0.59	
0.00/0.59	  Strict Usable Rules:
0.00/0.59	    { minus(x, 0()) -> x
0.00/0.59	    , minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs:
0.00/0.59	  { minus^#(x, 0()) -> c_1(x)
0.00/0.59	  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
0.00/0.59	  , quot^#(0(), s(y)) -> c_3()
0.00/0.59	  , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	Strict Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	The weightgap principle applies (using the following constant
0.00/0.59	growth matrix-interpretation)
0.00/0.59	
0.00/0.59	The following argument positions are usable:
0.00/0.59	  Uargs(c_2) = {1}, Uargs(quot^#) = {1}, Uargs(c_4) = {1}
0.00/0.59	
0.00/0.59	TcT has computed the following constructor-restricted matrix
0.00/0.59	interpretation.
0.00/0.59	
0.00/0.59	    [minus](x1, x2) = [1 1] x1 + [2]           
0.00/0.59	                      [1 1]      [0]           
0.00/0.59	                                               
0.00/0.59	                [0] = [0]                      
0.00/0.59	                      [0]                      
0.00/0.59	                                               
0.00/0.59	            [s](x1) = [1 1] x1 + [0]           
0.00/0.59	                      [0 0]      [2]           
0.00/0.59	                                               
0.00/0.59	  [minus^#](x1, x2) = [0 0] x1 + [0 0] x2 + [2]
0.00/0.59	                      [1 1]      [1 1]      [2]
0.00/0.59	                                               
0.00/0.59	          [c_1](x1) = [0 0] x1 + [1]           
0.00/0.59	                      [1 1]      [1]           
0.00/0.59	                                               
0.00/0.59	          [c_2](x1) = [1 0] x1 + [1]           
0.00/0.59	                      [0 1]      [1]           
0.00/0.59	                                               
0.00/0.59	   [quot^#](x1, x2) = [1 0] x1 + [1]           
0.00/0.59	                      [0 0]      [0]           
0.00/0.59	                                               
0.00/0.59	              [c_3] = [0]                      
0.00/0.59	                      [0]                      
0.00/0.59	                                               
0.00/0.59	          [c_4](x1) = [1 0] x1 + [1]           
0.00/0.59	                      [0 1]      [2]           
0.00/0.59	
0.00/0.59	The order satisfies the following ordering constraints:
0.00/0.59	
0.00/0.59	        [minus(x, 0())] = [1 1] x + [2]                   
0.00/0.59	                          [1 1]     [0]                   
0.00/0.59	                        > [1 0] x + [0]                   
0.00/0.59	                          [0 1]     [0]                   
0.00/0.59	                        = [x]                             
0.00/0.59	                                                          
0.00/0.59	    [minus(s(x), s(y))] = [1 1] x + [4]                   
0.00/0.59	                          [1 1]     [2]                   
0.00/0.59	                        > [1 1] x + [2]                   
0.00/0.59	                          [1 1]     [0]                   
0.00/0.59	                        = [minus(x, y)]                   
0.00/0.59	                                                          
0.00/0.59	      [minus^#(x, 0())] = [0 0] x + [2]                   
0.00/0.59	                          [1 1]     [2]                   
0.00/0.59	                        > [0 0] x + [1]                   
0.00/0.59	                          [1 1]     [1]                   
0.00/0.59	                        = [c_1(x)]                        
0.00/0.59	                                                          
0.00/0.59	  [minus^#(s(x), s(y))] = [0 0] x + [0 0] y + [2]         
0.00/0.59	                          [1 1]     [1 1]     [6]         
0.00/0.59	                        ? [0 0] x + [0 0] y + [3]         
0.00/0.59	                          [1 1]     [1 1]     [3]         
0.00/0.59	                        = [c_2(minus^#(x, y))]            
0.00/0.59	                                                          
0.00/0.59	    [quot^#(0(), s(y))] = [1]                             
0.00/0.59	                          [0]                             
0.00/0.59	                        > [0]                             
0.00/0.59	                          [0]                             
0.00/0.59	                        = [c_3()]                         
0.00/0.59	                                                          
0.00/0.59	   [quot^#(s(x), s(y))] = [1 1] x + [1]                   
0.00/0.59	                          [0 0]     [0]                   
0.00/0.59	                        ? [1 1] x + [4]                   
0.00/0.59	                          [0 0]     [2]                   
0.00/0.59	                        = [c_4(quot^#(minus(x, y), s(y)))]
0.00/0.59	                                                          
0.00/0.59	
0.00/0.59	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs:
0.00/0.59	  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
0.00/0.59	  , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	Weak DPs:
0.00/0.59	  { minus^#(x, 0()) -> c_1(x)
0.00/0.59	  , quot^#(0(), s(y)) -> c_3() }
0.00/0.59	Weak Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.59	closed under successors. The DPs are removed.
0.00/0.59	
0.00/0.59	{ quot^#(0(), s(y)) -> c_3() }
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs:
0.00/0.59	  { minus^#(s(x), s(y)) -> c_2(minus^#(x, y))
0.00/0.59	  , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	Weak DPs: { minus^#(x, 0()) -> c_1(x) }
0.00/0.59	Weak Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	We use the processor 'matrix interpretation of dimension 1' to
0.00/0.59	orient following rules strictly.
0.00/0.59	
0.00/0.59	DPs:
0.00/0.59	  { 2: quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	Trs: { minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	
0.00/0.59	Sub-proof:
0.00/0.59	----------
0.00/0.59	  The following argument positions are usable:
0.00/0.59	    Uargs(c_2) = {1}, Uargs(c_4) = {1}
0.00/0.59	  
0.00/0.59	  TcT has computed the following constructor-based matrix
0.00/0.59	  interpretation satisfying not(EDA).
0.00/0.59	  
0.00/0.59	      [minus](x1, x2) = [1] x1 + [0]
0.00/0.59	                                    
0.00/0.59	                  [0] = [0]         
0.00/0.59	                                    
0.00/0.59	              [s](x1) = [1] x1 + [1]
0.00/0.59	                                    
0.00/0.59	    [minus^#](x1, x2) = [0]         
0.00/0.59	                                    
0.00/0.59	            [c_1](x1) = [0]         
0.00/0.59	                                    
0.00/0.59	            [c_2](x1) = [2] x1 + [0]
0.00/0.59	                                    
0.00/0.59	     [quot^#](x1, x2) = [1] x1 + [0]
0.00/0.59	                                    
0.00/0.59	            [c_4](x1) = [1] x1 + [0]
0.00/0.59	  
0.00/0.59	  The order satisfies the following ordering constraints:
0.00/0.59	  
0.00/0.59	          [minus(x, 0())] =  [1] x + [0]                     
0.00/0.59	                          >= [1] x + [0]                     
0.00/0.59	                          =  [x]                             
0.00/0.59	                                                             
0.00/0.59	      [minus(s(x), s(y))] =  [1] x + [1]                     
0.00/0.59	                          >  [1] x + [0]                     
0.00/0.59	                          =  [minus(x, y)]                   
0.00/0.59	                                                             
0.00/0.59	        [minus^#(x, 0())] =  [0]                             
0.00/0.59	                          >= [0]                             
0.00/0.59	                          =  [c_1(x)]                        
0.00/0.59	                                                             
0.00/0.59	    [minus^#(s(x), s(y))] =  [0]                             
0.00/0.59	                          >= [0]                             
0.00/0.59	                          =  [c_2(minus^#(x, y))]            
0.00/0.59	                                                             
0.00/0.59	     [quot^#(s(x), s(y))] =  [1] x + [1]                     
0.00/0.59	                          >  [1] x + [0]                     
0.00/0.59	                          =  [c_4(quot^#(minus(x, y), s(y)))]
0.00/0.59	                                                             
0.00/0.59	
0.00/0.59	The strictly oriented rules are moved into the weak component.
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) }
0.00/0.59	Weak DPs:
0.00/0.59	  { minus^#(x, 0()) -> c_1(x)
0.00/0.59	  , quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	Weak Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.59	closed under successors. The DPs are removed.
0.00/0.59	
0.00/0.59	{ quot^#(s(x), s(y)) -> c_4(quot^#(minus(x, y), s(y))) }
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) }
0.00/0.59	Weak DPs: { minus^#(x, 0()) -> c_1(x) }
0.00/0.59	Weak Trs:
0.00/0.59	  { minus(x, 0()) -> x
0.00/0.59	  , minus(s(x), s(y)) -> minus(x, y) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	No rule is usable, rules are removed from the input problem.
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(n^1)).
0.00/0.59	
0.00/0.59	Strict DPs: { minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) }
0.00/0.59	Weak DPs: { minus^#(x, 0()) -> c_1(x) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(n^1))
0.00/0.59	
0.00/0.59	We use the processor 'matrix interpretation of dimension 1' to
0.00/0.59	orient following rules strictly.
0.00/0.59	
0.00/0.59	DPs:
0.00/0.59	  { 1: minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) }
0.00/0.59	
0.00/0.59	Sub-proof:
0.00/0.59	----------
0.00/0.59	  The following argument positions are usable:
0.00/0.59	    Uargs(c_2) = {1}
0.00/0.59	  
0.00/0.59	  TcT has computed the following constructor-based matrix
0.00/0.59	  interpretation satisfying not(EDA).
0.00/0.59	  
0.00/0.59	      [minus](x1, x2) = [7] x1 + [7] x2 + [0]
0.00/0.59	                                             
0.00/0.59	                  [0] = [7]                  
0.00/0.59	                                             
0.00/0.59	              [s](x1) = [1] x1 + [4]         
0.00/0.59	                                             
0.00/0.59	    [minus^#](x1, x2) = [2] x1 + [0]         
0.00/0.59	                                             
0.00/0.59	            [c_1](x1) = [2] x1 + [0]         
0.00/0.59	                                             
0.00/0.59	            [c_2](x1) = [1] x1 + [1]         
0.00/0.59	                                             
0.00/0.59	     [quot^#](x1, x2) = [7] x1 + [7] x2 + [0]
0.00/0.59	                                             
0.00/0.59	            [c_4](x1) = [7] x1 + [0]         
0.00/0.59	  
0.00/0.59	  The order satisfies the following ordering constraints:
0.00/0.59	  
0.00/0.59	        [minus^#(x, 0())] =  [2] x + [0]         
0.00/0.59	                          >= [2] x + [0]         
0.00/0.59	                          =  [c_1(x)]            
0.00/0.59	                                                 
0.00/0.59	    [minus^#(s(x), s(y))] =  [2] x + [8]         
0.00/0.59	                          >  [2] x + [1]         
0.00/0.59	                          =  [c_2(minus^#(x, y))]
0.00/0.59	                                                 
0.00/0.59	
0.00/0.59	The strictly oriented rules are moved into the weak component.
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(1)).
0.00/0.59	
0.00/0.59	Weak DPs:
0.00/0.59	  { minus^#(x, 0()) -> c_1(x)
0.00/0.59	  , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) }
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(1))
0.00/0.59	
0.00/0.59	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.59	closed under successors. The DPs are removed.
0.00/0.59	
0.00/0.59	{ minus^#(x, 0()) -> c_1(x)
0.00/0.59	, minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) }
0.00/0.59	
0.00/0.59	We are left with following problem, upon which TcT provides the
0.00/0.59	certificate YES(O(1),O(1)).
0.00/0.59	
0.00/0.59	Rules: Empty
0.00/0.59	Obligation:
0.00/0.59	  runtime complexity
0.00/0.59	Answer:
0.00/0.59	  YES(O(1),O(1))
0.00/0.59	
0.00/0.59	Empty rules are trivially bounded
0.00/0.59	
0.00/0.59	Hurray, we answered YES(O(1),O(n^1))
0.00/0.59	EOF