YES(O(1),O(n^1))
2.62/1.08	YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict Trs:
2.62/1.08	  { perfectp(0()) -> false()
2.62/1.08	  , perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
2.62/1.08	  , f(0(), y, 0(), u) -> true()
2.62/1.08	  , f(0(), y, s(z), u) -> false()
2.62/1.08	  , f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
2.62/1.08	  , f(s(x), s(y), z, u) ->
2.62/1.08	    if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	We add the following weak dependency pairs:
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(0()) -> c_1()
2.62/1.08	  , perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	  , f^#(0(), y, s(z), u) -> c_4()
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	
2.62/1.08	and mark the set of starting terms.
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(0()) -> c_1()
2.62/1.08	  , perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	  , f^#(0(), y, s(z), u) -> c_4()
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	Strict Trs:
2.62/1.08	  { perfectp(0()) -> false()
2.62/1.08	  , perfectp(s(x)) -> f(x, s(0()), s(x), s(x))
2.62/1.08	  , f(0(), y, 0(), u) -> true()
2.62/1.08	  , f(0(), y, s(z), u) -> false()
2.62/1.08	  , f(s(x), 0(), z, u) -> f(x, u, minus(z, s(x)), u)
2.62/1.08	  , f(s(x), s(y), z, u) ->
2.62/1.08	    if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	No rule is usable, rules are removed from the input problem.
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(0()) -> c_1()
2.62/1.08	  , perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	  , f^#(0(), y, s(z), u) -> c_4()
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	The weightgap principle applies (using the following constant
2.62/1.08	growth matrix-interpretation)
2.62/1.08	
2.62/1.08	The following argument positions are usable:
2.62/1.08	  Uargs(c_2) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {2}
2.62/1.08	
2.62/1.08	TcT has computed the following constructor-restricted matrix
2.62/1.08	interpretation.
2.62/1.08	
2.62/1.08	                    [0] = [0]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	                [s](x1) = [0]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	        [minus](x1, x2) = [1 0] x1 + [0]
2.62/1.08	                          [0 0]      [0]
2.62/1.08	                                        
2.62/1.08	       [perfectp^#](x1) = [0]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	                  [c_1] = [1]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	              [c_2](x1) = [1 0] x1 + [0]
2.62/1.08	                          [0 1]      [0]
2.62/1.08	                                        
2.62/1.08	  [f^#](x1, x2, x3, x4) = [1]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	                  [c_3] = [0]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	                  [c_4] = [0]           
2.62/1.08	                          [0]           
2.62/1.08	                                        
2.62/1.08	              [c_5](x1) = [1 0] x1 + [0]
2.62/1.08	                          [0 1]      [0]
2.62/1.08	                                        
2.62/1.08	          [c_6](x1, x2) = [1 0] x2 + [0]
2.62/1.08	                          [0 1]      [0]
2.62/1.08	
2.62/1.08	The order satisfies the following ordering constraints:
2.62/1.08	
2.62/1.08	        [perfectp^#(0())] =  [0]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          ?  [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          =  [c_1()]                                             
2.62/1.08	                                                                                 
2.62/1.08	       [perfectp^#(s(x))] =  [0]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          ?  [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          =  [c_2(f^#(x, s(0()), s(x), s(x)))]                   
2.62/1.08	                                                                                 
2.62/1.08	    [f^#(0(), y, 0(), u)] =  [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          >  [0]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          =  [c_3()]                                             
2.62/1.08	                                                                                 
2.62/1.08	   [f^#(0(), y, s(z), u)] =  [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          >  [0]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          =  [c_4()]                                             
2.62/1.08	                                                                                 
2.62/1.08	   [f^#(s(x), 0(), z, u)] =  [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          >= [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          =  [c_5(f^#(x, u, minus(z, s(x)), u))]                 
2.62/1.08	                                                                                 
2.62/1.08	  [f^#(s(x), s(y), z, u)] =  [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          >= [1]                                                 
2.62/1.08	                             [0]                                                 
2.62/1.08	                          =  [c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u))]
2.62/1.08	                                                                                 
2.62/1.08	
2.62/1.08	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(0()) -> c_1()
2.62/1.08	  , perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	Weak DPs:
2.62/1.08	  { f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	  , f^#(0(), y, s(z), u) -> c_4() }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	We estimate the number of application of {1} by applications of
2.62/1.08	Pre({1}) = {}. Here rules are labeled as follows:
2.62/1.08	
2.62/1.08	  DPs:
2.62/1.08	    { 1: perfectp^#(0()) -> c_1()
2.62/1.08	    , 2: perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	    , 3: f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	    , 4: f^#(s(x), s(y), z, u) ->
2.62/1.08	         c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u))
2.62/1.08	    , 5: f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	    , 6: f^#(0(), y, s(z), u) -> c_4() }
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	Weak DPs:
2.62/1.08	  { perfectp^#(0()) -> c_1()
2.62/1.08	  , f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	  , f^#(0(), y, s(z), u) -> c_4() }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	The following weak DPs constitute a sub-graph of the DG that is
2.62/1.08	closed under successors. The DPs are removed.
2.62/1.08	
2.62/1.08	{ perfectp^#(0()) -> c_1()
2.62/1.08	, f^#(0(), y, 0(), u) -> c_3()
2.62/1.08	, f^#(0(), y, s(z), u) -> c_4() }
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(s(x)) -> c_2(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_5(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	Due to missing edges in the dependency-graph, the right-hand sides
2.62/1.08	of following rules could be simplified:
2.62/1.08	
2.62/1.08	  { f^#(s(x), s(y), z, u) ->
2.62/1.08	    c_6(f^#(s(x), minus(y, x), z, u), f^#(x, u, z, u)) }
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { perfectp^#(s(x)) -> c_1(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	  , f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	Consider the dependency graph
2.62/1.08	
2.62/1.08	  1: perfectp^#(s(x)) -> c_1(f^#(x, s(0()), s(x), s(x)))
2.62/1.08	     -->_1 f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) :3
2.62/1.08	  
2.62/1.08	  2: f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	     -->_1 f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) :3
2.62/1.08	     -->_1 f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u)) :2
2.62/1.08	  
2.62/1.08	  3: f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u))
2.62/1.08	     -->_1 f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) :3
2.62/1.08	     -->_1 f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u)) :2
2.62/1.08	  
2.62/1.08	
2.62/1.08	Following roots of the dependency graph are removed, as the
2.62/1.08	considered set of starting terms is closed under reduction with
2.62/1.08	respect to these rules (modulo compound contexts).
2.62/1.08	
2.62/1.08	  { perfectp^#(s(x)) -> c_1(f^#(x, s(0()), s(x), s(x))) }
2.62/1.08	
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(n^1)).
2.62/1.08	
2.62/1.08	Strict DPs:
2.62/1.08	  { f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(n^1))
2.62/1.08	
2.62/1.08	We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
2.62/1.08	to orient following rules strictly.
2.62/1.08	
2.62/1.08	DPs:
2.62/1.08	  { 1: f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , 2: f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) }
2.62/1.08	
2.62/1.08	Sub-proof:
2.62/1.08	----------
2.62/1.08	  The input was oriented with the instance of 'Small Polynomial Path
2.62/1.08	  Order (PS,1-bounded)' as induced by the safe mapping
2.62/1.08	  
2.62/1.08	   safe(0) = {}, safe(s) = {1}, safe(minus) = {1, 2},
2.62/1.08	   safe(f^#) = {2, 3, 4}, safe(c_2) = {}, safe(c_3) = {}
2.62/1.08	  
2.62/1.08	  and precedence
2.62/1.08	  
2.62/1.08	   empty .
2.62/1.08	  
2.62/1.08	  Following symbols are considered recursive:
2.62/1.08	  
2.62/1.08	   {f^#}
2.62/1.08	  
2.62/1.08	  The recursion depth is 1.
2.62/1.08	  
2.62/1.08	  Further, following argument filtering is employed:
2.62/1.08	  
2.62/1.08	   pi(0) = [], pi(s) = [1], pi(minus) = [], pi(f^#) = [1],
2.62/1.08	   pi(c_2) = [1], pi(c_3) = [1]
2.62/1.08	  
2.62/1.08	  Usable defined function symbols are a subset of:
2.62/1.08	  
2.62/1.08	   {f^#}
2.62/1.08	  
2.62/1.08	  For your convenience, here are the satisfied ordering constraints:
2.62/1.08	  
2.62/1.08	     pi(f^#(s(x), 0(), z, u)) = f^#(s(; x);)                         
2.62/1.08	                              > c_2(f^#(x;);)                        
2.62/1.08	                              = pi(c_2(f^#(x, u, minus(z, s(x)), u)))
2.62/1.08	                                                                     
2.62/1.08	    pi(f^#(s(x), s(y), z, u)) = f^#(s(; x);)                         
2.62/1.08	                              > c_3(f^#(x;);)                        
2.62/1.08	                              = pi(c_3(f^#(x, u, z, u)))             
2.62/1.08	                                                                     
2.62/1.08	
2.62/1.08	The strictly oriented rules are moved into the weak component.
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(1)).
2.62/1.08	
2.62/1.08	Weak DPs:
2.62/1.08	  { f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	  , f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) }
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(1))
2.62/1.08	
2.62/1.08	The following weak DPs constitute a sub-graph of the DG that is
2.62/1.08	closed under successors. The DPs are removed.
2.62/1.08	
2.62/1.08	{ f^#(s(x), 0(), z, u) -> c_2(f^#(x, u, minus(z, s(x)), u))
2.62/1.08	, f^#(s(x), s(y), z, u) -> c_3(f^#(x, u, z, u)) }
2.62/1.08	
2.62/1.08	We are left with following problem, upon which TcT provides the
2.62/1.08	certificate YES(O(1),O(1)).
2.62/1.08	
2.62/1.08	Rules: Empty
2.62/1.08	Obligation:
2.62/1.08	  innermost runtime complexity
2.62/1.08	Answer:
2.62/1.08	  YES(O(1),O(1))
2.62/1.08	
2.62/1.08	Empty rules are trivially bounded
2.62/1.08	
2.62/1.08	Hurray, we answered YES(O(1),O(n^1))
2.62/1.08	EOF