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