MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { pairNs() -> cons(0(), incr(oddNs())) , incr(cons(X, XS)) -> cons(s(X), incr(XS)) , oddNs() -> incr(pairNs()) , take(0(), XS) -> nil() , take(s(N), cons(X, XS)) -> cons(X, take(N, XS)) , zip(X, nil()) -> nil() , zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS)) , zip(nil(), XS) -> nil() , tail(cons(X, XS)) -> XS , repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS))) , repItems(nil()) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { pairNs^#() -> c_1(incr^#(oddNs()), oddNs^#()) , incr^#(cons(X, XS)) -> c_2(incr^#(XS)) , oddNs^#() -> c_3(incr^#(pairNs()), pairNs^#()) , take^#(0(), XS) -> c_4() , take^#(s(N), cons(X, XS)) -> c_5(take^#(N, XS)) , zip^#(X, nil()) -> c_6() , zip^#(cons(X, XS), cons(Y, YS)) -> c_7(zip^#(XS, YS)) , zip^#(nil(), XS) -> c_8() , tail^#(cons(X, XS)) -> c_9() , repItems^#(cons(X, XS)) -> c_10(repItems^#(XS)) , repItems^#(nil()) -> c_11() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { pairNs^#() -> c_1(incr^#(oddNs()), oddNs^#()) , incr^#(cons(X, XS)) -> c_2(incr^#(XS)) , oddNs^#() -> c_3(incr^#(pairNs()), pairNs^#()) , take^#(0(), XS) -> c_4() , take^#(s(N), cons(X, XS)) -> c_5(take^#(N, XS)) , zip^#(X, nil()) -> c_6() , zip^#(cons(X, XS), cons(Y, YS)) -> c_7(zip^#(XS, YS)) , zip^#(nil(), XS) -> c_8() , tail^#(cons(X, XS)) -> c_9() , repItems^#(cons(X, XS)) -> c_10(repItems^#(XS)) , repItems^#(nil()) -> c_11() } Weak Trs: { pairNs() -> cons(0(), incr(oddNs())) , incr(cons(X, XS)) -> cons(s(X), incr(XS)) , oddNs() -> incr(pairNs()) , take(0(), XS) -> nil() , take(s(N), cons(X, XS)) -> cons(X, take(N, XS)) , zip(X, nil()) -> nil() , zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS)) , zip(nil(), XS) -> nil() , tail(cons(X, XS)) -> XS , repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS))) , repItems(nil()) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,6,8,9,11} by applications of Pre({4,6,8,9,11}) = {5,7,10}. Here rules are labeled as follows: DPs: { 1: pairNs^#() -> c_1(incr^#(oddNs()), oddNs^#()) , 2: incr^#(cons(X, XS)) -> c_2(incr^#(XS)) , 3: oddNs^#() -> c_3(incr^#(pairNs()), pairNs^#()) , 4: take^#(0(), XS) -> c_4() , 5: take^#(s(N), cons(X, XS)) -> c_5(take^#(N, XS)) , 6: zip^#(X, nil()) -> c_6() , 7: zip^#(cons(X, XS), cons(Y, YS)) -> c_7(zip^#(XS, YS)) , 8: zip^#(nil(), XS) -> c_8() , 9: tail^#(cons(X, XS)) -> c_9() , 10: repItems^#(cons(X, XS)) -> c_10(repItems^#(XS)) , 11: repItems^#(nil()) -> c_11() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { pairNs^#() -> c_1(incr^#(oddNs()), oddNs^#()) , incr^#(cons(X, XS)) -> c_2(incr^#(XS)) , oddNs^#() -> c_3(incr^#(pairNs()), pairNs^#()) , take^#(s(N), cons(X, XS)) -> c_5(take^#(N, XS)) , zip^#(cons(X, XS), cons(Y, YS)) -> c_7(zip^#(XS, YS)) , repItems^#(cons(X, XS)) -> c_10(repItems^#(XS)) } Weak DPs: { take^#(0(), XS) -> c_4() , zip^#(X, nil()) -> c_6() , zip^#(nil(), XS) -> c_8() , tail^#(cons(X, XS)) -> c_9() , repItems^#(nil()) -> c_11() } Weak Trs: { pairNs() -> cons(0(), incr(oddNs())) , incr(cons(X, XS)) -> cons(s(X), incr(XS)) , oddNs() -> incr(pairNs()) , take(0(), XS) -> nil() , take(s(N), cons(X, XS)) -> cons(X, take(N, XS)) , zip(X, nil()) -> nil() , zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS)) , zip(nil(), XS) -> nil() , tail(cons(X, XS)) -> XS , repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS))) , repItems(nil()) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { take^#(0(), XS) -> c_4() , zip^#(X, nil()) -> c_6() , zip^#(nil(), XS) -> c_8() , tail^#(cons(X, XS)) -> c_9() , repItems^#(nil()) -> c_11() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { pairNs^#() -> c_1(incr^#(oddNs()), oddNs^#()) , incr^#(cons(X, XS)) -> c_2(incr^#(XS)) , oddNs^#() -> c_3(incr^#(pairNs()), pairNs^#()) , take^#(s(N), cons(X, XS)) -> c_5(take^#(N, XS)) , zip^#(cons(X, XS), cons(Y, YS)) -> c_7(zip^#(XS, YS)) , repItems^#(cons(X, XS)) -> c_10(repItems^#(XS)) } Weak Trs: { pairNs() -> cons(0(), incr(oddNs())) , incr(cons(X, XS)) -> cons(s(X), incr(XS)) , oddNs() -> incr(pairNs()) , take(0(), XS) -> nil() , take(s(N), cons(X, XS)) -> cons(X, take(N, XS)) , zip(X, nil()) -> nil() , zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), zip(XS, YS)) , zip(nil(), XS) -> nil() , tail(cons(X, XS)) -> XS , repItems(cons(X, XS)) -> cons(X, cons(X, repItems(XS))) , repItems(nil()) -> nil() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { pairNs() -> cons(0(), incr(oddNs())) , incr(cons(X, XS)) -> cons(s(X), incr(XS)) , oddNs() -> incr(pairNs()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { pairNs^#() -> c_1(incr^#(oddNs()), oddNs^#()) , incr^#(cons(X, XS)) -> c_2(incr^#(XS)) , oddNs^#() -> c_3(incr^#(pairNs()), pairNs^#()) , take^#(s(N), cons(X, XS)) -> c_5(take^#(N, XS)) , zip^#(cons(X, XS), cons(Y, YS)) -> c_7(zip^#(XS, YS)) , repItems^#(cons(X, XS)) -> c_10(repItems^#(XS)) } Weak Trs: { pairNs() -> cons(0(), incr(oddNs())) , incr(cons(X, XS)) -> cons(s(X), incr(XS)) , oddNs() -> incr(pairNs()) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: The input cannot be shown compatible 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..