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