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 The input cannot be shown compatible Arrrr..