WORST_CASE(Omega(n^1),?)
proof of input_PfYPfzfzZg.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(2) CdtProblem
(3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 1 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 317 ms]
(12) BEST
    (13) proven lower bound
        (14) LowerBoundPropagationProof [FINISHED, 0 ms]
        (15) BOUNDS(n^1, INF)
    (16) typed CpxTrs
        (17) RewriteLemmaProof [LOWER BOUND(ID), 97 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 53 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 90 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 125 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 37 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 0 ms]
        (28) typed CpxTrs
        (29) RewriteLemmaProof [LOWER BOUND(ID), 13 ms]
        (30) typed CpxTrs


----------------------------------------

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


The TRS R consists of the following rules:

   dbl(0) -> 0
   dbl(s(X)) -> s(s(dbl(X)))
   dbls(nil) -> nil
   dbls(cons(X, Y)) -> cons(dbl(X), dbls(Y))
   sel(0, cons(X, Y)) -> X
   sel(s(X), cons(Y, Z)) -> sel(X, Z)
   indx(nil, X) -> nil
   indx(cons(X, Y), Z) -> cons(sel(X, Z), indx(Y, Z))
   from(X) -> cons(X, from(s(X)))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   dbls(nil) -> nil
   dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   indx(nil, z0) -> nil
   indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
   from(z0) -> cons(z0, from(s(z0)))
Tuples:
   DBL(0) -> c
   DBL(s(z0)) -> c1(DBL(z0))
   DBLS(nil) -> c2
   DBLS(cons(z0, z1)) -> c3(DBL(z0))
   DBLS(cons(z0, z1)) -> c4(DBLS(z1))
   SEL(0, cons(z0, z1)) -> c5
   SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
   INDX(nil, z0) -> c7
   INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
   INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
   FROM(z0) -> c10(FROM(s(z0)))
S tuples:
   DBL(0) -> c
   DBL(s(z0)) -> c1(DBL(z0))
   DBLS(nil) -> c2
   DBLS(cons(z0, z1)) -> c3(DBL(z0))
   DBLS(cons(z0, z1)) -> c4(DBLS(z1))
   SEL(0, cons(z0, z1)) -> c5
   SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
   INDX(nil, z0) -> c7
   INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
   INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
   FROM(z0) -> c10(FROM(s(z0)))
K tuples:none
Defined Rule Symbols:   dbl_1, dbls_1, sel_2, indx_2, from_1

Defined Pair Symbols:   DBL_1, DBLS_1, SEL_2, INDX_2, FROM_1

Compound Symbols:   c, c1_1, c2, c3_1, c4_1, c5, c6_1, c7, c8_1, c9_1, c10_1


----------------------------------------

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

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


The TRS R consists of the following rules:

   DBL(0) -> c
   DBL(s(z0)) -> c1(DBL(z0))
   DBLS(nil) -> c2
   DBLS(cons(z0, z1)) -> c3(DBL(z0))
   DBLS(cons(z0, z1)) -> c4(DBLS(z1))
   SEL(0, cons(z0, z1)) -> c5
   SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
   INDX(nil, z0) -> c7
   INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
   INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
   FROM(z0) -> c10(FROM(s(z0)))

The (relative) TRS S consists of the following rules:

   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   dbls(nil) -> nil
   dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   indx(nil, z0) -> nil
   indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
   from(z0) -> cons(z0, from(s(z0)))

Rewrite Strategy: INNERMOST
----------------------------------------

(5) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   DBL(0') -> c
   DBL(s(z0)) -> c1(DBL(z0))
   DBLS(nil) -> c2
   DBLS(cons(z0, z1)) -> c3(DBL(z0))
   DBLS(cons(z0, z1)) -> c4(DBLS(z1))
   SEL(0', cons(z0, z1)) -> c5
   SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
   INDX(nil, z0) -> c7
   INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
   INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
   FROM(z0) -> c10(FROM(s(z0)))

The (relative) TRS S consists of the following rules:

   dbl(0') -> 0'
   dbl(s(z0)) -> s(s(dbl(z0)))
   dbls(nil) -> nil
   dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
   sel(0', cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   indx(nil, z0) -> nil
   indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
   from(z0) -> cons(z0, from(s(z0)))

Rewrite Strategy: INNERMOST
----------------------------------------

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(8)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10

----------------------------------------

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
DBL, DBLS, SEL, INDX, FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
DBL < DBLS
SEL < INDX
dbl < dbls
sel < indx

----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
DBL, DBLS, SEL, INDX, FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
DBL < DBLS
SEL < INDX
dbl < dbls
sel < indx

----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)

Induction Base:
DBL(gen_0':s9_11(0)) ->_R^Omega(1)
c

Induction Step:
DBL(gen_0':s9_11(+(n16_11, 1))) ->_R^Omega(1)
c1(DBL(gen_0':s9_11(n16_11))) ->_IH
c1(gen_c:c18_11(c17_11))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(12)
Complex Obligation (BEST)

----------------------------------------

(13)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
DBL, DBLS, SEL, INDX, FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
DBL < DBLS
SEL < INDX
dbl < dbls
sel < indx

----------------------------------------

(14) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(15)
BOUNDS(n^1, INF)

----------------------------------------

(16)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
DBLS, SEL, INDX, FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
SEL < INDX
dbl < dbls
sel < indx

----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)

Induction Base:
DBLS(gen_nil:cons11_11(0)) ->_R^Omega(1)
c2

Induction Step:
DBLS(gen_nil:cons11_11(+(n304_11, 1))) ->_R^Omega(1)
c4(DBLS(gen_nil:cons11_11(n304_11))) ->_IH
c4(gen_c2:c3:c410_11(c305_11))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(18)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
SEL, INDX, FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
SEL < INDX
dbl < dbls
sel < indx

----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)

Induction Base:
SEL(gen_0':s9_11(0), gen_nil:cons11_11(+(1, 0))) ->_R^Omega(1)
c5

Induction Step:
SEL(gen_0':s9_11(+(n826_11, 1)), gen_nil:cons11_11(+(1, +(n826_11, 1)))) ->_R^Omega(1)
c6(SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11)))) ->_IH
c6(gen_c5:c612_11(c827_11))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
INDX, FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
dbl < dbls
sel < indx

----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b)) -> gen_c7:c8:c913_11(n1426_11), rt in Omega(1 + n1426_11)

Induction Base:
INDX(gen_nil:cons11_11(0), gen_nil:cons11_11(b)) ->_R^Omega(1)
c7

Induction Step:
INDX(gen_nil:cons11_11(+(n1426_11, 1)), gen_nil:cons11_11(b)) ->_R^Omega(1)
c9(INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b))) ->_IH
c9(gen_c7:c8:c913_11(c1427_11))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)
INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b)) -> gen_c7:c8:c913_11(n1426_11), rt in Omega(1 + n1426_11)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
FROM, dbl, dbls, sel, indx, from

They will be analysed ascendingly in the following order:
dbl < dbls
sel < indx

----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
dbl(gen_0':s9_11(n2735_11)) -> gen_0':s9_11(*(2, n2735_11)), rt in Omega(0)

Induction Base:
dbl(gen_0':s9_11(0)) ->_R^Omega(0)
0'

Induction Step:
dbl(gen_0':s9_11(+(n2735_11, 1))) ->_R^Omega(0)
s(s(dbl(gen_0':s9_11(n2735_11)))) ->_IH
s(s(gen_0':s9_11(*(2, c2736_11))))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(24)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)
INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b)) -> gen_c7:c8:c913_11(n1426_11), rt in Omega(1 + n1426_11)
dbl(gen_0':s9_11(n2735_11)) -> gen_0':s9_11(*(2, n2735_11)), rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
dbls, sel, indx, from

They will be analysed ascendingly in the following order:
sel < indx

----------------------------------------

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
dbls(gen_nil:cons11_11(n3133_11)) -> gen_nil:cons11_11(n3133_11), rt in Omega(0)

Induction Base:
dbls(gen_nil:cons11_11(0)) ->_R^Omega(0)
nil

Induction Step:
dbls(gen_nil:cons11_11(+(n3133_11, 1))) ->_R^Omega(0)
cons(dbl(0'), dbls(gen_nil:cons11_11(n3133_11))) ->_L^Omega(0)
cons(gen_0':s9_11(*(2, 0)), dbls(gen_nil:cons11_11(n3133_11))) ->_IH
cons(gen_0':s9_11(0), gen_nil:cons11_11(c3134_11))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(26)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)
INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b)) -> gen_c7:c8:c913_11(n1426_11), rt in Omega(1 + n1426_11)
dbl(gen_0':s9_11(n2735_11)) -> gen_0':s9_11(*(2, n2735_11)), rt in Omega(0)
dbls(gen_nil:cons11_11(n3133_11)) -> gen_nil:cons11_11(n3133_11), rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
sel, indx, from

They will be analysed ascendingly in the following order:
sel < indx

----------------------------------------

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sel(gen_0':s9_11(n3658_11), gen_nil:cons11_11(+(1, n3658_11))) -> gen_0':s9_11(0), rt in Omega(0)

Induction Base:
sel(gen_0':s9_11(0), gen_nil:cons11_11(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
sel(gen_0':s9_11(+(n3658_11, 1)), gen_nil:cons11_11(+(1, +(n3658_11, 1)))) ->_R^Omega(0)
sel(gen_0':s9_11(n3658_11), gen_nil:cons11_11(+(1, n3658_11))) ->_IH
gen_0':s9_11(0)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(28)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)
INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b)) -> gen_c7:c8:c913_11(n1426_11), rt in Omega(1 + n1426_11)
dbl(gen_0':s9_11(n2735_11)) -> gen_0':s9_11(*(2, n2735_11)), rt in Omega(0)
dbls(gen_nil:cons11_11(n3133_11)) -> gen_nil:cons11_11(n3133_11), rt in Omega(0)
sel(gen_0':s9_11(n3658_11), gen_nil:cons11_11(+(1, n3658_11))) -> gen_0':s9_11(0), rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
indx, from
----------------------------------------

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
indx(gen_nil:cons11_11(n4299_11), gen_nil:cons11_11(1)) -> gen_nil:cons11_11(n4299_11), rt in Omega(0)

Induction Base:
indx(gen_nil:cons11_11(0), gen_nil:cons11_11(1)) ->_R^Omega(0)
nil

Induction Step:
indx(gen_nil:cons11_11(+(n4299_11, 1)), gen_nil:cons11_11(1)) ->_R^Omega(0)
cons(sel(0', gen_nil:cons11_11(1)), indx(gen_nil:cons11_11(n4299_11), gen_nil:cons11_11(1))) ->_L^Omega(0)
cons(gen_0':s9_11(0), indx(gen_nil:cons11_11(n4299_11), gen_nil:cons11_11(1))) ->_IH
cons(gen_0':s9_11(0), gen_nil:cons11_11(c4300_11))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(30)
Obligation:
Innermost TRS:
Rules:
DBL(0') -> c
DBL(s(z0)) -> c1(DBL(z0))
DBLS(nil) -> c2
DBLS(cons(z0, z1)) -> c3(DBL(z0))
DBLS(cons(z0, z1)) -> c4(DBLS(z1))
SEL(0', cons(z0, z1)) -> c5
SEL(s(z0), cons(z1, z2)) -> c6(SEL(z0, z2))
INDX(nil, z0) -> c7
INDX(cons(z0, z1), z2) -> c8(SEL(z0, z2))
INDX(cons(z0, z1), z2) -> c9(INDX(z1, z2))
FROM(z0) -> c10(FROM(s(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
dbls(nil) -> nil
dbls(cons(z0, z1)) -> cons(dbl(z0), dbls(z1))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
indx(nil, z0) -> nil
indx(cons(z0, z1), z2) -> cons(sel(z0, z2), indx(z1, z2))
from(z0) -> cons(z0, from(s(z0)))

Types:
DBL :: 0':s -> c:c1
0' :: 0':s
c :: c:c1
s :: 0':s -> 0':s
c1 :: c:c1 -> c:c1
DBLS :: nil:cons -> c2:c3:c4
nil :: nil:cons
c2 :: c2:c3:c4
cons :: 0':s -> nil:cons -> nil:cons
c3 :: c:c1 -> c2:c3:c4
c4 :: c2:c3:c4 -> c2:c3:c4
SEL :: 0':s -> nil:cons -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
INDX :: nil:cons -> nil:cons -> c7:c8:c9
c7 :: c7:c8:c9
c8 :: c5:c6 -> c7:c8:c9
c9 :: c7:c8:c9 -> c7:c8:c9
FROM :: 0':s -> c10
c10 :: c10 -> c10
dbl :: 0':s -> 0':s
dbls :: nil:cons -> nil:cons
sel :: 0':s -> nil:cons -> 0':s
indx :: nil:cons -> nil:cons -> nil:cons
from :: 0':s -> nil:cons
hole_c:c11_11 :: c:c1
hole_0':s2_11 :: 0':s
hole_c2:c3:c43_11 :: c2:c3:c4
hole_nil:cons4_11 :: nil:cons
hole_c5:c65_11 :: c5:c6
hole_c7:c8:c96_11 :: c7:c8:c9
hole_c107_11 :: c10
gen_c:c18_11 :: Nat -> c:c1
gen_0':s9_11 :: Nat -> 0':s
gen_c2:c3:c410_11 :: Nat -> c2:c3:c4
gen_nil:cons11_11 :: Nat -> nil:cons
gen_c5:c612_11 :: Nat -> c5:c6
gen_c7:c8:c913_11 :: Nat -> c7:c8:c9
gen_c1014_11 :: Nat -> c10


Lemmas:
DBL(gen_0':s9_11(n16_11)) -> gen_c:c18_11(n16_11), rt in Omega(1 + n16_11)
DBLS(gen_nil:cons11_11(n304_11)) -> gen_c2:c3:c410_11(n304_11), rt in Omega(1 + n304_11)
SEL(gen_0':s9_11(n826_11), gen_nil:cons11_11(+(1, n826_11))) -> gen_c5:c612_11(n826_11), rt in Omega(1 + n826_11)
INDX(gen_nil:cons11_11(n1426_11), gen_nil:cons11_11(b)) -> gen_c7:c8:c913_11(n1426_11), rt in Omega(1 + n1426_11)
dbl(gen_0':s9_11(n2735_11)) -> gen_0':s9_11(*(2, n2735_11)), rt in Omega(0)
dbls(gen_nil:cons11_11(n3133_11)) -> gen_nil:cons11_11(n3133_11), rt in Omega(0)
sel(gen_0':s9_11(n3658_11), gen_nil:cons11_11(+(1, n3658_11))) -> gen_0':s9_11(0), rt in Omega(0)
indx(gen_nil:cons11_11(n4299_11), gen_nil:cons11_11(1)) -> gen_nil:cons11_11(n4299_11), rt in Omega(0)


Generator Equations:
gen_c:c18_11(0) <=> c
gen_c:c18_11(+(x, 1)) <=> c1(gen_c:c18_11(x))
gen_0':s9_11(0) <=> 0'
gen_0':s9_11(+(x, 1)) <=> s(gen_0':s9_11(x))
gen_c2:c3:c410_11(0) <=> c2
gen_c2:c3:c410_11(+(x, 1)) <=> c4(gen_c2:c3:c410_11(x))
gen_nil:cons11_11(0) <=> nil
gen_nil:cons11_11(+(x, 1)) <=> cons(0', gen_nil:cons11_11(x))
gen_c5:c612_11(0) <=> c5
gen_c5:c612_11(+(x, 1)) <=> c6(gen_c5:c612_11(x))
gen_c7:c8:c913_11(0) <=> c7
gen_c7:c8:c913_11(+(x, 1)) <=> c9(gen_c7:c8:c913_11(x))
gen_c1014_11(0) <=> hole_c107_11
gen_c1014_11(+(x, 1)) <=> c10(gen_c1014_11(x))


The following defined symbols remain to be analysed:
from