Runtime Complexity TRS:
The TRS R consists of the following rules:

a__pairNs → cons(0, incr(oddNs))
a__oddNs → a__incr(a__pairNs)
a__incr(cons(X, XS)) → cons(s(mark(X)), incr(XS))
a__take(0, XS) → nil
a__take(s(N), cons(X, XS)) → cons(mark(X), take(N, XS))
a__zip(nil, XS) → nil
a__zip(X, nil) → nil
a__zip(cons(X, XS), cons(Y, YS)) → cons(pair(mark(X), mark(Y)), zip(XS, YS))
a__tail(cons(X, XS)) → mark(XS)
a__repItems(nil) → nil
a__repItems(cons(X, XS)) → cons(mark(X), cons(X, repItems(XS)))
mark(pairNs) → a__pairNs
mark(incr(X)) → a__incr(mark(X))
mark(oddNs) → a__oddNs
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(zip(X1, X2)) → a__zip(mark(X1), mark(X2))
mark(tail(X)) → a__tail(mark(X))
mark(repItems(X)) → a__repItems(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(s(X)) → s(mark(X))
mark(nil) → nil
mark(pair(X1, X2)) → pair(mark(X1), mark(X2))
a__pairNs → pairNs
a__incr(X) → incr(X)
a__oddNs → oddNs
a__take(X1, X2) → take(X1, X2)
a__zip(X1, X2) → zip(X1, X2)
a__tail(X) → tail(X)
a__repItems(X) → repItems(X)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__pairNs' → cons'(0', incr'(oddNs'))
a__oddNs' → a__incr'(a__pairNs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__take'(0', XS) → nil'
a__take'(s'(N), cons'(X, XS)) → cons'(mark'(X), take'(N, XS))
a__zip'(nil', XS) → nil'
a__zip'(X, nil') → nil'
a__zip'(cons'(X, XS), cons'(Y, YS)) → cons'(pair'(mark'(X), mark'(Y)), zip'(XS, YS))
a__tail'(cons'(X, XS)) → mark'(XS)
a__repItems'(nil') → nil'
a__repItems'(cons'(X, XS)) → cons'(mark'(X), cons'(X, repItems'(XS)))
mark'(pairNs') → a__pairNs'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(oddNs') → a__oddNs'
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(zip'(X1, X2)) → a__zip'(mark'(X1), mark'(X2))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(repItems'(X)) → a__repItems'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(nil') → nil'
mark'(pair'(X1, X2)) → pair'(mark'(X1), mark'(X2))
a__pairNs' → pairNs'
a__incr'(X) → incr'(X)
a__oddNs' → oddNs'
a__take'(X1, X2) → take'(X1, X2)
a__zip'(X1, X2) → zip'(X1, X2)
a__tail'(X) → tail'(X)
a__repItems'(X) → repItems'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__pairNs' → cons'(0', incr'(oddNs'))
a__oddNs' → a__incr'(a__pairNs')
a__incr'(cons'(X, XS)) → cons'(s'(mark'(X)), incr'(XS))
a__take'(0', XS) → nil'
a__take'(s'(N), cons'(X, XS)) → cons'(mark'(X), take'(N, XS))
a__zip'(nil', XS) → nil'
a__zip'(X, nil') → nil'
a__zip'(cons'(X, XS), cons'(Y, YS)) → cons'(pair'(mark'(X), mark'(Y)), zip'(XS, YS))
a__tail'(cons'(X, XS)) → mark'(XS)
a__repItems'(nil') → nil'
a__repItems'(cons'(X, XS)) → cons'(mark'(X), cons'(X, repItems'(XS)))
mark'(pairNs') → a__pairNs'
mark'(incr'(X)) → a__incr'(mark'(X))
mark'(oddNs') → a__oddNs'
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(zip'(X1, X2)) → a__zip'(mark'(X1), mark'(X2))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(repItems'(X)) → a__repItems'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(s'(X)) → s'(mark'(X))
mark'(nil') → nil'
mark'(pair'(X1, X2)) → pair'(mark'(X1), mark'(X2))
a__pairNs' → pairNs'
a__incr'(X) → incr'(X)
a__oddNs' → oddNs'
a__take'(X1, X2) → take'(X1, X2)
a__zip'(X1, X2) → zip'(X1, X2)
a__tail'(X) → tail'(X)
a__repItems'(X) → repItems'(X)

Types:
a__pairNs' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
cons' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
0' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
incr' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
oddNs' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
a__oddNs' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
a__incr' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
s' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
mark' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
a__take' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
nil' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
take' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
a__zip' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
pair' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
zip' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
a__tail' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
a__repItems' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
repItems' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
pairNs' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
tail' :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail' → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
_hole_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'1 :: 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'
_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2 :: Nat → 0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'

Heuristically decided to analyse the following defined symbols:
a__oddNs', a__incr', mark', a__tail', a__repItems'

They will be analysed ascendingly in the following order:
a__oddNs' = a__incr'
a__oddNs' = mark'
a__oddNs' = a__tail'
a__oddNs' = a__repItems'
a__incr' = mark'
a__incr' = a__tail'
a__incr' = a__repItems'
mark' = a__tail'
mark' = a__repItems'
a__tail' = a__repItems'

Generator Equations:
_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(0) ⇔ 0'
_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(+(x, 1)) ⇔ cons'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(x), 0')

The following defined symbols remain to be analysed:
a__incr', a__oddNs', mark', a__tail', a__repItems'

Could not prove a rewrite lemma for the defined symbol a__incr'.

The following defined symbols remain to be analysed:
mark', a__oddNs', a__tail', a__repItems'

Proved the following rewrite lemma:
mark'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_n575949)) → _gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_n575949), rt ∈ Ω(1 + _n575949)

Induction Base:
mark'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(0)) →_R^Ω(1)
0'

Induction Step:
mark'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(+(_$n575950, 1))) →_R^Ω(1)
cons'(mark'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_$n575950)), 0') →_IH
cons'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_$n575950), 0')

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
mark'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_n575949)) → _gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_n575949), rt ∈ Ω(1 + _n575949)

The following defined symbols remain to be analysed:
a__oddNs', a__incr', a__tail', a__repItems'

Could not prove a rewrite lemma for the defined symbol a__oddNs'.

The following defined symbols remain to be analysed:
a__tail', a__incr', a__repItems'

Could not prove a rewrite lemma for the defined symbol a__tail'.

The following defined symbols remain to be analysed:
a__repItems', a__incr'

Could not prove a rewrite lemma for the defined symbol a__repItems'.

The following defined symbols remain to be analysed:
a__incr'

Could not prove a rewrite lemma for the defined symbol a__incr'.

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_n575949)) → _gen_0':oddNs':incr':cons':s':nil':take':pair':zip':repItems':pairNs':tail'2(_n575949), rt ∈ Ω(1 + _n575949)