YES(O(1),O(n^1))
0.00/0.67	YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(n^1)).
0.00/0.67	
0.00/0.67	Strict Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X
0.00/0.67	  , div(0(), s(Y)) -> 0()
0.00/0.67	  , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y))) }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	We add the following weak dependency pairs:
0.00/0.67	
0.00/0.67	Strict DPs:
0.00/0.67	  { minus^#(X, 0()) -> c_1()
0.00/0.67	  , minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	  , p^#(s(X)) -> c_3()
0.00/0.67	  , div^#(0(), s(Y)) -> c_4()
0.00/0.67	  , div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	
0.00/0.67	and mark the set of starting terms.
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(n^1)).
0.00/0.67	
0.00/0.67	Strict DPs:
0.00/0.67	  { minus^#(X, 0()) -> c_1()
0.00/0.67	  , minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	  , p^#(s(X)) -> c_3()
0.00/0.67	  , div^#(0(), s(Y)) -> c_4()
0.00/0.67	  , div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Strict Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X
0.00/0.67	  , div(0(), s(Y)) -> 0()
0.00/0.67	  , div(s(X), s(Y)) -> s(div(minus(X, Y), s(Y))) }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	We replace rewrite rules by usable rules:
0.00/0.67	
0.00/0.67	  Strict Usable Rules:
0.00/0.67	    { minus(X, 0()) -> X
0.00/0.67	    , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	    , p(s(X)) -> X }
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(n^1)).
0.00/0.67	
0.00/0.67	Strict DPs:
0.00/0.67	  { minus^#(X, 0()) -> c_1()
0.00/0.67	  , minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	  , p^#(s(X)) -> c_3()
0.00/0.67	  , div^#(0(), s(Y)) -> c_4()
0.00/0.67	  , div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Strict Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	The weightgap principle applies (using the following constant
0.00/0.67	growth matrix-interpretation)
0.00/0.67	
0.00/0.67	The following argument positions are usable:
0.00/0.67	  Uargs(p) = {1}, Uargs(c_2) = {1}, Uargs(p^#) = {1},
0.00/0.67	  Uargs(div^#) = {1}, Uargs(c_5) = {1}
0.00/0.67	
0.00/0.67	TcT has computed the following constructor-restricted matrix
0.00/0.67	interpretation.
0.00/0.67	
0.00/0.67	    [minus](x1, x2) = [1 0] x1 + [2]           
0.00/0.67	                      [2 2]      [0]           
0.00/0.67	                                               
0.00/0.67	                [0] = [0]                      
0.00/0.67	                      [0]                      
0.00/0.67	                                               
0.00/0.67	            [s](x1) = [1 2] x1 + [2]           
0.00/0.67	                      [0 0]      [0]           
0.00/0.67	                                               
0.00/0.67	            [p](x1) = [1 0] x1 + [0]           
0.00/0.67	                      [2 0]      [0]           
0.00/0.67	                                               
0.00/0.67	  [minus^#](x1, x2) = [2 0] x1 + [0 0] x2 + [2]
0.00/0.67	                      [1 2]      [1 1]      [2]
0.00/0.67	                                               
0.00/0.67	              [c_1] = [1]                      
0.00/0.67	                      [1]                      
0.00/0.67	                                               
0.00/0.67	          [c_2](x1) = [1 0] x1 + [1]           
0.00/0.67	                      [0 1]      [2]           
0.00/0.67	                                               
0.00/0.67	          [p^#](x1) = [2 0] x1 + [2]           
0.00/0.67	                      [0 0]      [2]           
0.00/0.67	                                               
0.00/0.67	              [c_3] = [1]                      
0.00/0.67	                      [1]                      
0.00/0.67	                                               
0.00/0.67	    [div^#](x1, x2) = [1 0] x1 + [0]           
0.00/0.67	                      [0 0]      [0]           
0.00/0.67	                                               
0.00/0.67	              [c_4] = [1]                      
0.00/0.67	                      [1]                      
0.00/0.67	                                               
0.00/0.67	          [c_5](x1) = [1 0] x1 + [2]           
0.00/0.67	                      [0 1]      [2]           
0.00/0.67	
0.00/0.67	The order satisfies the following ordering constraints:
0.00/0.67	
0.00/0.67	        [minus(X, 0())] = [1 0] X + [2]                  
0.00/0.67	                          [2 2]     [0]                  
0.00/0.67	                        > [1 0] X + [0]                  
0.00/0.67	                          [0 1]     [0]                  
0.00/0.67	                        = [X]                            
0.00/0.67	                                                         
0.00/0.67	    [minus(s(X), s(Y))] = [1 2] X + [4]                  
0.00/0.67	                          [2 4]     [4]                  
0.00/0.67	                        > [1 0] X + [2]                  
0.00/0.67	                          [2 0]     [4]                  
0.00/0.67	                        = [p(minus(X, Y))]               
0.00/0.67	                                                         
0.00/0.67	              [p(s(X))] = [1 2] X + [2]                  
0.00/0.67	                          [2 4]     [4]                  
0.00/0.67	                        > [1 0] X + [0]                  
0.00/0.67	                          [0 1]     [0]                  
0.00/0.67	                        = [X]                            
0.00/0.67	                                                         
0.00/0.67	      [minus^#(X, 0())] = [2 0] X + [2]                  
0.00/0.67	                          [1 2]     [2]                  
0.00/0.67	                        > [1]                            
0.00/0.67	                          [1]                            
0.00/0.67	                        = [c_1()]                        
0.00/0.67	                                                         
0.00/0.67	  [minus^#(s(X), s(Y))] = [2 4] X + [0 0] Y + [6]        
0.00/0.67	                          [1 2]     [1 2]     [6]        
0.00/0.67	                        ? [2 0] X + [7]                  
0.00/0.67	                          [0 0]     [4]                  
0.00/0.67	                        = [c_2(p^#(minus(X, Y)))]        
0.00/0.67	                                                         
0.00/0.67	            [p^#(s(X))] = [2 4] X + [6]                  
0.00/0.67	                          [0 0]     [2]                  
0.00/0.67	                        > [1]                            
0.00/0.67	                          [1]                            
0.00/0.67	                        = [c_3()]                        
0.00/0.67	                                                         
0.00/0.67	     [div^#(0(), s(Y))] = [0]                            
0.00/0.67	                          [0]                            
0.00/0.67	                        ? [1]                            
0.00/0.67	                          [1]                            
0.00/0.67	                        = [c_4()]                        
0.00/0.67	                                                         
0.00/0.67	    [div^#(s(X), s(Y))] = [1 2] X + [2]                  
0.00/0.67	                          [0 0]     [0]                  
0.00/0.67	                        ? [1 0] X + [4]                  
0.00/0.67	                          [0 0]     [2]                  
0.00/0.67	                        = [c_5(div^#(minus(X, Y), s(Y)))]
0.00/0.67	                                                         
0.00/0.67	
0.00/0.67	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(n^1)).
0.00/0.67	
0.00/0.67	Strict DPs:
0.00/0.67	  { minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	  , div^#(0(), s(Y)) -> c_4()
0.00/0.67	  , div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Weak DPs:
0.00/0.67	  { minus^#(X, 0()) -> c_1()
0.00/0.67	  , p^#(s(X)) -> c_3() }
0.00/0.67	Weak Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	We estimate the number of application of {1,2} by applications of
0.00/0.67	Pre({1,2}) = {3}. Here rules are labeled as follows:
0.00/0.67	
0.00/0.67	  DPs:
0.00/0.67	    { 1: minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	    , 2: div^#(0(), s(Y)) -> c_4()
0.00/0.67	    , 3: div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y)))
0.00/0.67	    , 4: minus^#(X, 0()) -> c_1()
0.00/0.67	    , 5: p^#(s(X)) -> c_3() }
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(n^1)).
0.00/0.67	
0.00/0.67	Strict DPs: { div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Weak DPs:
0.00/0.67	  { minus^#(X, 0()) -> c_1()
0.00/0.67	  , minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	  , p^#(s(X)) -> c_3()
0.00/0.67	  , div^#(0(), s(Y)) -> c_4() }
0.00/0.67	Weak Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.67	closed under successors. The DPs are removed.
0.00/0.67	
0.00/0.67	{ minus^#(X, 0()) -> c_1()
0.00/0.67	, minus^#(s(X), s(Y)) -> c_2(p^#(minus(X, Y)))
0.00/0.67	, p^#(s(X)) -> c_3()
0.00/0.67	, div^#(0(), s(Y)) -> c_4() }
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(n^1)).
0.00/0.67	
0.00/0.67	Strict DPs: { div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Weak Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(n^1))
0.00/0.67	
0.00/0.67	We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
0.00/0.67	to orient following rules strictly.
0.00/0.67	
0.00/0.67	DPs:
0.00/0.67	  { 1: div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Trs:
0.00/0.67	  { minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	
0.00/0.67	Sub-proof:
0.00/0.67	----------
0.00/0.67	  The input was oriented with the instance of 'Small Polynomial Path
0.00/0.67	  Order (PS,1-bounded)' as induced by the safe mapping
0.00/0.67	  
0.00/0.67	   safe(minus) = {}, safe(0) = {}, safe(s) = {1}, safe(p) = {},
0.00/0.67	   safe(div^#) = {}, safe(c_5) = {}
0.00/0.67	  
0.00/0.67	  and precedence
0.00/0.67	  
0.00/0.67	   minus > p, minus ~ div^# .
0.00/0.67	  
0.00/0.67	  Following symbols are considered recursive:
0.00/0.67	  
0.00/0.67	   {p, div^#}
0.00/0.67	  
0.00/0.67	  The recursion depth is 1.
0.00/0.67	  
0.00/0.67	  Further, following argument filtering is employed:
0.00/0.67	  
0.00/0.67	   pi(minus) = 1, pi(0) = [], pi(s) = [1], pi(p) = 1,
0.00/0.67	   pi(div^#) = [1, 2], pi(c_5) = [1]
0.00/0.67	  
0.00/0.67	  Usable defined function symbols are a subset of:
0.00/0.67	  
0.00/0.67	   {minus, p, div^#}
0.00/0.67	  
0.00/0.67	  For your convenience, here are the satisfied ordering constraints:
0.00/0.67	  
0.00/0.67	    pi(div^#(s(X), s(Y))) =  div^#(s(; X),  s(; Y);)          
0.00/0.67	                          >  c_5(div^#(X,  s(; Y););)         
0.00/0.67	                          =  pi(c_5(div^#(minus(X, Y), s(Y))))
0.00/0.67	                                                              
0.00/0.67	        pi(minus(X, 0())) =  X                                
0.00/0.67	                          >= X                                
0.00/0.67	                          =  pi(X)                            
0.00/0.67	                                                              
0.00/0.67	    pi(minus(s(X), s(Y))) =  s(; X)                           
0.00/0.67	                          >  X                                
0.00/0.67	                          =  pi(p(minus(X, Y)))               
0.00/0.67	                                                              
0.00/0.67	              pi(p(s(X))) =  s(; X)                           
0.00/0.67	                          >  X                                
0.00/0.67	                          =  pi(X)                            
0.00/0.67	                                                              
0.00/0.67	
0.00/0.67	The strictly oriented rules are moved into the weak component.
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(1)).
0.00/0.67	
0.00/0.67	Weak DPs: { div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	Weak Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(1))
0.00/0.67	
0.00/0.67	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.67	closed under successors. The DPs are removed.
0.00/0.67	
0.00/0.67	{ div^#(s(X), s(Y)) -> c_5(div^#(minus(X, Y), s(Y))) }
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(1)).
0.00/0.67	
0.00/0.67	Weak Trs:
0.00/0.67	  { minus(X, 0()) -> X
0.00/0.67	  , minus(s(X), s(Y)) -> p(minus(X, Y))
0.00/0.67	  , p(s(X)) -> X }
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(1))
0.00/0.67	
0.00/0.67	No rule is usable, rules are removed from the input problem.
0.00/0.67	
0.00/0.67	We are left with following problem, upon which TcT provides the
0.00/0.67	certificate YES(O(1),O(1)).
0.00/0.67	
0.00/0.67	Rules: Empty
0.00/0.67	Obligation:
0.00/0.67	  innermost runtime complexity
0.00/0.67	Answer:
0.00/0.67	  YES(O(1),O(1))
0.00/0.67	
0.00/0.67	Empty rules are trivially bounded
0.00/0.67	
0.00/0.67	Hurray, we answered YES(O(1),O(n^1))
0.00/0.67	EOF