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

a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__sel(0, cons(X, Z)) → mark(X)
a__first(0, Z) → nil
a__first(s(X), cons(Y, Z)) → cons(mark(Y), first(X, Z))
a__from(X) → cons(mark(X), from(s(X)))
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__sel1(0, cons(X, Z)) → a__quote(X)
a__first1(0, Z) → nil1
a__first1(s(X), cons(Y, Z)) → cons1(a__quote(Y), a__first1(mark(X), mark(Z)))
a__quote(0) → 01
a__quote1(cons(X, Z)) → cons1(a__quote(X), a__quote1(Z))
a__quote1(nil) → nil1
a__quote(s(X)) → s1(a__quote(X))
a__quote(sel(X, Z)) → a__sel1(mark(X), mark(Z))
a__quote1(first(X, Z)) → a__first1(mark(X), mark(Z))
a__unquote(01) → 0
a__unquote(s1(X)) → s(a__unquote(mark(X)))
a__unquote1(nil1) → nil
a__unquote1(cons1(X, Z)) → a__fcons(a__unquote(mark(X)), a__unquote1(mark(Z)))
a__fcons(X, Z) → cons(mark(X), Z)
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(first(X1, X2)) → a__first(mark(X1), mark(X2))
mark(from(X)) → a__from(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(X)
mark(first1(X1, X2)) → a__first1(mark(X1), mark(X2))
mark(quote1(X)) → a__quote1(X)
mark(unquote(X)) → a__unquote(mark(X))
mark(unquote1(X)) → a__unquote1(mark(X))
mark(fcons(X1, X2)) → a__fcons(mark(X1), mark(X2))
mark(s(X)) → s(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(0) → 0
mark(nil) → nil
mark(nil1) → nil1
mark(cons1(X1, X2)) → cons1(mark(X1), mark(X2))
mark(01) → 01
mark(s1(X)) → s1(mark(X))
a__sel(X1, X2) → sel(X1, X2)
a__first(X1, X2) → first(X1, X2)
a__from(X) → from(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
a__first1(X1, X2) → first1(X1, X2)
a__quote1(X) → quote1(X)
a__unquote(X) → unquote(X)
a__unquote1(X) → unquote1(X)
a__fcons(X1, X2) → fcons(X1, X2)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a__sel'(s'(X), cons'(Y, Z)) → a__sel'(mark'(X), mark'(Z))
a__sel'(0', cons'(X, Z)) → mark'(X)
a__first'(0', Z) → nil'
a__first'(s'(X), cons'(Y, Z)) → cons'(mark'(Y), first'(X, Z))
a__from'(X) → cons'(mark'(X), from'(s'(X)))
a__sel1'(s'(X), cons'(Y, Z)) → a__sel1'(mark'(X), mark'(Z))
a__sel1'(0', cons'(X, Z)) → a__quote'(X)
a__first1'(0', Z) → nil1'
a__first1'(s'(X), cons'(Y, Z)) → cons1'(a__quote'(Y), a__first1'(mark'(X), mark'(Z)))
a__quote'(0') → 01'
a__quote1'(cons'(X, Z)) → cons1'(a__quote'(X), a__quote1'(Z))
a__quote1'(nil') → nil1'
a__quote'(s'(X)) → s1'(a__quote'(X))
a__quote'(sel'(X, Z)) → a__sel1'(mark'(X), mark'(Z))
a__quote1'(first'(X, Z)) → a__first1'(mark'(X), mark'(Z))
a__unquote'(01') → 0'
a__unquote'(s1'(X)) → s'(a__unquote'(mark'(X)))
a__unquote1'(nil1') → nil'
a__unquote1'(cons1'(X, Z)) → a__fcons'(a__unquote'(mark'(X)), a__unquote1'(mark'(Z)))
a__fcons'(X, Z) → cons'(mark'(X), Z)
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(first'(X1, X2)) → a__first'(mark'(X1), mark'(X2))
mark'(from'(X)) → a__from'(mark'(X))
mark'(sel1'(X1, X2)) → a__sel1'(mark'(X1), mark'(X2))
mark'(quote'(X)) → a__quote'(X)
mark'(first1'(X1, X2)) → a__first1'(mark'(X1), mark'(X2))
mark'(quote1'(X)) → a__quote1'(X)
mark'(unquote'(X)) → a__unquote'(mark'(X))
mark'(unquote1'(X)) → a__unquote1'(mark'(X))
mark'(fcons'(X1, X2)) → a__fcons'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(nil') → nil'
mark'(nil1') → nil1'
mark'(cons1'(X1, X2)) → cons1'(mark'(X1), mark'(X2))
mark'(01') → 01'
mark'(s1'(X)) → s1'(mark'(X))
a__sel'(X1, X2) → sel'(X1, X2)
a__first'(X1, X2) → first'(X1, X2)
a__from'(X) → from'(X)
a__sel1'(X1, X2) → sel1'(X1, X2)
a__quote'(X) → quote'(X)
a__first1'(X1, X2) → first1'(X1, X2)
a__quote1'(X) → quote1'(X)
a__unquote'(X) → unquote'(X)
a__unquote1'(X) → unquote1'(X)
a__fcons'(X1, X2) → fcons'(X1, X2)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__sel'(s'(X), cons'(Y, Z)) → a__sel'(mark'(X), mark'(Z))
a__sel'(0', cons'(X, Z)) → mark'(X)
a__first'(0', Z) → nil'
a__first'(s'(X), cons'(Y, Z)) → cons'(mark'(Y), first'(X, Z))
a__from'(X) → cons'(mark'(X), from'(s'(X)))
a__sel1'(s'(X), cons'(Y, Z)) → a__sel1'(mark'(X), mark'(Z))
a__sel1'(0', cons'(X, Z)) → a__quote'(X)
a__first1'(0', Z) → nil1'
a__first1'(s'(X), cons'(Y, Z)) → cons1'(a__quote'(Y), a__first1'(mark'(X), mark'(Z)))
a__quote'(0') → 01'
a__quote1'(cons'(X, Z)) → cons1'(a__quote'(X), a__quote1'(Z))
a__quote1'(nil') → nil1'
a__quote'(s'(X)) → s1'(a__quote'(X))
a__quote'(sel'(X, Z)) → a__sel1'(mark'(X), mark'(Z))
a__quote1'(first'(X, Z)) → a__first1'(mark'(X), mark'(Z))
a__unquote'(01') → 0'
a__unquote'(s1'(X)) → s'(a__unquote'(mark'(X)))
a__unquote1'(nil1') → nil'
a__unquote1'(cons1'(X, Z)) → a__fcons'(a__unquote'(mark'(X)), a__unquote1'(mark'(Z)))
a__fcons'(X, Z) → cons'(mark'(X), Z)
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(first'(X1, X2)) → a__first'(mark'(X1), mark'(X2))
mark'(from'(X)) → a__from'(mark'(X))
mark'(sel1'(X1, X2)) → a__sel1'(mark'(X1), mark'(X2))
mark'(quote'(X)) → a__quote'(X)
mark'(first1'(X1, X2)) → a__first1'(mark'(X1), mark'(X2))
mark'(quote1'(X)) → a__quote1'(X)
mark'(unquote'(X)) → a__unquote'(mark'(X))
mark'(unquote1'(X)) → a__unquote1'(mark'(X))
mark'(fcons'(X1, X2)) → a__fcons'(mark'(X1), mark'(X2))
mark'(s'(X)) → s'(mark'(X))
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(0') → 0'
mark'(nil') → nil'
mark'(nil1') → nil1'
mark'(cons1'(X1, X2)) → cons1'(mark'(X1), mark'(X2))
mark'(01') → 01'
mark'(s1'(X)) → s1'(mark'(X))
a__sel'(X1, X2) → sel'(X1, X2)
a__first'(X1, X2) → first'(X1, X2)
a__from'(X) → from'(X)
a__sel1'(X1, X2) → sel1'(X1, X2)
a__quote'(X) → quote'(X)
a__first1'(X1, X2) → first1'(X1, X2)
a__quote1'(X) → quote1'(X)
a__unquote'(X) → unquote'(X)
a__unquote1'(X) → unquote1'(X)
a__fcons'(X1, X2) → fcons'(X1, X2)

Types:
a__sel' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
s' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
cons' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
mark' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
0' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__first' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
nil' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
first' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__from' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
from' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__sel1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__quote' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__first1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
nil1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
cons1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
01' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__quote1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
s1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
sel' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__unquote' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__unquote1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
a__fcons' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
sel1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
quote' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
first1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
quote1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
unquote' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
unquote1' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
fcons' :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons' → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
_hole_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'1 :: s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'
_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2 :: Nat → s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'

Heuristically decided to analyse the following defined symbols:
a__sel', mark', a__from', a__sel1', a__quote', a__first1', a__quote1', a__unquote', a__unquote1', a__fcons'

They will be analysed ascendingly in the following order:
a__sel' = mark'
a__sel' = a__from'
a__sel' = a__sel1'
a__sel' = a__quote'
a__sel' = a__first1'
a__sel' = a__quote1'
a__sel' = a__unquote'
a__sel' = a__unquote1'
a__sel' = a__fcons'
mark' = a__from'
mark' = a__sel1'
mark' = a__quote'
mark' = a__first1'
mark' = a__quote1'
mark' = a__unquote'
mark' = a__unquote1'
mark' = a__fcons'
a__from' = a__sel1'
a__from' = a__quote'
a__from' = a__first1'
a__from' = a__quote1'
a__from' = a__unquote'
a__from' = a__unquote1'
a__from' = a__fcons'
a__sel1' = a__quote'
a__sel1' = a__first1'
a__sel1' = a__quote1'
a__sel1' = a__unquote'
a__sel1' = a__unquote1'
a__sel1' = a__fcons'
a__quote' = a__first1'
a__quote' = a__quote1'
a__quote' = a__unquote'
a__quote' = a__unquote1'
a__quote' = a__fcons'
a__first1' = a__quote1'
a__first1' = a__unquote'
a__first1' = a__unquote1'
a__first1' = a__fcons'
a__quote1' = a__unquote'
a__quote1' = a__unquote1'
a__quote1' = a__fcons'
a__unquote' = a__unquote1'
a__unquote' = a__fcons'
a__unquote1' = a__fcons'

Generator Equations:
_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(0) ⇔ 0'
_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(x, 1)) ⇔ s'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(x))

The following defined symbols remain to be analysed:
mark', a__sel', a__from', a__sel1', a__quote', a__first1', a__quote1', a__unquote', a__unquote1', a__fcons'

Proved the following rewrite lemma:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n4)) → _gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n4), rt ∈ Ω(1 + _n4)

Induction Base:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(0)) →_R^Ω(1)
0'

Induction Step:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(_$n5, 1))) →_R^Ω(1)
s'(mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_$n5))) →_IH
s'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_$n5))

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

The following defined symbols remain to be analysed:
a__sel', a__from', a__sel1', a__quote', a__first1', a__quote1', a__unquote', a__unquote1', a__fcons'

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

The following defined symbols remain to be analysed:
a__from', a__sel1', a__quote', a__first1', a__quote1', a__unquote', a__unquote1', a__fcons'

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

The following defined symbols remain to be analysed:
a__sel1', a__quote', a__first1', a__quote1', a__unquote', a__unquote1', a__fcons'

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

The following defined symbols remain to be analysed:
a__quote', a__first1', a__quote1', a__unquote', a__unquote1', a__fcons'

Proved the following rewrite lemma:
a__quote'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(1, _n8200717))) → _*3, rt ∈ Ω(_n8200717)

Induction Base:
a__quote'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(1, 0)))

Induction Step:
a__quote'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(1, +(_$n8200718, 1)))) →_R^Ω(1)
s1'(a__quote'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(1, _$n8200718)))) →_IH
s1'(_*3)

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

Lemmas:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n4)) → _gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n4), rt ∈ Ω(1 + _n4)
a__quote'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(1, _n8200717))) → _*3, rt ∈ Ω(_n8200717)

The following defined symbols remain to be analysed:
a__first1', a__sel', mark', a__from', a__sel1', a__quote1', a__unquote', a__unquote1', a__fcons'

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

The following defined symbols remain to be analysed:
a__quote1', a__sel', mark', a__from', a__sel1', a__unquote', a__unquote1', a__fcons'

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

The following defined symbols remain to be analysed:
a__unquote', a__sel', mark', a__from', a__sel1', a__unquote1', a__fcons'

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

The following defined symbols remain to be analysed:
a__unquote1', a__sel', mark', a__from', a__sel1', a__fcons'

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

The following defined symbols remain to be analysed:
a__fcons', a__sel', mark', a__from', a__sel1'

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

The following defined symbols remain to be analysed:
mark', a__sel', a__from', a__sel1'

Proved the following rewrite lemma:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n8204014)) → _gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n8204014), rt ∈ Ω(1 + _n8204014)

Induction Base:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(0)) →_R^Ω(1)
0'

Induction Step:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(_$n8204015, 1))) →_R^Ω(1)
s'(mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_$n8204015))) →_IH
s'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_$n8204015))

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

Lemmas:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n8204014)) → _gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n8204014), rt ∈ Ω(1 + _n8204014)
a__quote'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(+(1, _n8200717))) → _*3, rt ∈ Ω(_n8200717)

The following defined symbols remain to be analysed:
a__sel', a__from', a__sel1'

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

The following defined symbols remain to be analysed:
a__from', a__sel1'

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

The following defined symbols remain to be analysed:
a__sel1'

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n8204014)) → _gen_s':cons':0':nil':first':from':nil1':cons1':01':s1':sel':sel1':quote':first1':quote1':unquote':unquote1':fcons'2(_n8204014), rt ∈ Ω(1 + _n8204014)