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