The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

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

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0) → 01
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

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

sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

(5) OrderProof (LOWER BOUND(ID) transformation)

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

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

(6) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

Induction Base:
sel(gen_s:0'5_0(0), gen_cons:nil6_0(+(1, 0))) →_R^Ω(1)
0'

Induction Step:
sel(gen_s:0'5_0(+(n10_0, 1)), gen_cons:nil6_0(+(1, +(n10_0, 1)))) →_R^Ω(1)
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) →_IH
gen_s:0'5_0(0)

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

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)

Induction Base:
first(gen_s:0'5_0(0), gen_cons:nil6_0(0)) →_R^Ω(1)
nil

Induction Step:
first(gen_s:0'5_0(+(n498_0, 1)), gen_cons:nil6_0(+(n498_0, 1))) →_R^Ω(1)
cons(0', first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0))) →_IH
cons(0', gen_cons:nil6_0(c499_0))

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

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(14) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

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

Proved the following rewrite lemma:
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)

Induction Base:
unquote(gen_01':s17_0(0)) →_R^Ω(1)
0'

Induction Step:
unquote(gen_01':s17_0(+(n1015_0, 1))) →_R^Ω(1)
s(unquote(gen_01':s17_0(n1015_0))) →_IH
s(gen_s:0'5_0(c1016_0))

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

(16) Complex Obligation (BEST)

(17) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)

Induction Base:
unquote1(gen_nil1:cons18_0(0)) →_R^Ω(1)
nil

Induction Step:
unquote1(gen_nil1:cons18_0(+(n1292_0, 1))) →_R^Ω(1)
fcons(unquote(01'), unquote1(gen_nil1:cons18_0(n1292_0))) →_L^Ω(1)
fcons(gen_s:0'5_0(0), unquote1(gen_nil1:cons18_0(n1292_0))) →_IH
fcons(gen_s:0'5_0(0), gen_cons:nil6_0(c1293_0)) →_R^Ω(1)
cons(gen_s:0'5_0(0), gen_cons:nil6_0(n1292_0))

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

(19) Complex Obligation (BEST)

(20) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(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

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quote(gen_s:0'5_0(n1996_0)) → gen_01':s17_0(n1996_0), rt ∈ Ω(1 + n1996₀)

Induction Base:
quote(gen_s:0'5_0(0)) →_R^Ω(1)
01'

Induction Step:
quote(gen_s:0'5_0(+(n1996_0, 1))) →_R^Ω(1)
s1(quote(gen_s:0'5_0(n1996_0))) →_IH
s1(gen_01':s17_0(c1997_0))

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

(22) Complex Obligation (BEST)

(23) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n1996_0)) → gen_01':s17_0(n1996_0), rt ∈ Ω(1 + n1996₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(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

(24) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)

Induction Base:
sel1(gen_s:0'5_0(0), gen_cons:nil6_0(+(1, 0))) →_R^Ω(1)
quote(0') →_L^Ω(1)
gen_01':s17_0(0)

Induction Step:
sel1(gen_s:0'5_0(+(n2449_0, 1)), gen_cons:nil6_0(+(1, +(n2449_0, 1)))) →_R^Ω(1)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) →_IH
gen_01':s17_0(0)

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

(25) Complex Obligation (BEST)

(26) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n1996_0)) → gen_01':s17_0(n1996_0), rt ∈ Ω(1 + n1996₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

(27) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)

Induction Base:
quote(gen_s:0'5_0(0)) →_R^Ω(1)
01'

Induction Step:
quote(gen_s:0'5_0(+(n3020_0, 1))) →_R^Ω(1)
s1(quote(gen_s:0'5_0(n3020_0))) →_IH
s1(gen_01':s17_0(c3021_0))

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

(28) Complex Obligation (BEST)

(29) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

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

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

(30) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0)) → gen_nil1:cons18_0(n3477_0), rt ∈ Ω(1 + n3477₀)

Induction Base:
first1(gen_s:0'5_0(0), gen_cons:nil6_0(0)) →_R^Ω(1)
nil1

Induction Step:
first1(gen_s:0'5_0(+(n3477_0, 1)), gen_cons:nil6_0(+(n3477_0, 1))) →_R^Ω(1)
cons1(quote(0'), first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0))) →_L^Ω(1)
cons1(gen_01':s17_0(0), first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0))) →_IH
cons1(gen_01':s17_0(0), gen_nil1:cons18_0(c3478_0))

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

(31) Complex Obligation (BEST)

(32) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)
first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0)) → gen_nil1:cons18_0(n3477_0), rt ∈ Ω(1 + n3477₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

The following defined symbols remain to be analysed:
quote1

(33) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
quote1(gen_cons:nil6_0(n4221_0)) → gen_nil1:cons18_0(n4221_0), rt ∈ Ω(1 + n4221₀)

Induction Base:
quote1(gen_cons:nil6_0(0)) →_R^Ω(1)
nil1

Induction Step:
quote1(gen_cons:nil6_0(+(n4221_0, 1))) →_R^Ω(1)
cons1(quote(0'), quote1(gen_cons:nil6_0(n4221_0))) →_L^Ω(1)
cons1(gen_01':s17_0(0), quote1(gen_cons:nil6_0(n4221_0))) →_IH
cons1(gen_01':s17_0(0), gen_nil1:cons18_0(c4222_0))

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

(34) Complex Obligation (BEST)

(35) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)
first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0)) → gen_nil1:cons18_0(n3477_0), rt ∈ Ω(1 + n3477₀)
quote1(gen_cons:nil6_0(n4221_0)) → gen_nil1:cons18_0(n4221_0), rt ∈ Ω(1 + n4221₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(37) BOUNDS(n^1, INF)

(38) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)
first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0)) → gen_nil1:cons18_0(n3477_0), rt ∈ Ω(1 + n3477₀)
quote1(gen_cons:nil6_0(n4221_0)) → gen_nil1:cons18_0(n4221_0), rt ∈ Ω(1 + n4221₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(40) BOUNDS(n^1, INF)

(41) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)
first1(gen_s:0'5_0(n3477_0), gen_cons:nil6_0(n3477_0)) → gen_nil1:cons18_0(n3477_0), rt ∈ Ω(1 + n3477₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(42) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(43) BOUNDS(n^1, INF)

(44) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n3020_0)) → gen_01':s17_0(n3020_0), rt ∈ Ω(1 + n3020₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(45) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(46) BOUNDS(n^1, INF)

(47) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n1996_0)) → gen_01':s17_0(n1996_0), rt ∈ Ω(1 + n1996₀)
sel1(gen_s:0'5_0(n2449_0), gen_cons:nil6_0(+(1, n2449_0))) → gen_01':s17_0(0), rt ∈ Ω(1 + n2449₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(48) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(49) BOUNDS(n^1, INF)

(50) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)
quote(gen_s:0'5_0(n1996_0)) → gen_01':s17_0(n1996_0), rt ∈ Ω(1 + n1996₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(51) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(52) BOUNDS(n^1, INF)

(53) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)
unquote1(gen_nil1:cons18_0(n1292_0)) → gen_cons:nil6_0(n1292_0), rt ∈ Ω(1 + n1292₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(54) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(55) BOUNDS(n^1, INF)

(56) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)
unquote(gen_01':s17_0(n1015_0)) → gen_s:0'5_0(n1015_0), rt ∈ Ω(1 + n1015₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(57) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(58) BOUNDS(n^1, INF)

(59) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)
first(gen_s:0'5_0(n498_0), gen_cons:nil6_0(n498_0)) → gen_cons:nil6_0(n498_0), rt ∈ Ω(1 + n498₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(60) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(61) BOUNDS(n^1, INF)

(62) Obligation:

Innermost TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, Z)
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
from(X) → cons(X, from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, Z)
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, Z))
quote(0') → 01'
quote1(cons(X, Z)) → cons1(quote(X), quote1(Z))
quote1(nil) → nil1
quote(s(X)) → s1(quote(X))
quote(sel(X, Z)) → sel1(X, Z)
quote1(first(X, Z)) → first1(X, 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)

Types:
sel :: s:0' → cons:nil → s:0'
s :: s:0' → s:0'
cons :: s:0' → cons:nil → cons:nil
0' :: s:0'
first :: s:0' → cons:nil → cons:nil
nil :: cons:nil
from :: s:0' → cons:nil
sel1 :: s:0' → cons:nil → 01':s1
quote :: s:0' → 01':s1
first1 :: s:0' → cons:nil → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
01' :: 01':s1
quote1 :: cons:nil → nil1:cons1
s1 :: 01':s1 → 01':s1
unquote :: 01':s1 → s:0'
unquote1 :: nil1:cons1 → cons:nil
fcons :: s:0' → cons:nil → cons:nil
hole_s:0'1_0 :: s:0'
hole_cons:nil2_0 :: cons:nil
hole_01':s13_0 :: 01':s1
hole_nil1:cons14_0 :: nil1:cons1
gen_s:0'5_0 :: Nat → s:0'
gen_cons:nil6_0 :: Nat → cons:nil
gen_01':s17_0 :: Nat → 01':s1
gen_nil1:cons18_0 :: Nat → nil1:cons1

Lemmas:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

Generator Equations:
gen_s:0'5_0(0) ⇔ 0'
gen_s:0'5_0(+(x, 1)) ⇔ s(gen_s:0'5_0(x))
gen_cons:nil6_0(0) ⇔ nil
gen_cons:nil6_0(+(x, 1)) ⇔ cons(0', gen_cons:nil6_0(x))
gen_01':s17_0(0) ⇔ 01'
gen_01':s17_0(+(x, 1)) ⇔ s1(gen_01':s17_0(x))
gen_nil1:cons18_0(0) ⇔ nil1
gen_nil1:cons18_0(+(x, 1)) ⇔ cons1(01', gen_nil1:cons18_0(x))

No more defined symbols left to analyse.

(63) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
sel(gen_s:0'5_0(n10_0), gen_cons:nil6_0(+(1, n10_0))) → gen_s:0'5_0(0), rt ∈ Ω(1 + n10₀)

(64) BOUNDS(n^1, INF)