YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { pairNs() -> cons(0(), n__incr(n__oddNs())) , cons(X1, X2) -> n__cons(X1, X2) , oddNs() -> n__oddNs() , oddNs() -> incr(pairNs()) , incr(X) -> n__incr(X) , incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__oddNs()) -> oddNs() , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__zip(X1, X2)) -> zip(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__repItems(X)) -> repItems(activate(X)) , take(X1, X2) -> n__take(X1, X2) , take(0(), XS) -> nil() , take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))) , zip(X1, X2) -> n__zip(X1, X2) , zip(X, nil()) -> nil() , zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate(XS), activate(YS))) , zip(nil(), XS) -> nil() , tail(cons(X, XS)) -> activate(XS) , repItems(X) -> n__repItems(X) , repItems(cons(X, XS)) -> cons(X, n__cons(X, n__repItems(activate(XS)))) , repItems(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) Arguments of following rules are not normal-forms: { incr(cons(X, XS)) -> cons(s(X), n__incr(activate(XS))) , take(s(N), cons(X, XS)) -> cons(X, n__take(N, activate(XS))) , zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate(XS), activate(YS))) , tail(cons(X, XS)) -> activate(XS) , repItems(cons(X, XS)) -> cons(X, n__cons(X, n__repItems(activate(XS)))) } All above mentioned rules can be savely removed. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { pairNs() -> cons(0(), n__incr(n__oddNs())) , cons(X1, X2) -> n__cons(X1, X2) , oddNs() -> n__oddNs() , oddNs() -> incr(pairNs()) , incr(X) -> n__incr(X) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__oddNs()) -> oddNs() , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__zip(X1, X2)) -> zip(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__repItems(X)) -> repItems(activate(X)) , take(X1, X2) -> n__take(X1, X2) , take(0(), XS) -> nil() , zip(X1, X2) -> n__zip(X1, X2) , zip(X, nil()) -> nil() , zip(nil(), XS) -> nil() , repItems(X) -> n__repItems(X) , repItems(nil()) -> nil() } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 4. The enriched problem is compatible with the following automaton. { pairNs_0() -> 1 , pairNs_1() -> 6 , pairNs_2() -> 10 , cons_0(2, 2) -> 1 , cons_1(3, 4) -> 1 , cons_1(6, 2) -> 1 , cons_1(6, 2) -> 6 , cons_2(7, 8) -> 6 , cons_3(11, 12) -> 10 , 0_0() -> 1 , 0_0() -> 2 , 0_0() -> 6 , 0_1() -> 3 , 0_2() -> 7 , 0_3() -> 11 , n__incr_0(2) -> 1 , n__incr_0(2) -> 2 , n__incr_0(2) -> 6 , n__incr_1(2) -> 1 , n__incr_1(5) -> 4 , n__incr_2(6) -> 1 , n__incr_2(6) -> 6 , n__incr_2(9) -> 8 , n__incr_3(10) -> 1 , n__incr_3(10) -> 6 , n__incr_3(13) -> 12 , n__oddNs_0() -> 1 , n__oddNs_0() -> 2 , n__oddNs_0() -> 6 , n__oddNs_1() -> 1 , n__oddNs_1() -> 5 , n__oddNs_2() -> 1 , n__oddNs_2() -> 6 , n__oddNs_2() -> 9 , n__oddNs_3() -> 13 , oddNs_0() -> 1 , oddNs_1() -> 1 , oddNs_1() -> 6 , incr_0(2) -> 1 , incr_1(6) -> 1 , incr_1(6) -> 6 , incr_2(10) -> 1 , incr_2(10) -> 6 , s_0(2) -> 1 , s_0(2) -> 2 , s_0(2) -> 6 , activate_0(2) -> 1 , activate_1(2) -> 6 , take_0(2, 2) -> 1 , take_1(6, 6) -> 1 , take_1(6, 6) -> 6 , nil_0() -> 1 , nil_0() -> 2 , nil_0() -> 6 , nil_1() -> 1 , nil_1() -> 6 , nil_2() -> 1 , nil_2() -> 6 , n__take_0(2, 2) -> 1 , n__take_0(2, 2) -> 2 , n__take_0(2, 2) -> 6 , n__take_1(2, 2) -> 1 , n__take_2(6, 6) -> 1 , n__take_2(6, 6) -> 6 , zip_0(2, 2) -> 1 , zip_1(6, 6) -> 1 , zip_1(6, 6) -> 6 , pair_0(2, 2) -> 1 , pair_0(2, 2) -> 2 , pair_0(2, 2) -> 6 , n__zip_0(2, 2) -> 1 , n__zip_0(2, 2) -> 2 , n__zip_0(2, 2) -> 6 , n__zip_1(2, 2) -> 1 , n__zip_2(6, 6) -> 1 , n__zip_2(6, 6) -> 6 , tail_0(2) -> 1 , repItems_0(2) -> 1 , repItems_1(6) -> 1 , repItems_1(6) -> 6 , n__cons_0(2, 2) -> 1 , n__cons_0(2, 2) -> 2 , n__cons_0(2, 2) -> 6 , n__cons_1(2, 2) -> 1 , n__cons_2(3, 4) -> 1 , n__cons_2(6, 2) -> 1 , n__cons_2(6, 2) -> 6 , n__cons_3(7, 8) -> 6 , n__cons_4(11, 12) -> 10 , n__repItems_0(2) -> 1 , n__repItems_0(2) -> 2 , n__repItems_0(2) -> 6 , n__repItems_1(2) -> 1 , n__repItems_2(6) -> 1 , n__repItems_2(6) -> 6 , 2 -> 1 , 2 -> 6 } Hurray, we answered YES(?,O(n^1))