MAYBE 1181.66/297.25 MAYBE 1181.66/297.25 1181.66/297.25 We are left with following problem, upon which TcT provides the 1181.66/297.25 certificate MAYBE. 1181.66/297.25 1181.66/297.25 Strict Trs: 1181.66/297.25 { a__dbl(X) -> dbl(X) 1181.66/297.25 , a__dbl(0()) -> 0() 1181.66/297.25 , a__dbl(s(X)) -> s(s(dbl(X))) 1181.66/297.25 , a__dbls(X) -> dbls(X) 1181.66/297.25 , a__dbls(nil()) -> nil() 1181.66/297.25 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1181.66/297.25 , a__sel(X1, X2) -> sel(X1, X2) 1181.66/297.25 , a__sel(0(), cons(X, Y)) -> mark(X) 1181.66/297.25 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1181.66/297.25 , mark(0()) -> 0() 1181.66/297.25 , mark(s(X)) -> s(X) 1181.66/297.25 , mark(dbl(X)) -> a__dbl(mark(X)) 1181.66/297.25 , mark(nil()) -> nil() 1181.66/297.25 , mark(cons(X1, X2)) -> cons(X1, X2) 1181.66/297.25 , mark(dbls(X)) -> a__dbls(mark(X)) 1181.66/297.25 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1181.66/297.25 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1181.66/297.25 , mark(from(X)) -> a__from(X) 1181.66/297.25 , mark(01()) -> 01() 1181.66/297.25 , mark(s1(X)) -> s1(mark(X)) 1181.66/297.25 , mark(dbl1(X)) -> a__dbl1(mark(X)) 1181.66/297.25 , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2)) 1181.66/297.25 , mark(quote(X)) -> a__quote(mark(X)) 1181.66/297.25 , a__indx(X1, X2) -> indx(X1, X2) 1181.66/297.25 , a__indx(nil(), X) -> nil() 1181.66/297.25 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1181.66/297.25 , a__from(X) -> cons(X, from(s(X))) 1181.66/297.25 , a__from(X) -> from(X) 1181.66/297.25 , a__dbl1(X) -> dbl1(X) 1181.66/297.25 , a__dbl1(0()) -> 01() 1181.66/297.25 , a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X)))) 1181.66/297.25 , a__sel1(X1, X2) -> sel1(X1, X2) 1181.66/297.25 , a__sel1(0(), cons(X, Y)) -> mark(X) 1181.66/297.25 , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z)) 1181.66/297.25 , a__quote(X) -> quote(X) 1181.66/297.25 , a__quote(0()) -> 01() 1181.66/297.25 , a__quote(s(X)) -> s1(a__quote(mark(X))) 1181.66/297.25 , a__quote(dbl(X)) -> a__dbl1(mark(X)) 1181.66/297.25 , a__quote(sel(X, Y)) -> a__sel1(mark(X), mark(Y)) } 1181.66/297.25 Obligation: 1181.66/297.25 runtime complexity 1181.66/297.25 Answer: 1181.66/297.25 MAYBE 1181.66/297.25 1181.66/297.25 None of the processors succeeded. 1181.66/297.25 1181.66/297.25 Details of failed attempt(s): 1181.66/297.25 ----------------------------- 1181.66/297.25 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1181.66/297.25 following reason: 1181.66/297.25 1181.66/297.25 Computation stopped due to timeout after 297.0 seconds. 1181.66/297.25 1181.66/297.25 2) 'Best' failed due to the following reason: 1181.66/297.25 1181.66/297.25 None of the processors succeeded. 1181.66/297.25 1181.66/297.25 Details of failed attempt(s): 1181.66/297.25 ----------------------------- 1181.66/297.25 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1181.66/297.25 seconds)' failed due to the following reason: 1181.66/297.25 1181.66/297.25 Computation stopped due to timeout after 148.0 seconds. 1181.66/297.25 1181.66/297.25 2) 'Best' failed due to the following reason: 1181.66/297.25 1181.66/297.25 None of the processors succeeded. 1181.66/297.25 1181.66/297.25 Details of failed attempt(s): 1181.66/297.25 ----------------------------- 1181.66/297.25 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1181.66/297.25 following reason: 1181.66/297.25 1181.66/297.25 The processor is inapplicable, reason: 1181.66/297.25 Processor only applicable for innermost runtime complexity analysis 1181.66/297.25 1181.66/297.25 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1181.66/297.25 to the following reason: 1181.66/297.25 1181.66/297.25 The processor is inapplicable, reason: 1181.66/297.25 Processor only applicable for innermost runtime complexity analysis 1181.66/297.25 1181.66/297.25 1181.66/297.25 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1181.66/297.25 failed due to the following reason: 1181.66/297.25 1181.66/297.25 None of the processors succeeded. 1181.66/297.25 1181.66/297.25 Details of failed attempt(s): 1181.66/297.25 ----------------------------- 1181.66/297.25 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1181.66/297.25 failed due to the following reason: 1181.66/297.25 1181.66/297.25 match-boundness of the problem could not be verified. 1181.66/297.25 1181.66/297.25 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1181.66/297.25 failed due to the following reason: 1181.66/297.25 1181.66/297.25 match-boundness of the problem could not be verified. 1181.66/297.25 1181.66/297.25 1181.66/297.25 1181.66/297.25 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1181.66/297.25 the following reason: 1181.66/297.25 1181.66/297.25 We add the following weak dependency pairs: 1181.66/297.25 1181.66/297.25 Strict DPs: 1181.66/297.25 { a__dbl^#(X) -> c_1(X) 1181.66/297.25 , a__dbl^#(0()) -> c_2() 1181.66/297.25 , a__dbl^#(s(X)) -> c_3(X) 1181.66/297.25 , a__dbls^#(X) -> c_4(X) 1181.66/297.25 , a__dbls^#(nil()) -> c_5() 1181.66/297.25 , a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1181.66/297.25 , a__sel^#(X1, X2) -> c_7(X1, X2) 1181.66/297.25 , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1181.66/297.25 , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1181.66/297.25 , mark^#(0()) -> c_10() 1181.66/297.25 , mark^#(s(X)) -> c_11(X) 1181.66/297.25 , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1181.66/297.25 , mark^#(nil()) -> c_13() 1181.66/297.25 , mark^#(cons(X1, X2)) -> c_14(X1, X2) 1181.66/297.25 , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1181.66/297.25 , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1181.66/297.25 , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1181.66/297.25 , mark^#(from(X)) -> c_18(a__from^#(X)) 1181.66/297.25 , mark^#(01()) -> c_19() 1181.66/297.25 , mark^#(s1(X)) -> c_20(mark^#(X)) 1181.66/297.25 , mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X))) 1181.66/297.25 , mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2))) 1181.66/297.25 , mark^#(quote(X)) -> c_23(a__quote^#(mark(X))) 1181.66/297.25 , a__indx^#(X1, X2) -> c_24(X1, X2) 1181.66/297.25 , a__indx^#(nil(), X) -> c_25() 1181.66/297.25 , a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z) 1181.66/297.25 , a__from^#(X) -> c_27(X, X) 1181.66/297.25 , a__from^#(X) -> c_28(X) 1181.66/297.25 , a__dbl1^#(X) -> c_29(X) 1181.66/297.25 , a__dbl1^#(0()) -> c_30() 1181.66/297.25 , a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X))) 1181.66/297.25 , a__sel1^#(X1, X2) -> c_32(X1, X2) 1181.66/297.25 , a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X)) 1181.66/297.25 , a__sel1^#(s(X), cons(Y, Z)) -> c_34(a__sel1^#(mark(X), mark(Z))) 1181.66/297.25 , a__quote^#(X) -> c_35(X) 1181.66/297.25 , a__quote^#(0()) -> c_36() 1181.66/297.25 , a__quote^#(s(X)) -> c_37(a__quote^#(mark(X))) 1181.66/297.25 , a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X))) 1181.66/297.25 , a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) } 1181.66/297.25 1181.66/297.25 and mark the set of starting terms. 1181.66/297.25 1181.66/297.25 We are left with following problem, upon which TcT provides the 1181.66/297.25 certificate MAYBE. 1181.66/297.25 1181.66/297.25 Strict DPs: 1181.66/297.25 { a__dbl^#(X) -> c_1(X) 1181.66/297.25 , a__dbl^#(0()) -> c_2() 1181.66/297.25 , a__dbl^#(s(X)) -> c_3(X) 1181.66/297.25 , a__dbls^#(X) -> c_4(X) 1181.66/297.25 , a__dbls^#(nil()) -> c_5() 1181.66/297.25 , a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1181.66/297.25 , a__sel^#(X1, X2) -> c_7(X1, X2) 1181.66/297.25 , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1181.66/297.25 , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1181.66/297.25 , mark^#(0()) -> c_10() 1181.66/297.25 , mark^#(s(X)) -> c_11(X) 1181.66/297.25 , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1181.66/297.25 , mark^#(nil()) -> c_13() 1181.66/297.25 , mark^#(cons(X1, X2)) -> c_14(X1, X2) 1181.66/297.25 , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1181.66/297.25 , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1181.66/297.25 , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1181.66/297.25 , mark^#(from(X)) -> c_18(a__from^#(X)) 1181.66/297.25 , mark^#(01()) -> c_19() 1181.66/297.25 , mark^#(s1(X)) -> c_20(mark^#(X)) 1181.66/297.25 , mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X))) 1181.66/297.25 , mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2))) 1181.66/297.25 , mark^#(quote(X)) -> c_23(a__quote^#(mark(X))) 1181.66/297.25 , a__indx^#(X1, X2) -> c_24(X1, X2) 1181.66/297.25 , a__indx^#(nil(), X) -> c_25() 1181.66/297.25 , a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z) 1181.66/297.25 , a__from^#(X) -> c_27(X, X) 1181.66/297.25 , a__from^#(X) -> c_28(X) 1181.66/297.25 , a__dbl1^#(X) -> c_29(X) 1181.66/297.25 , a__dbl1^#(0()) -> c_30() 1181.66/297.25 , a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X))) 1181.66/297.25 , a__sel1^#(X1, X2) -> c_32(X1, X2) 1181.66/297.25 , a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X)) 1181.66/297.25 , a__sel1^#(s(X), cons(Y, Z)) -> c_34(a__sel1^#(mark(X), mark(Z))) 1181.66/297.25 , a__quote^#(X) -> c_35(X) 1181.66/297.25 , a__quote^#(0()) -> c_36() 1181.66/297.25 , a__quote^#(s(X)) -> c_37(a__quote^#(mark(X))) 1181.66/297.25 , a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X))) 1181.66/297.25 , a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) } 1181.66/297.25 Strict Trs: 1181.66/297.25 { a__dbl(X) -> dbl(X) 1181.66/297.25 , a__dbl(0()) -> 0() 1181.66/297.25 , a__dbl(s(X)) -> s(s(dbl(X))) 1181.66/297.25 , a__dbls(X) -> dbls(X) 1181.66/297.25 , a__dbls(nil()) -> nil() 1181.66/297.25 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1181.66/297.25 , a__sel(X1, X2) -> sel(X1, X2) 1181.66/297.25 , a__sel(0(), cons(X, Y)) -> mark(X) 1181.66/297.25 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1181.66/297.25 , mark(0()) -> 0() 1181.66/297.25 , mark(s(X)) -> s(X) 1181.66/297.25 , mark(dbl(X)) -> a__dbl(mark(X)) 1181.66/297.25 , mark(nil()) -> nil() 1181.66/297.25 , mark(cons(X1, X2)) -> cons(X1, X2) 1181.66/297.25 , mark(dbls(X)) -> a__dbls(mark(X)) 1181.66/297.25 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1181.66/297.25 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1181.66/297.25 , mark(from(X)) -> a__from(X) 1181.66/297.25 , mark(01()) -> 01() 1181.66/297.25 , mark(s1(X)) -> s1(mark(X)) 1181.66/297.25 , mark(dbl1(X)) -> a__dbl1(mark(X)) 1181.66/297.25 , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2)) 1181.66/297.25 , mark(quote(X)) -> a__quote(mark(X)) 1181.66/297.29 , a__indx(X1, X2) -> indx(X1, X2) 1181.66/297.29 , a__indx(nil(), X) -> nil() 1181.66/297.29 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1181.66/297.29 , a__from(X) -> cons(X, from(s(X))) 1181.66/297.29 , a__from(X) -> from(X) 1181.66/297.29 , a__dbl1(X) -> dbl1(X) 1181.66/297.29 , a__dbl1(0()) -> 01() 1181.66/297.29 , a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X)))) 1181.66/297.29 , a__sel1(X1, X2) -> sel1(X1, X2) 1181.66/297.29 , a__sel1(0(), cons(X, Y)) -> mark(X) 1181.66/297.29 , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z)) 1181.66/297.29 , a__quote(X) -> quote(X) 1181.66/297.29 , a__quote(0()) -> 01() 1181.66/297.29 , a__quote(s(X)) -> s1(a__quote(mark(X))) 1181.66/297.29 , a__quote(dbl(X)) -> a__dbl1(mark(X)) 1181.66/297.29 , a__quote(sel(X, Y)) -> a__sel1(mark(X), mark(Y)) } 1181.66/297.29 Obligation: 1181.66/297.29 runtime complexity 1181.66/297.29 Answer: 1181.66/297.29 MAYBE 1181.66/297.29 1181.66/297.29 We estimate the number of application of {2,5,10,13,19,25,30,36} by 1181.66/297.29 applications of Pre({2,5,10,13,19,25,30,36}) = 1181.66/297.29 {1,3,4,6,7,8,11,12,14,15,17,20,21,23,24,26,27,28,29,31,32,33,35,37,38}. 1181.66/297.29 Here rules are labeled as follows: 1181.66/297.29 1181.66/297.29 DPs: 1181.66/297.29 { 1: a__dbl^#(X) -> c_1(X) 1181.66/297.29 , 2: a__dbl^#(0()) -> c_2() 1181.66/297.29 , 3: a__dbl^#(s(X)) -> c_3(X) 1181.66/297.29 , 4: a__dbls^#(X) -> c_4(X) 1181.66/297.29 , 5: a__dbls^#(nil()) -> c_5() 1181.66/297.29 , 6: a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1181.66/297.29 , 7: a__sel^#(X1, X2) -> c_7(X1, X2) 1181.66/297.29 , 8: a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1181.66/297.29 , 9: a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1181.66/297.29 , 10: mark^#(0()) -> c_10() 1181.66/297.29 , 11: mark^#(s(X)) -> c_11(X) 1181.66/297.29 , 12: mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1181.66/297.29 , 13: mark^#(nil()) -> c_13() 1181.66/297.29 , 14: mark^#(cons(X1, X2)) -> c_14(X1, X2) 1181.66/297.29 , 15: mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1181.66/297.29 , 16: mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1181.66/297.29 , 17: mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1181.66/297.29 , 18: mark^#(from(X)) -> c_18(a__from^#(X)) 1181.66/297.29 , 19: mark^#(01()) -> c_19() 1181.66/297.29 , 20: mark^#(s1(X)) -> c_20(mark^#(X)) 1181.66/297.29 , 21: mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X))) 1181.66/297.29 , 22: mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2))) 1181.66/297.29 , 23: mark^#(quote(X)) -> c_23(a__quote^#(mark(X))) 1181.66/297.29 , 24: a__indx^#(X1, X2) -> c_24(X1, X2) 1181.66/297.29 , 25: a__indx^#(nil(), X) -> c_25() 1181.66/297.29 , 26: a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z) 1181.66/297.29 , 27: a__from^#(X) -> c_27(X, X) 1181.66/297.29 , 28: a__from^#(X) -> c_28(X) 1181.66/297.29 , 29: a__dbl1^#(X) -> c_29(X) 1181.66/297.29 , 30: a__dbl1^#(0()) -> c_30() 1181.66/297.29 , 31: a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X))) 1181.66/297.29 , 32: a__sel1^#(X1, X2) -> c_32(X1, X2) 1181.66/297.29 , 33: a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X)) 1181.66/297.29 , 34: a__sel1^#(s(X), cons(Y, Z)) -> 1181.66/297.29 c_34(a__sel1^#(mark(X), mark(Z))) 1181.66/297.29 , 35: a__quote^#(X) -> c_35(X) 1181.66/297.29 , 36: a__quote^#(0()) -> c_36() 1181.66/297.29 , 37: a__quote^#(s(X)) -> c_37(a__quote^#(mark(X))) 1181.66/297.29 , 38: a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X))) 1181.66/297.29 , 39: a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) } 1181.66/297.29 1181.66/297.29 We are left with following problem, upon which TcT provides the 1181.66/297.29 certificate MAYBE. 1181.66/297.29 1181.66/297.29 Strict DPs: 1181.66/297.29 { a__dbl^#(X) -> c_1(X) 1181.66/297.29 , a__dbl^#(s(X)) -> c_3(X) 1181.66/297.29 , a__dbls^#(X) -> c_4(X) 1181.66/297.29 , a__dbls^#(cons(X, Y)) -> c_6(X, Y) 1181.66/297.29 , a__sel^#(X1, X2) -> c_7(X1, X2) 1181.66/297.29 , a__sel^#(0(), cons(X, Y)) -> c_8(mark^#(X)) 1181.66/297.29 , a__sel^#(s(X), cons(Y, Z)) -> c_9(a__sel^#(mark(X), mark(Z))) 1181.66/297.29 , mark^#(s(X)) -> c_11(X) 1181.66/297.29 , mark^#(dbl(X)) -> c_12(a__dbl^#(mark(X))) 1181.66/297.29 , mark^#(cons(X1, X2)) -> c_14(X1, X2) 1181.66/297.29 , mark^#(dbls(X)) -> c_15(a__dbls^#(mark(X))) 1181.66/297.29 , mark^#(sel(X1, X2)) -> c_16(a__sel^#(mark(X1), mark(X2))) 1181.66/297.29 , mark^#(indx(X1, X2)) -> c_17(a__indx^#(mark(X1), X2)) 1181.66/297.29 , mark^#(from(X)) -> c_18(a__from^#(X)) 1181.66/297.29 , mark^#(s1(X)) -> c_20(mark^#(X)) 1181.66/297.29 , mark^#(dbl1(X)) -> c_21(a__dbl1^#(mark(X))) 1181.66/297.29 , mark^#(sel1(X1, X2)) -> c_22(a__sel1^#(mark(X1), mark(X2))) 1181.66/297.29 , mark^#(quote(X)) -> c_23(a__quote^#(mark(X))) 1181.66/297.29 , a__indx^#(X1, X2) -> c_24(X1, X2) 1181.66/297.29 , a__indx^#(cons(X, Y), Z) -> c_26(X, Z, Y, Z) 1181.66/297.29 , a__from^#(X) -> c_27(X, X) 1181.66/297.29 , a__from^#(X) -> c_28(X) 1181.66/297.29 , a__dbl1^#(X) -> c_29(X) 1181.66/297.29 , a__dbl1^#(s(X)) -> c_31(a__dbl1^#(mark(X))) 1181.66/297.29 , a__sel1^#(X1, X2) -> c_32(X1, X2) 1181.66/297.29 , a__sel1^#(0(), cons(X, Y)) -> c_33(mark^#(X)) 1181.66/297.29 , a__sel1^#(s(X), cons(Y, Z)) -> c_34(a__sel1^#(mark(X), mark(Z))) 1181.66/297.29 , a__quote^#(X) -> c_35(X) 1181.66/297.29 , a__quote^#(s(X)) -> c_37(a__quote^#(mark(X))) 1181.66/297.29 , a__quote^#(dbl(X)) -> c_38(a__dbl1^#(mark(X))) 1181.66/297.29 , a__quote^#(sel(X, Y)) -> c_39(a__sel1^#(mark(X), mark(Y))) } 1181.66/297.29 Strict Trs: 1181.66/297.29 { a__dbl(X) -> dbl(X) 1181.66/297.29 , a__dbl(0()) -> 0() 1181.66/297.29 , a__dbl(s(X)) -> s(s(dbl(X))) 1181.66/297.29 , a__dbls(X) -> dbls(X) 1181.66/297.29 , a__dbls(nil()) -> nil() 1181.66/297.29 , a__dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y)) 1181.66/297.29 , a__sel(X1, X2) -> sel(X1, X2) 1181.66/297.29 , a__sel(0(), cons(X, Y)) -> mark(X) 1181.66/297.29 , a__sel(s(X), cons(Y, Z)) -> a__sel(mark(X), mark(Z)) 1181.66/297.29 , mark(0()) -> 0() 1181.66/297.29 , mark(s(X)) -> s(X) 1181.66/297.29 , mark(dbl(X)) -> a__dbl(mark(X)) 1181.66/297.29 , mark(nil()) -> nil() 1181.66/297.29 , mark(cons(X1, X2)) -> cons(X1, X2) 1181.66/297.29 , mark(dbls(X)) -> a__dbls(mark(X)) 1181.66/297.29 , mark(sel(X1, X2)) -> a__sel(mark(X1), mark(X2)) 1181.66/297.29 , mark(indx(X1, X2)) -> a__indx(mark(X1), X2) 1181.66/297.29 , mark(from(X)) -> a__from(X) 1181.66/297.29 , mark(01()) -> 01() 1181.66/297.29 , mark(s1(X)) -> s1(mark(X)) 1181.66/297.29 , mark(dbl1(X)) -> a__dbl1(mark(X)) 1181.66/297.29 , mark(sel1(X1, X2)) -> a__sel1(mark(X1), mark(X2)) 1181.66/297.29 , mark(quote(X)) -> a__quote(mark(X)) 1181.66/297.29 , a__indx(X1, X2) -> indx(X1, X2) 1181.66/297.29 , a__indx(nil(), X) -> nil() 1181.66/297.29 , a__indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z)) 1181.66/297.29 , a__from(X) -> cons(X, from(s(X))) 1181.66/297.29 , a__from(X) -> from(X) 1181.66/297.29 , a__dbl1(X) -> dbl1(X) 1181.66/297.29 , a__dbl1(0()) -> 01() 1181.66/297.29 , a__dbl1(s(X)) -> s1(s1(a__dbl1(mark(X)))) 1181.66/297.29 , a__sel1(X1, X2) -> sel1(X1, X2) 1181.66/297.29 , a__sel1(0(), cons(X, Y)) -> mark(X) 1181.66/297.29 , a__sel1(s(X), cons(Y, Z)) -> a__sel1(mark(X), mark(Z)) 1181.66/297.29 , a__quote(X) -> quote(X) 1181.66/297.29 , a__quote(0()) -> 01() 1181.66/297.29 , a__quote(s(X)) -> s1(a__quote(mark(X))) 1181.66/297.29 , a__quote(dbl(X)) -> a__dbl1(mark(X)) 1181.66/297.29 , a__quote(sel(X, Y)) -> a__sel1(mark(X), mark(Y)) } 1181.66/297.29 Weak DPs: 1181.66/297.29 { a__dbl^#(0()) -> c_2() 1181.66/297.29 , a__dbls^#(nil()) -> c_5() 1181.66/297.29 , mark^#(0()) -> c_10() 1181.66/297.29 , mark^#(nil()) -> c_13() 1181.66/297.29 , mark^#(01()) -> c_19() 1181.66/297.29 , a__indx^#(nil(), X) -> c_25() 1181.66/297.29 , a__dbl1^#(0()) -> c_30() 1181.66/297.29 , a__quote^#(0()) -> c_36() } 1181.66/297.29 Obligation: 1181.66/297.29 runtime complexity 1181.66/297.29 Answer: 1181.66/297.29 MAYBE 1181.66/297.29 1181.66/297.29 Empty strict component of the problem is NOT empty. 1181.66/297.29 1181.66/297.29 1181.66/297.29 Arrrr.. 1182.26/297.46 EOF