MAYBE 784.64/297.13 MAYBE 784.64/297.13 784.64/297.13 We are left with following problem, upon which TcT provides the 784.64/297.13 certificate MAYBE. 784.64/297.13 784.64/297.13 Strict Trs: 784.64/297.13 { a__pairNs() -> cons(0(), incr(oddNs())) 784.64/297.13 , a__pairNs() -> pairNs() 784.64/297.13 , a__oddNs() -> oddNs() 784.64/297.13 , a__oddNs() -> a__incr(a__pairNs()) 784.64/297.13 , a__incr(X) -> incr(X) 784.64/297.13 , a__incr(cons(X, XS)) -> cons(s(mark(X)), incr(XS)) 784.64/297.13 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 784.64/297.13 , mark(0()) -> 0() 784.64/297.13 , mark(incr(X)) -> a__incr(mark(X)) 784.64/297.13 , mark(oddNs()) -> a__oddNs() 784.64/297.13 , mark(s(X)) -> s(mark(X)) 784.64/297.13 , mark(nil()) -> nil() 784.64/297.13 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 784.64/297.13 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 784.64/297.13 , mark(zip(X1, X2)) -> a__zip(mark(X1), mark(X2)) 784.64/297.13 , mark(repItems(X)) -> a__repItems(mark(X)) 784.64/297.13 , mark(pairNs()) -> a__pairNs() 784.64/297.13 , mark(tail(X)) -> a__tail(mark(X)) 784.64/297.13 , a__take(X1, X2) -> take(X1, X2) 784.64/297.13 , a__take(0(), XS) -> nil() 784.64/297.13 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 784.64/297.13 , a__zip(X1, X2) -> zip(X1, X2) 784.64/297.13 , a__zip(X, nil()) -> nil() 784.64/297.13 , a__zip(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 cons(pair(mark(X), mark(Y)), zip(XS, YS)) 784.64/297.13 , a__zip(nil(), XS) -> nil() 784.64/297.13 , a__tail(X) -> tail(X) 784.64/297.13 , a__tail(cons(X, XS)) -> mark(XS) 784.64/297.13 , a__repItems(X) -> repItems(X) 784.64/297.13 , a__repItems(cons(X, XS)) -> cons(mark(X), cons(X, repItems(XS))) 784.64/297.13 , a__repItems(nil()) -> nil() } 784.64/297.13 Obligation: 784.64/297.13 runtime complexity 784.64/297.13 Answer: 784.64/297.13 MAYBE 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 784.64/297.13 following reason: 784.64/297.13 784.64/297.13 Computation stopped due to timeout after 297.0 seconds. 784.64/297.13 784.64/297.13 2) 'Best' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 784.64/297.13 seconds)' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'empty' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 2) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'empty' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 2) 'Fastest' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'empty' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 2) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'empty' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 2) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'empty' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 2) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 784.64/297.13 784.64/297.13 784.64/297.13 2) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'empty' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 2) 'With Problem ...' failed due to the following reason: 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 784.64/297.13 784.64/297.13 784.64/297.13 784.64/297.13 2) 'Best' failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 784.64/297.13 to the following reason: 784.64/297.13 784.64/297.13 The processor is inapplicable, reason: 784.64/297.13 Processor only applicable for innermost runtime complexity analysis 784.64/297.13 784.64/297.13 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 784.64/297.13 following reason: 784.64/297.13 784.64/297.13 The processor is inapplicable, reason: 784.64/297.13 Processor only applicable for innermost runtime complexity analysis 784.64/297.13 784.64/297.13 784.64/297.13 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 784.64/297.13 failed due to the following reason: 784.64/297.13 784.64/297.13 None of the processors succeeded. 784.64/297.13 784.64/297.13 Details of failed attempt(s): 784.64/297.13 ----------------------------- 784.64/297.13 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 784.64/297.13 failed due to the following reason: 784.64/297.13 784.64/297.13 match-boundness of the problem could not be verified. 784.64/297.13 784.64/297.13 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 784.64/297.13 failed due to the following reason: 784.64/297.13 784.64/297.13 match-boundness of the problem could not be verified. 784.64/297.13 784.64/297.13 784.64/297.13 784.64/297.13 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 784.64/297.13 the following reason: 784.64/297.13 784.64/297.13 We add the following weak dependency pairs: 784.64/297.13 784.64/297.13 Strict DPs: 784.64/297.13 { a__pairNs^#() -> c_1() 784.64/297.13 , a__pairNs^#() -> c_2() 784.64/297.13 , a__oddNs^#() -> c_3() 784.64/297.13 , a__oddNs^#() -> c_4(a__incr^#(a__pairNs())) 784.64/297.13 , a__incr^#(X) -> c_5(X) 784.64/297.13 , a__incr^#(cons(X, XS)) -> c_6(mark^#(X), XS) 784.64/297.13 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 784.64/297.13 , mark^#(0()) -> c_8() 784.64/297.13 , mark^#(incr(X)) -> c_9(a__incr^#(mark(X))) 784.64/297.13 , mark^#(oddNs()) -> c_10(a__oddNs^#()) 784.64/297.13 , mark^#(s(X)) -> c_11(mark^#(X)) 784.64/297.13 , mark^#(nil()) -> c_12() 784.64/297.13 , mark^#(take(X1, X2)) -> c_13(a__take^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(pair(X1, X2)) -> c_14(mark^#(X1), mark^#(X2)) 784.64/297.13 , mark^#(zip(X1, X2)) -> c_15(a__zip^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(repItems(X)) -> c_16(a__repItems^#(mark(X))) 784.64/297.13 , mark^#(pairNs()) -> c_17(a__pairNs^#()) 784.64/297.13 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 784.64/297.13 , a__take^#(X1, X2) -> c_19(X1, X2) 784.64/297.13 , a__take^#(0(), XS) -> c_20() 784.64/297.13 , a__take^#(s(N), cons(X, XS)) -> c_21(mark^#(X), N, XS) 784.64/297.13 , a__zip^#(X1, X2) -> c_22(X1, X2) 784.64/297.13 , a__zip^#(X, nil()) -> c_23() 784.64/297.13 , a__zip^#(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 c_24(mark^#(X), mark^#(Y), XS, YS) 784.64/297.13 , a__zip^#(nil(), XS) -> c_25() 784.64/297.13 , a__repItems^#(X) -> c_28(X) 784.64/297.13 , a__repItems^#(cons(X, XS)) -> c_29(mark^#(X), X, XS) 784.64/297.13 , a__repItems^#(nil()) -> c_30() 784.64/297.13 , a__tail^#(X) -> c_26(X) 784.64/297.13 , a__tail^#(cons(X, XS)) -> c_27(mark^#(XS)) } 784.64/297.13 784.64/297.13 and mark the set of starting terms. 784.64/297.13 784.64/297.13 We are left with following problem, upon which TcT provides the 784.64/297.13 certificate MAYBE. 784.64/297.13 784.64/297.13 Strict DPs: 784.64/297.13 { a__pairNs^#() -> c_1() 784.64/297.13 , a__pairNs^#() -> c_2() 784.64/297.13 , a__oddNs^#() -> c_3() 784.64/297.13 , a__oddNs^#() -> c_4(a__incr^#(a__pairNs())) 784.64/297.13 , a__incr^#(X) -> c_5(X) 784.64/297.13 , a__incr^#(cons(X, XS)) -> c_6(mark^#(X), XS) 784.64/297.13 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 784.64/297.13 , mark^#(0()) -> c_8() 784.64/297.13 , mark^#(incr(X)) -> c_9(a__incr^#(mark(X))) 784.64/297.13 , mark^#(oddNs()) -> c_10(a__oddNs^#()) 784.64/297.13 , mark^#(s(X)) -> c_11(mark^#(X)) 784.64/297.13 , mark^#(nil()) -> c_12() 784.64/297.13 , mark^#(take(X1, X2)) -> c_13(a__take^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(pair(X1, X2)) -> c_14(mark^#(X1), mark^#(X2)) 784.64/297.13 , mark^#(zip(X1, X2)) -> c_15(a__zip^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(repItems(X)) -> c_16(a__repItems^#(mark(X))) 784.64/297.13 , mark^#(pairNs()) -> c_17(a__pairNs^#()) 784.64/297.13 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 784.64/297.13 , a__take^#(X1, X2) -> c_19(X1, X2) 784.64/297.13 , a__take^#(0(), XS) -> c_20() 784.64/297.13 , a__take^#(s(N), cons(X, XS)) -> c_21(mark^#(X), N, XS) 784.64/297.13 , a__zip^#(X1, X2) -> c_22(X1, X2) 784.64/297.13 , a__zip^#(X, nil()) -> c_23() 784.64/297.13 , a__zip^#(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 c_24(mark^#(X), mark^#(Y), XS, YS) 784.64/297.13 , a__zip^#(nil(), XS) -> c_25() 784.64/297.13 , a__repItems^#(X) -> c_28(X) 784.64/297.13 , a__repItems^#(cons(X, XS)) -> c_29(mark^#(X), X, XS) 784.64/297.13 , a__repItems^#(nil()) -> c_30() 784.64/297.13 , a__tail^#(X) -> c_26(X) 784.64/297.13 , a__tail^#(cons(X, XS)) -> c_27(mark^#(XS)) } 784.64/297.13 Strict Trs: 784.64/297.13 { a__pairNs() -> cons(0(), incr(oddNs())) 784.64/297.13 , a__pairNs() -> pairNs() 784.64/297.13 , a__oddNs() -> oddNs() 784.64/297.13 , a__oddNs() -> a__incr(a__pairNs()) 784.64/297.13 , a__incr(X) -> incr(X) 784.64/297.13 , a__incr(cons(X, XS)) -> cons(s(mark(X)), incr(XS)) 784.64/297.13 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 784.64/297.13 , mark(0()) -> 0() 784.64/297.13 , mark(incr(X)) -> a__incr(mark(X)) 784.64/297.13 , mark(oddNs()) -> a__oddNs() 784.64/297.13 , mark(s(X)) -> s(mark(X)) 784.64/297.13 , mark(nil()) -> nil() 784.64/297.13 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 784.64/297.13 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 784.64/297.13 , mark(zip(X1, X2)) -> a__zip(mark(X1), mark(X2)) 784.64/297.13 , mark(repItems(X)) -> a__repItems(mark(X)) 784.64/297.13 , mark(pairNs()) -> a__pairNs() 784.64/297.13 , mark(tail(X)) -> a__tail(mark(X)) 784.64/297.13 , a__take(X1, X2) -> take(X1, X2) 784.64/297.13 , a__take(0(), XS) -> nil() 784.64/297.13 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 784.64/297.13 , a__zip(X1, X2) -> zip(X1, X2) 784.64/297.13 , a__zip(X, nil()) -> nil() 784.64/297.13 , a__zip(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 cons(pair(mark(X), mark(Y)), zip(XS, YS)) 784.64/297.13 , a__zip(nil(), XS) -> nil() 784.64/297.13 , a__tail(X) -> tail(X) 784.64/297.13 , a__tail(cons(X, XS)) -> mark(XS) 784.64/297.13 , a__repItems(X) -> repItems(X) 784.64/297.13 , a__repItems(cons(X, XS)) -> cons(mark(X), cons(X, repItems(XS))) 784.64/297.13 , a__repItems(nil()) -> nil() } 784.64/297.13 Obligation: 784.64/297.13 runtime complexity 784.64/297.13 Answer: 784.64/297.13 MAYBE 784.64/297.13 784.64/297.13 We estimate the number of application of {1,2,3,8,12,20,23,25,28} 784.64/297.13 by applications of Pre({1,2,3,8,12,20,23,25,28}) = 784.64/297.13 {5,6,7,10,11,13,14,15,16,17,19,21,22,24,26,27,29,30}. Here rules 784.64/297.13 are labeled as follows: 784.64/297.13 784.64/297.13 DPs: 784.64/297.13 { 1: a__pairNs^#() -> c_1() 784.64/297.13 , 2: a__pairNs^#() -> c_2() 784.64/297.13 , 3: a__oddNs^#() -> c_3() 784.64/297.13 , 4: a__oddNs^#() -> c_4(a__incr^#(a__pairNs())) 784.64/297.13 , 5: a__incr^#(X) -> c_5(X) 784.64/297.13 , 6: a__incr^#(cons(X, XS)) -> c_6(mark^#(X), XS) 784.64/297.13 , 7: mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 784.64/297.13 , 8: mark^#(0()) -> c_8() 784.64/297.13 , 9: mark^#(incr(X)) -> c_9(a__incr^#(mark(X))) 784.64/297.13 , 10: mark^#(oddNs()) -> c_10(a__oddNs^#()) 784.64/297.13 , 11: mark^#(s(X)) -> c_11(mark^#(X)) 784.64/297.13 , 12: mark^#(nil()) -> c_12() 784.64/297.13 , 13: mark^#(take(X1, X2)) -> c_13(a__take^#(mark(X1), mark(X2))) 784.64/297.13 , 14: mark^#(pair(X1, X2)) -> c_14(mark^#(X1), mark^#(X2)) 784.64/297.13 , 15: mark^#(zip(X1, X2)) -> c_15(a__zip^#(mark(X1), mark(X2))) 784.64/297.13 , 16: mark^#(repItems(X)) -> c_16(a__repItems^#(mark(X))) 784.64/297.13 , 17: mark^#(pairNs()) -> c_17(a__pairNs^#()) 784.64/297.13 , 18: mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 784.64/297.13 , 19: a__take^#(X1, X2) -> c_19(X1, X2) 784.64/297.13 , 20: a__take^#(0(), XS) -> c_20() 784.64/297.13 , 21: a__take^#(s(N), cons(X, XS)) -> c_21(mark^#(X), N, XS) 784.64/297.13 , 22: a__zip^#(X1, X2) -> c_22(X1, X2) 784.64/297.13 , 23: a__zip^#(X, nil()) -> c_23() 784.64/297.13 , 24: a__zip^#(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 c_24(mark^#(X), mark^#(Y), XS, YS) 784.64/297.13 , 25: a__zip^#(nil(), XS) -> c_25() 784.64/297.13 , 26: a__repItems^#(X) -> c_28(X) 784.64/297.13 , 27: a__repItems^#(cons(X, XS)) -> c_29(mark^#(X), X, XS) 784.64/297.13 , 28: a__repItems^#(nil()) -> c_30() 784.64/297.13 , 29: a__tail^#(X) -> c_26(X) 784.64/297.13 , 30: a__tail^#(cons(X, XS)) -> c_27(mark^#(XS)) } 784.64/297.13 784.64/297.13 We are left with following problem, upon which TcT provides the 784.64/297.13 certificate MAYBE. 784.64/297.13 784.64/297.13 Strict DPs: 784.64/297.13 { a__oddNs^#() -> c_4(a__incr^#(a__pairNs())) 784.64/297.13 , a__incr^#(X) -> c_5(X) 784.64/297.13 , a__incr^#(cons(X, XS)) -> c_6(mark^#(X), XS) 784.64/297.13 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 784.64/297.13 , mark^#(incr(X)) -> c_9(a__incr^#(mark(X))) 784.64/297.13 , mark^#(oddNs()) -> c_10(a__oddNs^#()) 784.64/297.13 , mark^#(s(X)) -> c_11(mark^#(X)) 784.64/297.13 , mark^#(take(X1, X2)) -> c_13(a__take^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(pair(X1, X2)) -> c_14(mark^#(X1), mark^#(X2)) 784.64/297.13 , mark^#(zip(X1, X2)) -> c_15(a__zip^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(repItems(X)) -> c_16(a__repItems^#(mark(X))) 784.64/297.13 , mark^#(pairNs()) -> c_17(a__pairNs^#()) 784.64/297.13 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 784.64/297.13 , a__take^#(X1, X2) -> c_19(X1, X2) 784.64/297.13 , a__take^#(s(N), cons(X, XS)) -> c_21(mark^#(X), N, XS) 784.64/297.13 , a__zip^#(X1, X2) -> c_22(X1, X2) 784.64/297.13 , a__zip^#(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 c_24(mark^#(X), mark^#(Y), XS, YS) 784.64/297.13 , a__repItems^#(X) -> c_28(X) 784.64/297.13 , a__repItems^#(cons(X, XS)) -> c_29(mark^#(X), X, XS) 784.64/297.13 , a__tail^#(X) -> c_26(X) 784.64/297.13 , a__tail^#(cons(X, XS)) -> c_27(mark^#(XS)) } 784.64/297.13 Strict Trs: 784.64/297.13 { a__pairNs() -> cons(0(), incr(oddNs())) 784.64/297.13 , a__pairNs() -> pairNs() 784.64/297.13 , a__oddNs() -> oddNs() 784.64/297.13 , a__oddNs() -> a__incr(a__pairNs()) 784.64/297.13 , a__incr(X) -> incr(X) 784.64/297.13 , a__incr(cons(X, XS)) -> cons(s(mark(X)), incr(XS)) 784.64/297.13 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 784.64/297.13 , mark(0()) -> 0() 784.64/297.13 , mark(incr(X)) -> a__incr(mark(X)) 784.64/297.13 , mark(oddNs()) -> a__oddNs() 784.64/297.13 , mark(s(X)) -> s(mark(X)) 784.64/297.13 , mark(nil()) -> nil() 784.64/297.13 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 784.64/297.13 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 784.64/297.13 , mark(zip(X1, X2)) -> a__zip(mark(X1), mark(X2)) 784.64/297.13 , mark(repItems(X)) -> a__repItems(mark(X)) 784.64/297.13 , mark(pairNs()) -> a__pairNs() 784.64/297.13 , mark(tail(X)) -> a__tail(mark(X)) 784.64/297.13 , a__take(X1, X2) -> take(X1, X2) 784.64/297.13 , a__take(0(), XS) -> nil() 784.64/297.13 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 784.64/297.13 , a__zip(X1, X2) -> zip(X1, X2) 784.64/297.13 , a__zip(X, nil()) -> nil() 784.64/297.13 , a__zip(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 cons(pair(mark(X), mark(Y)), zip(XS, YS)) 784.64/297.13 , a__zip(nil(), XS) -> nil() 784.64/297.13 , a__tail(X) -> tail(X) 784.64/297.13 , a__tail(cons(X, XS)) -> mark(XS) 784.64/297.13 , a__repItems(X) -> repItems(X) 784.64/297.13 , a__repItems(cons(X, XS)) -> cons(mark(X), cons(X, repItems(XS))) 784.64/297.13 , a__repItems(nil()) -> nil() } 784.64/297.13 Weak DPs: 784.64/297.13 { a__pairNs^#() -> c_1() 784.64/297.13 , a__pairNs^#() -> c_2() 784.64/297.13 , a__oddNs^#() -> c_3() 784.64/297.13 , mark^#(0()) -> c_8() 784.64/297.13 , mark^#(nil()) -> c_12() 784.64/297.13 , a__take^#(0(), XS) -> c_20() 784.64/297.13 , a__zip^#(X, nil()) -> c_23() 784.64/297.13 , a__zip^#(nil(), XS) -> c_25() 784.64/297.13 , a__repItems^#(nil()) -> c_30() } 784.64/297.13 Obligation: 784.64/297.13 runtime complexity 784.64/297.13 Answer: 784.64/297.13 MAYBE 784.64/297.13 784.64/297.13 We estimate the number of application of {12} by applications of 784.64/297.13 Pre({12}) = {2,3,4,7,9,14,15,16,17,18,19,20,21}. Here rules are 784.64/297.13 labeled as follows: 784.64/297.13 784.64/297.13 DPs: 784.64/297.13 { 1: a__oddNs^#() -> c_4(a__incr^#(a__pairNs())) 784.64/297.13 , 2: a__incr^#(X) -> c_5(X) 784.64/297.13 , 3: a__incr^#(cons(X, XS)) -> c_6(mark^#(X), XS) 784.64/297.13 , 4: mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 784.64/297.13 , 5: mark^#(incr(X)) -> c_9(a__incr^#(mark(X))) 784.64/297.13 , 6: mark^#(oddNs()) -> c_10(a__oddNs^#()) 784.64/297.13 , 7: mark^#(s(X)) -> c_11(mark^#(X)) 784.64/297.13 , 8: mark^#(take(X1, X2)) -> c_13(a__take^#(mark(X1), mark(X2))) 784.64/297.13 , 9: mark^#(pair(X1, X2)) -> c_14(mark^#(X1), mark^#(X2)) 784.64/297.13 , 10: mark^#(zip(X1, X2)) -> c_15(a__zip^#(mark(X1), mark(X2))) 784.64/297.13 , 11: mark^#(repItems(X)) -> c_16(a__repItems^#(mark(X))) 784.64/297.13 , 12: mark^#(pairNs()) -> c_17(a__pairNs^#()) 784.64/297.13 , 13: mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 784.64/297.13 , 14: a__take^#(X1, X2) -> c_19(X1, X2) 784.64/297.13 , 15: a__take^#(s(N), cons(X, XS)) -> c_21(mark^#(X), N, XS) 784.64/297.13 , 16: a__zip^#(X1, X2) -> c_22(X1, X2) 784.64/297.13 , 17: a__zip^#(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 c_24(mark^#(X), mark^#(Y), XS, YS) 784.64/297.13 , 18: a__repItems^#(X) -> c_28(X) 784.64/297.13 , 19: a__repItems^#(cons(X, XS)) -> c_29(mark^#(X), X, XS) 784.64/297.13 , 20: a__tail^#(X) -> c_26(X) 784.64/297.13 , 21: a__tail^#(cons(X, XS)) -> c_27(mark^#(XS)) 784.64/297.13 , 22: a__pairNs^#() -> c_1() 784.64/297.13 , 23: a__pairNs^#() -> c_2() 784.64/297.13 , 24: a__oddNs^#() -> c_3() 784.64/297.13 , 25: mark^#(0()) -> c_8() 784.64/297.13 , 26: mark^#(nil()) -> c_12() 784.64/297.13 , 27: a__take^#(0(), XS) -> c_20() 784.64/297.13 , 28: a__zip^#(X, nil()) -> c_23() 784.64/297.13 , 29: a__zip^#(nil(), XS) -> c_25() 784.64/297.13 , 30: a__repItems^#(nil()) -> c_30() } 784.64/297.13 784.64/297.13 We are left with following problem, upon which TcT provides the 784.64/297.13 certificate MAYBE. 784.64/297.13 784.64/297.13 Strict DPs: 784.64/297.13 { a__oddNs^#() -> c_4(a__incr^#(a__pairNs())) 784.64/297.13 , a__incr^#(X) -> c_5(X) 784.64/297.13 , a__incr^#(cons(X, XS)) -> c_6(mark^#(X), XS) 784.64/297.13 , mark^#(cons(X1, X2)) -> c_7(mark^#(X1), X2) 784.64/297.13 , mark^#(incr(X)) -> c_9(a__incr^#(mark(X))) 784.64/297.13 , mark^#(oddNs()) -> c_10(a__oddNs^#()) 784.64/297.13 , mark^#(s(X)) -> c_11(mark^#(X)) 784.64/297.13 , mark^#(take(X1, X2)) -> c_13(a__take^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(pair(X1, X2)) -> c_14(mark^#(X1), mark^#(X2)) 784.64/297.13 , mark^#(zip(X1, X2)) -> c_15(a__zip^#(mark(X1), mark(X2))) 784.64/297.13 , mark^#(repItems(X)) -> c_16(a__repItems^#(mark(X))) 784.64/297.13 , mark^#(tail(X)) -> c_18(a__tail^#(mark(X))) 784.64/297.13 , a__take^#(X1, X2) -> c_19(X1, X2) 784.64/297.13 , a__take^#(s(N), cons(X, XS)) -> c_21(mark^#(X), N, XS) 784.64/297.13 , a__zip^#(X1, X2) -> c_22(X1, X2) 784.64/297.13 , a__zip^#(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 c_24(mark^#(X), mark^#(Y), XS, YS) 784.64/297.13 , a__repItems^#(X) -> c_28(X) 784.64/297.13 , a__repItems^#(cons(X, XS)) -> c_29(mark^#(X), X, XS) 784.64/297.13 , a__tail^#(X) -> c_26(X) 784.64/297.13 , a__tail^#(cons(X, XS)) -> c_27(mark^#(XS)) } 784.64/297.13 Strict Trs: 784.64/297.13 { a__pairNs() -> cons(0(), incr(oddNs())) 784.64/297.13 , a__pairNs() -> pairNs() 784.64/297.13 , a__oddNs() -> oddNs() 784.64/297.13 , a__oddNs() -> a__incr(a__pairNs()) 784.64/297.13 , a__incr(X) -> incr(X) 784.64/297.13 , a__incr(cons(X, XS)) -> cons(s(mark(X)), incr(XS)) 784.64/297.13 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 784.64/297.13 , mark(0()) -> 0() 784.64/297.13 , mark(incr(X)) -> a__incr(mark(X)) 784.64/297.13 , mark(oddNs()) -> a__oddNs() 784.64/297.13 , mark(s(X)) -> s(mark(X)) 784.64/297.13 , mark(nil()) -> nil() 784.64/297.13 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 784.64/297.13 , mark(pair(X1, X2)) -> pair(mark(X1), mark(X2)) 784.64/297.13 , mark(zip(X1, X2)) -> a__zip(mark(X1), mark(X2)) 784.64/297.13 , mark(repItems(X)) -> a__repItems(mark(X)) 784.64/297.13 , mark(pairNs()) -> a__pairNs() 784.64/297.13 , mark(tail(X)) -> a__tail(mark(X)) 784.64/297.13 , a__take(X1, X2) -> take(X1, X2) 784.64/297.13 , a__take(0(), XS) -> nil() 784.64/297.13 , a__take(s(N), cons(X, XS)) -> cons(mark(X), take(N, XS)) 784.64/297.13 , a__zip(X1, X2) -> zip(X1, X2) 784.64/297.13 , a__zip(X, nil()) -> nil() 784.64/297.13 , a__zip(cons(X, XS), cons(Y, YS)) -> 784.64/297.13 cons(pair(mark(X), mark(Y)), zip(XS, YS)) 784.64/297.13 , a__zip(nil(), XS) -> nil() 784.64/297.13 , a__tail(X) -> tail(X) 784.64/297.13 , a__tail(cons(X, XS)) -> mark(XS) 784.64/297.13 , a__repItems(X) -> repItems(X) 784.64/297.13 , a__repItems(cons(X, XS)) -> cons(mark(X), cons(X, repItems(XS))) 784.64/297.13 , a__repItems(nil()) -> nil() } 784.64/297.13 Weak DPs: 784.64/297.13 { a__pairNs^#() -> c_1() 784.64/297.13 , a__pairNs^#() -> c_2() 784.64/297.13 , a__oddNs^#() -> c_3() 784.64/297.13 , mark^#(0()) -> c_8() 784.64/297.13 , mark^#(nil()) -> c_12() 784.64/297.13 , mark^#(pairNs()) -> c_17(a__pairNs^#()) 784.64/297.13 , a__take^#(0(), XS) -> c_20() 784.64/297.13 , a__zip^#(X, nil()) -> c_23() 784.64/297.13 , a__zip^#(nil(), XS) -> c_25() 784.64/297.13 , a__repItems^#(nil()) -> c_30() } 784.64/297.13 Obligation: 784.64/297.13 runtime complexity 784.64/297.13 Answer: 784.64/297.13 MAYBE 784.64/297.13 784.64/297.13 Empty strict component of the problem is NOT empty. 784.64/297.13 784.64/297.13 784.64/297.13 Arrrr.. 784.64/297.19 EOF