MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { dbl(X) -> n__dbl(X) , dbl(0()) -> 0() , dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) , s(X) -> n__s(X) , activate(X) -> X , activate(n__s(X)) -> s(X) , activate(n__dbl(X)) -> dbl(X) , activate(n__dbls(X)) -> dbls(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__indx(X1, X2)) -> indx(X1, X2) , activate(n__from(X)) -> from(X) , dbls(X) -> n__dbls(X) , dbls(nil()) -> nil() , dbls(cons(X, Y)) -> cons(n__dbl(activate(X)), n__dbls(activate(Y))) , sel(X1, X2) -> n__sel(X1, X2) , sel(0(), cons(X, Y)) -> activate(X) , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)) , indx(X1, X2) -> n__indx(X1, X2) , indx(nil(), X) -> nil() , indx(cons(X, Y), Z) -> cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z))) , from(X) -> cons(activate(X), n__from(n__s(activate(X)))) , from(X) -> n__from(X) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) '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: Computation stopped due to timeout after 30.0 seconds. 2) '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 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. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { dbl^#(X) -> c_1(X) , dbl^#(0()) -> c_2() , dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X))))) , s^#(X) -> c_4(X) , activate^#(X) -> c_5(X) , activate^#(n__s(X)) -> c_6(s^#(X)) , activate^#(n__dbl(X)) -> c_7(dbl^#(X)) , activate^#(n__dbls(X)) -> c_8(dbls^#(X)) , activate^#(n__sel(X1, X2)) -> c_9(sel^#(X1, X2)) , activate^#(n__indx(X1, X2)) -> c_10(indx^#(X1, X2)) , activate^#(n__from(X)) -> c_11(from^#(X)) , dbls^#(X) -> c_12(X) , dbls^#(nil()) -> c_13() , dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y)) , sel^#(X1, X2) -> c_15(X1, X2) , sel^#(0(), cons(X, Y)) -> c_16(activate^#(X)) , sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z))) , indx^#(X1, X2) -> c_18(X1, X2) , indx^#(nil(), X) -> c_19() , indx^#(cons(X, Y), Z) -> c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z)) , from^#(X) -> c_21(activate^#(X), activate^#(X)) , from^#(X) -> c_22(X) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { dbl^#(X) -> c_1(X) , dbl^#(0()) -> c_2() , dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X))))) , s^#(X) -> c_4(X) , activate^#(X) -> c_5(X) , activate^#(n__s(X)) -> c_6(s^#(X)) , activate^#(n__dbl(X)) -> c_7(dbl^#(X)) , activate^#(n__dbls(X)) -> c_8(dbls^#(X)) , activate^#(n__sel(X1, X2)) -> c_9(sel^#(X1, X2)) , activate^#(n__indx(X1, X2)) -> c_10(indx^#(X1, X2)) , activate^#(n__from(X)) -> c_11(from^#(X)) , dbls^#(X) -> c_12(X) , dbls^#(nil()) -> c_13() , dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y)) , sel^#(X1, X2) -> c_15(X1, X2) , sel^#(0(), cons(X, Y)) -> c_16(activate^#(X)) , sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z))) , indx^#(X1, X2) -> c_18(X1, X2) , indx^#(nil(), X) -> c_19() , indx^#(cons(X, Y), Z) -> c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z)) , from^#(X) -> c_21(activate^#(X), activate^#(X)) , from^#(X) -> c_22(X) } Strict Trs: { dbl(X) -> n__dbl(X) , dbl(0()) -> 0() , dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) , s(X) -> n__s(X) , activate(X) -> X , activate(n__s(X)) -> s(X) , activate(n__dbl(X)) -> dbl(X) , activate(n__dbls(X)) -> dbls(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__indx(X1, X2)) -> indx(X1, X2) , activate(n__from(X)) -> from(X) , dbls(X) -> n__dbls(X) , dbls(nil()) -> nil() , dbls(cons(X, Y)) -> cons(n__dbl(activate(X)), n__dbls(activate(Y))) , sel(X1, X2) -> n__sel(X1, X2) , sel(0(), cons(X, Y)) -> activate(X) , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)) , indx(X1, X2) -> n__indx(X1, X2) , indx(nil(), X) -> nil() , indx(cons(X, Y), Z) -> cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z))) , from(X) -> cons(activate(X), n__from(n__s(activate(X)))) , from(X) -> n__from(X) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,13,19} by applications of Pre({2,13,19}) = {1,4,5,7,8,10,12,15,18,22}. Here rules are labeled as follows: DPs: { 1: dbl^#(X) -> c_1(X) , 2: dbl^#(0()) -> c_2() , 3: dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X))))) , 4: s^#(X) -> c_4(X) , 5: activate^#(X) -> c_5(X) , 6: activate^#(n__s(X)) -> c_6(s^#(X)) , 7: activate^#(n__dbl(X)) -> c_7(dbl^#(X)) , 8: activate^#(n__dbls(X)) -> c_8(dbls^#(X)) , 9: activate^#(n__sel(X1, X2)) -> c_9(sel^#(X1, X2)) , 10: activate^#(n__indx(X1, X2)) -> c_10(indx^#(X1, X2)) , 11: activate^#(n__from(X)) -> c_11(from^#(X)) , 12: dbls^#(X) -> c_12(X) , 13: dbls^#(nil()) -> c_13() , 14: dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y)) , 15: sel^#(X1, X2) -> c_15(X1, X2) , 16: sel^#(0(), cons(X, Y)) -> c_16(activate^#(X)) , 17: sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z))) , 18: indx^#(X1, X2) -> c_18(X1, X2) , 19: indx^#(nil(), X) -> c_19() , 20: indx^#(cons(X, Y), Z) -> c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z)) , 21: from^#(X) -> c_21(activate^#(X), activate^#(X)) , 22: from^#(X) -> c_22(X) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { dbl^#(X) -> c_1(X) , dbl^#(s(X)) -> c_3(s^#(n__s(n__dbl(activate(X))))) , s^#(X) -> c_4(X) , activate^#(X) -> c_5(X) , activate^#(n__s(X)) -> c_6(s^#(X)) , activate^#(n__dbl(X)) -> c_7(dbl^#(X)) , activate^#(n__dbls(X)) -> c_8(dbls^#(X)) , activate^#(n__sel(X1, X2)) -> c_9(sel^#(X1, X2)) , activate^#(n__indx(X1, X2)) -> c_10(indx^#(X1, X2)) , activate^#(n__from(X)) -> c_11(from^#(X)) , dbls^#(X) -> c_12(X) , dbls^#(cons(X, Y)) -> c_14(activate^#(X), activate^#(Y)) , sel^#(X1, X2) -> c_15(X1, X2) , sel^#(0(), cons(X, Y)) -> c_16(activate^#(X)) , sel^#(s(X), cons(Y, Z)) -> c_17(sel^#(activate(X), activate(Z))) , indx^#(X1, X2) -> c_18(X1, X2) , indx^#(cons(X, Y), Z) -> c_20(activate^#(X), activate^#(Z), activate^#(Y), activate^#(Z)) , from^#(X) -> c_21(activate^#(X), activate^#(X)) , from^#(X) -> c_22(X) } Strict Trs: { dbl(X) -> n__dbl(X) , dbl(0()) -> 0() , dbl(s(X)) -> s(n__s(n__dbl(activate(X)))) , s(X) -> n__s(X) , activate(X) -> X , activate(n__s(X)) -> s(X) , activate(n__dbl(X)) -> dbl(X) , activate(n__dbls(X)) -> dbls(X) , activate(n__sel(X1, X2)) -> sel(X1, X2) , activate(n__indx(X1, X2)) -> indx(X1, X2) , activate(n__from(X)) -> from(X) , dbls(X) -> n__dbls(X) , dbls(nil()) -> nil() , dbls(cons(X, Y)) -> cons(n__dbl(activate(X)), n__dbls(activate(Y))) , sel(X1, X2) -> n__sel(X1, X2) , sel(0(), cons(X, Y)) -> activate(X) , sel(s(X), cons(Y, Z)) -> sel(activate(X), activate(Z)) , indx(X1, X2) -> n__indx(X1, X2) , indx(nil(), X) -> nil() , indx(cons(X, Y), Z) -> cons(n__sel(activate(X), activate(Z)), n__indx(activate(Y), activate(Z))) , from(X) -> cons(activate(X), n__from(n__s(activate(X)))) , from(X) -> n__from(X) } Weak DPs: { dbl^#(0()) -> c_2() , dbls^#(nil()) -> c_13() , indx^#(nil(), X) -> c_19() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..