MAYBE
217.15/121.34	MAYBE
217.15/121.34	
217.15/121.34	We are left with following problem, upon which TcT provides the
217.15/121.34	certificate MAYBE.
217.15/121.34	
217.15/121.34	Strict Trs:
217.15/121.34	  { half(0()) -> 0()
217.15/121.34	  , half(s(0())) -> 0()
217.15/121.34	  , half(s(s(x))) -> s(half(x))
217.15/121.34	  , inc(0()) -> 0()
217.15/121.34	  , inc(s(x)) -> s(inc(x))
217.15/121.34	  , zero(0()) -> true()
217.15/121.34	  , zero(s(x)) -> false()
217.15/121.34	  , p(0()) -> 0()
217.15/121.34	  , p(s(x)) -> x
217.15/121.34	  , bits(x) -> bitIter(x, 0())
217.15/121.34	  , bitIter(x, y) -> if(zero(x), x, inc(y))
217.15/121.34	  , if(true(), x, y) -> p(y)
217.15/121.34	  , if(false(), x, y) -> bitIter(half(x), y) }
217.15/121.34	Obligation:
217.15/121.34	  runtime complexity
217.15/121.34	Answer:
217.15/121.34	  MAYBE
217.15/121.34	
217.15/121.34	None of the processors succeeded.
217.15/121.34	
217.15/121.34	Details of failed attempt(s):
217.15/121.34	-----------------------------
217.15/121.34	1) 'Best' failed due to the following reason:
217.15/121.34	   
217.15/121.34	   None of the processors succeeded.
217.15/121.34	   
217.15/121.34	   Details of failed attempt(s):
217.15/121.34	   -----------------------------
217.15/121.34	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
217.15/121.34	      seconds)' failed due to the following reason:
217.15/121.34	      
217.15/121.34	      None of the processors succeeded.
217.15/121.34	      
217.15/121.34	      Details of failed attempt(s):
217.15/121.34	      -----------------------------
217.15/121.34	      1) 'empty' failed due to the following reason:
217.15/121.34	         
217.15/121.34	         Empty strict component of the problem is NOT empty.
217.15/121.34	      
217.15/121.34	      2) 'With Problem ...' failed due to the following reason:
217.15/121.34	         
217.15/121.34	         None of the processors succeeded.
217.15/121.34	         
217.15/121.34	         Details of failed attempt(s):
217.15/121.34	         -----------------------------
217.15/121.34	         1) 'empty' failed due to the following reason:
217.15/121.34	            
217.15/121.34	            Empty strict component of the problem is NOT empty.
217.15/121.34	         
217.15/121.34	         2) 'Fastest' failed due to the following reason:
217.15/121.34	            
217.15/121.34	            None of the processors succeeded.
217.15/121.34	            
217.15/121.34	            Details of failed attempt(s):
217.15/121.34	            -----------------------------
217.15/121.34	            1) 'With Problem ...' failed due to the following reason:
217.15/121.34	               
217.15/121.34	               None of the processors succeeded.
217.15/121.34	               
217.15/121.34	               Details of failed attempt(s):
217.15/121.34	               -----------------------------
217.15/121.34	               1) 'empty' failed due to the following reason:
217.15/121.34	                  
217.15/121.34	                  Empty strict component of the problem is NOT empty.
217.15/121.34	               
217.15/121.34	               2) 'With Problem ...' failed due to the following reason:
217.15/121.34	                  
217.15/121.34	                  None of the processors succeeded.
217.15/121.34	                  
217.15/121.34	                  Details of failed attempt(s):
217.15/121.34	                  -----------------------------
217.15/121.34	                  1) 'empty' failed due to the following reason:
217.15/121.34	                     
217.15/121.34	                     Empty strict component of the problem is NOT empty.
217.15/121.34	                  
217.15/121.34	                  2) 'With Problem ...' failed due to the following reason:
217.15/121.34	                     
217.15/121.34	                     None of the processors succeeded.
217.15/121.34	                     
217.15/121.34	                     Details of failed attempt(s):
217.15/121.34	                     -----------------------------
217.15/121.34	                     1) 'empty' failed due to the following reason:
217.15/121.34	                        
217.15/121.34	                        Empty strict component of the problem is NOT empty.
217.15/121.34	                     
217.15/121.34	                     2) 'With Problem ...' failed due to the following reason:
217.15/121.34	                        
217.15/121.34	                        Empty strict component of the problem is NOT empty.
217.15/121.34	                     
217.15/121.34	                  
217.15/121.34	               
217.15/121.34	            
217.15/121.34	            2) 'With Problem ...' failed due to the following reason:
217.15/121.34	               
217.15/121.34	               None of the processors succeeded.
217.15/121.34	               
217.15/121.34	               Details of failed attempt(s):
217.15/121.34	               -----------------------------
217.15/121.34	               1) 'empty' failed due to the following reason:
217.15/121.34	                  
217.15/121.34	                  Empty strict component of the problem is NOT empty.
217.15/121.34	               
217.15/121.34	               2) 'With Problem ...' failed due to the following reason:
217.15/121.34	                  
217.15/121.34	                  Empty strict component of the problem is NOT empty.
217.15/121.34	               
217.15/121.34	            
217.15/121.34	         
217.15/121.34	      
217.15/121.34	   
217.15/121.34	   2) 'Best' failed due to the following reason:
217.15/121.34	      
217.15/121.34	      None of the processors succeeded.
217.15/121.34	      
217.15/121.34	      Details of failed attempt(s):
217.15/121.34	      -----------------------------
217.15/121.34	      1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
217.15/121.34	         to the following reason:
217.15/121.34	         
217.15/121.34	         The processor is inapplicable, reason:
217.15/121.34	           Processor only applicable for innermost runtime complexity analysis
217.15/121.34	      
217.15/121.34	      2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
217.15/121.34	         following reason:
217.15/121.34	         
217.15/121.34	         The processor is inapplicable, reason:
217.15/121.34	           Processor only applicable for innermost runtime complexity analysis
217.15/121.34	      
217.15/121.34	   
217.15/121.34	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
217.15/121.34	      failed due to the following reason:
217.15/121.34	      
217.15/121.34	      None of the processors succeeded.
217.15/121.34	      
217.15/121.34	      Details of failed attempt(s):
217.15/121.34	      -----------------------------
217.15/121.34	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
217.15/121.34	         failed due to the following reason:
217.15/121.34	         
217.15/121.34	         match-boundness of the problem could not be verified.
217.15/121.34	      
217.15/121.34	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
217.15/121.34	         failed due to the following reason:
217.15/121.34	         
217.15/121.34	         match-boundness of the problem could not be verified.
217.15/121.34	      
217.15/121.34	   
217.15/121.34	
217.15/121.34	2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
217.15/121.34	   the following reason:
217.15/121.34	   
217.15/121.34	   We add the following weak dependency pairs:
217.15/121.34	   
217.15/121.34	   Strict DPs:
217.15/121.34	     { half^#(0()) -> c_1()
217.15/121.34	     , half^#(s(0())) -> c_2()
217.15/121.34	     , half^#(s(s(x))) -> c_3(half^#(x))
217.15/121.34	     , inc^#(0()) -> c_4()
217.15/121.34	     , inc^#(s(x)) -> c_5(inc^#(x))
217.15/121.34	     , zero^#(0()) -> c_6()
217.15/121.34	     , zero^#(s(x)) -> c_7()
217.15/121.34	     , p^#(0()) -> c_8()
217.15/121.34	     , p^#(s(x)) -> c_9(x)
217.15/121.34	     , bits^#(x) -> c_10(bitIter^#(x, 0()))
217.15/121.34	     , bitIter^#(x, y) -> c_11(if^#(zero(x), x, inc(y)))
217.15/121.34	     , if^#(true(), x, y) -> c_12(p^#(y))
217.15/121.34	     , if^#(false(), x, y) -> c_13(bitIter^#(half(x), y)) }
217.15/121.34	   
217.15/121.34	   and mark the set of starting terms.
217.15/121.34	   
217.15/121.34	   We are left with following problem, upon which TcT provides the
217.15/121.34	   certificate MAYBE.
217.15/121.34	   
217.15/121.34	   Strict DPs:
217.15/121.34	     { half^#(0()) -> c_1()
217.15/121.34	     , half^#(s(0())) -> c_2()
217.15/121.34	     , half^#(s(s(x))) -> c_3(half^#(x))
217.15/121.34	     , inc^#(0()) -> c_4()
217.15/121.34	     , inc^#(s(x)) -> c_5(inc^#(x))
217.15/121.34	     , zero^#(0()) -> c_6()
217.15/121.34	     , zero^#(s(x)) -> c_7()
217.15/121.34	     , p^#(0()) -> c_8()
217.15/121.34	     , p^#(s(x)) -> c_9(x)
217.15/121.34	     , bits^#(x) -> c_10(bitIter^#(x, 0()))
217.15/121.34	     , bitIter^#(x, y) -> c_11(if^#(zero(x), x, inc(y)))
217.15/121.34	     , if^#(true(), x, y) -> c_12(p^#(y))
217.15/121.34	     , if^#(false(), x, y) -> c_13(bitIter^#(half(x), y)) }
217.15/121.34	   Strict Trs:
217.15/121.34	     { half(0()) -> 0()
217.15/121.34	     , half(s(0())) -> 0()
217.15/121.34	     , half(s(s(x))) -> s(half(x))
217.15/121.34	     , inc(0()) -> 0()
217.15/121.34	     , inc(s(x)) -> s(inc(x))
217.15/121.34	     , zero(0()) -> true()
217.15/121.34	     , zero(s(x)) -> false()
217.15/121.34	     , p(0()) -> 0()
217.15/121.34	     , p(s(x)) -> x
217.15/121.34	     , bits(x) -> bitIter(x, 0())
217.15/121.34	     , bitIter(x, y) -> if(zero(x), x, inc(y))
217.15/121.34	     , if(true(), x, y) -> p(y)
217.15/121.34	     , if(false(), x, y) -> bitIter(half(x), y) }
217.15/121.34	   Obligation:
217.15/121.34	     runtime complexity
217.15/121.34	   Answer:
217.15/121.34	     MAYBE
217.15/121.34	   
217.15/121.34	   We estimate the number of application of {1,2,4,6,7,8} by
217.15/121.34	   applications of Pre({1,2,4,6,7,8}) = {3,5,9,12}. Here rules are
217.15/121.34	   labeled as follows:
217.15/121.34	   
217.15/121.34	     DPs:
217.15/121.34	       { 1: half^#(0()) -> c_1()
217.15/121.34	       , 2: half^#(s(0())) -> c_2()
217.15/121.34	       , 3: half^#(s(s(x))) -> c_3(half^#(x))
217.15/121.34	       , 4: inc^#(0()) -> c_4()
217.15/121.34	       , 5: inc^#(s(x)) -> c_5(inc^#(x))
217.15/121.34	       , 6: zero^#(0()) -> c_6()
217.15/121.34	       , 7: zero^#(s(x)) -> c_7()
217.15/121.34	       , 8: p^#(0()) -> c_8()
217.15/121.34	       , 9: p^#(s(x)) -> c_9(x)
217.15/121.34	       , 10: bits^#(x) -> c_10(bitIter^#(x, 0()))
217.15/121.34	       , 11: bitIter^#(x, y) -> c_11(if^#(zero(x), x, inc(y)))
217.15/121.34	       , 12: if^#(true(), x, y) -> c_12(p^#(y))
217.15/121.34	       , 13: if^#(false(), x, y) -> c_13(bitIter^#(half(x), y)) }
217.15/121.34	   
217.15/121.34	   We are left with following problem, upon which TcT provides the
217.15/121.34	   certificate MAYBE.
217.15/121.34	   
217.15/121.34	   Strict DPs:
217.15/121.34	     { half^#(s(s(x))) -> c_3(half^#(x))
217.15/121.34	     , inc^#(s(x)) -> c_5(inc^#(x))
217.15/121.34	     , p^#(s(x)) -> c_9(x)
217.15/121.34	     , bits^#(x) -> c_10(bitIter^#(x, 0()))
217.15/121.34	     , bitIter^#(x, y) -> c_11(if^#(zero(x), x, inc(y)))
217.15/121.34	     , if^#(true(), x, y) -> c_12(p^#(y))
217.15/121.34	     , if^#(false(), x, y) -> c_13(bitIter^#(half(x), y)) }
217.15/121.34	   Strict Trs:
217.15/121.34	     { half(0()) -> 0()
217.15/121.34	     , half(s(0())) -> 0()
217.15/121.34	     , half(s(s(x))) -> s(half(x))
217.15/121.34	     , inc(0()) -> 0()
217.15/121.34	     , inc(s(x)) -> s(inc(x))
217.15/121.34	     , zero(0()) -> true()
217.15/121.34	     , zero(s(x)) -> false()
217.15/121.34	     , p(0()) -> 0()
217.15/121.34	     , p(s(x)) -> x
217.15/121.34	     , bits(x) -> bitIter(x, 0())
217.15/121.34	     , bitIter(x, y) -> if(zero(x), x, inc(y))
217.15/121.34	     , if(true(), x, y) -> p(y)
217.15/121.34	     , if(false(), x, y) -> bitIter(half(x), y) }
217.15/121.34	   Weak DPs:
217.15/121.34	     { half^#(0()) -> c_1()
217.15/121.34	     , half^#(s(0())) -> c_2()
217.15/121.34	     , inc^#(0()) -> c_4()
217.15/121.34	     , zero^#(0()) -> c_6()
217.15/121.34	     , zero^#(s(x)) -> c_7()
217.15/121.34	     , p^#(0()) -> c_8() }
217.15/121.34	   Obligation:
217.15/121.34	     runtime complexity
217.15/121.34	   Answer:
217.15/121.34	     MAYBE
217.15/121.34	   
217.15/121.34	   Empty strict component of the problem is NOT empty.
217.15/121.34	
217.15/121.34	
217.15/121.34	Arrrr..
217.38/121.50	EOF