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