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)) , lastbit(0()) -> 0() , lastbit(s(0())) -> s(0()) , lastbit(s(s(x))) -> lastbit(x) , zero(0()) -> true() , zero(s(x)) -> false() , conv(x) -> conviter(x, cons(0(), nil())) , conviter(x, l) -> if(zero(x), x, l) , if(true(), x, l) -> l , if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l)) } 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) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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) '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 3) '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. 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)) , lastbit^#(0()) -> c_4() , lastbit^#(s(0())) -> c_5() , lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) , zero^#(0()) -> c_7() , zero^#(s(x)) -> c_8() , conv^#(x) -> c_9(conviter^#(x, cons(0(), nil()))) , conviter^#(x, l) -> c_10(if^#(zero(x), x, l)) , if^#(true(), x, l) -> c_11(l) , if^#(false(), x, l) -> c_12(conviter^#(half(x), cons(lastbit(x), l))) } 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)) , lastbit^#(0()) -> c_4() , lastbit^#(s(0())) -> c_5() , lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) , zero^#(0()) -> c_7() , zero^#(s(x)) -> c_8() , conv^#(x) -> c_9(conviter^#(x, cons(0(), nil()))) , conviter^#(x, l) -> c_10(if^#(zero(x), x, l)) , if^#(true(), x, l) -> c_11(l) , if^#(false(), x, l) -> c_12(conviter^#(half(x), cons(lastbit(x), l))) } Strict Trs: { half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , lastbit(0()) -> 0() , lastbit(s(0())) -> s(0()) , lastbit(s(s(x))) -> lastbit(x) , zero(0()) -> true() , zero(s(x)) -> false() , conv(x) -> conviter(x, cons(0(), nil())) , conviter(x, l) -> if(zero(x), x, l) , if(true(), x, l) -> l , if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,5,7,8} by applications of Pre({1,2,4,5,7,8}) = {3,6,11}. 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: lastbit^#(0()) -> c_4() , 5: lastbit^#(s(0())) -> c_5() , 6: lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) , 7: zero^#(0()) -> c_7() , 8: zero^#(s(x)) -> c_8() , 9: conv^#(x) -> c_9(conviter^#(x, cons(0(), nil()))) , 10: conviter^#(x, l) -> c_10(if^#(zero(x), x, l)) , 11: if^#(true(), x, l) -> c_11(l) , 12: if^#(false(), x, l) -> c_12(conviter^#(half(x), cons(lastbit(x), l))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { half^#(s(s(x))) -> c_3(half^#(x)) , lastbit^#(s(s(x))) -> c_6(lastbit^#(x)) , conv^#(x) -> c_9(conviter^#(x, cons(0(), nil()))) , conviter^#(x, l) -> c_10(if^#(zero(x), x, l)) , if^#(true(), x, l) -> c_11(l) , if^#(false(), x, l) -> c_12(conviter^#(half(x), cons(lastbit(x), l))) } Strict Trs: { half(0()) -> 0() , half(s(0())) -> 0() , half(s(s(x))) -> s(half(x)) , lastbit(0()) -> 0() , lastbit(s(0())) -> s(0()) , lastbit(s(s(x))) -> lastbit(x) , zero(0()) -> true() , zero(s(x)) -> false() , conv(x) -> conviter(x, cons(0(), nil())) , conviter(x, l) -> if(zero(x), x, l) , if(true(), x, l) -> l , if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l)) } Weak DPs: { half^#(0()) -> c_1() , half^#(s(0())) -> c_2() , lastbit^#(0()) -> c_4() , lastbit^#(s(0())) -> c_5() , zero^#(0()) -> c_7() , zero^#(s(x)) -> c_8() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..