### (0) Obligation:

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

sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Rewrite Strategy: FULL

### (1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
activate(n__first(n__from(X62970_3), X2)) →+ first(cons(activate(X62970_3), n__from(n__s(activate(X62970_3)))), activate(X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0].
The pumping substitution is [X62970_3 / n__first(n__from(X62970_3), X2)].
The result substitution is [ ].

The rewrite sequence
activate(n__first(n__from(X62970_3), X2)) →+ first(cons(activate(X62970_3), n__from(n__s(activate(X62970_3)))), activate(X2))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0].
The pumping substitution is [X62970_3 / n__first(n__from(X62970_3), X2)].
The result substitution is [ ].

### (3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

### (4) Obligation:

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

sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

S is empty.
Rewrite Strategy: FULL

Infered types.

### (6) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

### (7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
sel, activate, sel1, quote, first1, quote1, unquote, unquote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

### (8) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
unquote, sel, activate, sel1, quote, first1, quote1, unquote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

### (9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)

Induction Base:
unquote(gen_01':s15_3(+(1, 0)))

Induction Step:
unquote(gen_01':s15_3(+(1, +(n8_3, 1)))) →RΩ(1)
s(unquote(gen_01':s15_3(+(1, n8_3)))) →IH
s(*7_3)

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

### (11) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
unquote1, sel, activate, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

### (12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)

Induction Base:
unquote1(gen_nil1:cons16_3(0))

Induction Step:
unquote1(gen_nil1:cons16_3(+(n1023_3, 1))) →RΩ(1)
fcons(unquote(01'), unquote1(gen_nil1:cons16_3(n1023_3))) →RΩ(1)
fcons(0', unquote1(gen_nil1:cons16_3(n1023_3))) →RΩ(1)
fcons(n__0, unquote1(gen_nil1:cons16_3(n1023_3))) →IH
fcons(n__0, *7_3)

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

### (14) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
activate, sel, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

### (15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Induction Base:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0)) →RΩ(1)
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0)

Induction Step:
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(n8099_3, 1))) →RΩ(1)
first(activate(n__0), activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3))) →RΩ(1)
first(n__0, activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3))) →IH
first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(c8100_3)) →RΩ(1)
n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3))

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

### (17) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
sel, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

### (18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol sel.

### (19) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
quote, sel1, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

### (20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol quote.

### (21) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
sel1, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

### (22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol sel1.

### (23) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
first1, quote1

They will be analysed ascendingly in the following order:
first1 < quote1

### (24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol first1.

### (25) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
quote1

### (26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol quote1.

### (27) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

### (28) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)

### (30) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)
activate(gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3)) → gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(n8099_3), rt ∈ Ω(1 + n80993)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

### (31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)

### (33) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n10233)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

### (34) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)

### (36) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(n__s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
s(X) → n__s(X)
0'n__0
cons(X1, X2) → n__cons(X1, X2)
niln__nil
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(activate(X1), activate(X2))
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__nil) → nil
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(X) → X

Types:
sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
activate :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
0' :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__first :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__from :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__s :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
sel1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
quote :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → 01':s1
first1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
01' :: 01':s1
quote1 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → nil1:cons1
n__cons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
n__nil :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote :: 01':s1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
unquote1 :: nil1:cons1 → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
fcons :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel1_3 :: n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3 :: Nat → n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)

Generator Equations:
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(0) ⇔ n__0
gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__s:n__from:n__0:n__cons:n__nil:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

### (37) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n83)