WORST_CASE(Omega(n^1),?)
proof of input_K2hFfSsVBW.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 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), 1 ms]
(8) typed CpxTrs
(9) OrderProof [LOWER BOUND(ID), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 447 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), 51 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 18 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 98 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 374 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 233.2 s]
        (26) BOUNDS(1, INF)


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

(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:

   from(X) -> cons(X, from(s(X)))
   sel(0, cons(X, XS)) -> X
   sel(s(N), cons(X, XS)) -> sel(N, XS)
   minus(X, 0) -> 0
   minus(s(X), s(Y)) -> minus(X, Y)
   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y)))
   zWquot(XS, nil) -> nil
   zWquot(nil, XS) -> nil
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), zWquot(XS, YS))

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:
   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))
Tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
S tuples:
   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
K tuples:none
Defined Rule Symbols:   from_1, sel_2, minus_2, quot_2, zWquot_2

Defined Pair Symbols:   FROM_1, SEL_2, MINUS_2, QUOT_2, ZWQUOT_2

Compound Symbols:   c_1, c1, c2_1, c3, c4_1, c5, c6_2, c7, c8, 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:

   FROM(z0) -> c(FROM(s(z0)))
   SEL(0, cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0) -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0, s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))

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

   from(z0) -> cons(z0, from(s(z0)))
   sel(0, cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0) -> 0
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0, s(z0)) -> 0
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

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:

   FROM(z0) -> c(FROM(s(z0)))
   SEL(0', cons(z0, z1)) -> c1
   SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
   MINUS(z0, 0') -> c3
   MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
   QUOT(0', s(z0)) -> c5
   QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
   ZWQUOT(z0, nil) -> c7
   ZWQUOT(nil, z0) -> c8
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
   ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))

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

   from(z0) -> cons(z0, from(s(z0)))
   sel(0', cons(z0, z1)) -> z0
   sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
   minus(z0, 0') -> 0'
   minus(s(z0), s(z1)) -> minus(z0, z1)
   quot(0', s(z0)) -> 0'
   quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
   zWquot(z0, nil) -> nil
   zWquot(nil, z0) -> nil
   zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
FROM, SEL, MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
QUOT < ZWQUOT
minus < quot
quot < zWquot

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

(10)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
FROM, SEL, MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
QUOT < ZWQUOT
minus < quot
quot < zWquot

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)

Induction Base:
SEL(gen_s:0'9_11(0), gen_cons:nil11_11(+(1, 0))) ->_R^Omega(1)
c1

Induction Step:
SEL(gen_s:0'9_11(+(n165_11, 1)), gen_cons:nil11_11(+(1, +(n165_11, 1)))) ->_R^Omega(1)
c2(SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11)))) ->_IH
c2(gen_c1:c210_11(c166_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:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
SEL, MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
QUOT < ZWQUOT
minus < quot
quot < zWquot

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
MINUS, QUOT, minus, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
MINUS < QUOT
minus < QUOT
QUOT < ZWQUOT
minus < quot
quot < zWquot

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)

Induction Base:
MINUS(gen_s:0'9_11(0), gen_s:0'9_11(0)) ->_R^Omega(1)
c3

Induction Step:
MINUS(gen_s:0'9_11(+(n693_11, 1)), gen_s:0'9_11(+(n693_11, 1))) ->_R^Omega(1)
c4(MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11))) ->_IH
c4(gen_c3:c412_11(c694_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:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
minus, QUOT, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
minus < QUOT
QUOT < ZWQUOT
minus < quot
quot < zWquot

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)

Induction Base:
minus(gen_s:0'9_11(0), gen_s:0'9_11(0)) ->_R^Omega(0)
0'

Induction Step:
minus(gen_s:0'9_11(+(n1270_11, 1)), gen_s:0'9_11(+(n1270_11, 1))) ->_R^Omega(0)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) ->_IH
gen_s:0'9_11(0)

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

(20)
Obligation:
Innermost TRS:
Rules:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
QUOT, ZWQUOT, from, sel, quot, zWquot

They will be analysed ascendingly in the following order:
QUOT < ZWQUOT
quot < zWquot

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11)) -> gen_c7:c8:c9:c1014_11(n2873_11), rt in Omega(1 + n2873_11)

Induction Base:
ZWQUOT(gen_cons:nil11_11(0), gen_cons:nil11_11(0)) ->_R^Omega(1)
c7

Induction Step:
ZWQUOT(gen_cons:nil11_11(+(n2873_11, 1)), gen_cons:nil11_11(+(n2873_11, 1))) ->_R^Omega(1)
c10(ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11))) ->_IH
c10(gen_c7:c8:c9:c1014_11(c2874_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:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)
ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11)) -> gen_c7:c8:c9:c1014_11(n2873_11), rt in Omega(1 + n2873_11)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


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

They will be analysed ascendingly in the following order:
quot < zWquot

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sel(gen_s:0'9_11(n4111_11), gen_cons:nil11_11(+(1, n4111_11))) -> gen_s:0'9_11(0), rt in Omega(0)

Induction Base:
sel(gen_s:0'9_11(0), gen_cons:nil11_11(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
sel(gen_s:0'9_11(+(n4111_11, 1)), gen_cons:nil11_11(+(1, +(n4111_11, 1)))) ->_R^Omega(0)
sel(gen_s:0'9_11(n4111_11), gen_cons:nil11_11(+(1, n4111_11))) ->_IH
gen_s:0'9_11(0)

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:
FROM(z0) -> c(FROM(s(z0)))
SEL(0', cons(z0, z1)) -> c1
SEL(s(z0), cons(z1, z2)) -> c2(SEL(z0, z2))
MINUS(z0, 0') -> c3
MINUS(s(z0), s(z1)) -> c4(MINUS(z0, z1))
QUOT(0', s(z0)) -> c5
QUOT(s(z0), s(z1)) -> c6(QUOT(minus(z0, z1), s(z1)), MINUS(z0, z1))
ZWQUOT(z0, nil) -> c7
ZWQUOT(nil, z0) -> c8
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c9(QUOT(z0, z2))
ZWQUOT(cons(z0, z1), cons(z2, z3)) -> c10(ZWQUOT(z1, z3))
from(z0) -> cons(z0, from(s(z0)))
sel(0', cons(z0, z1)) -> z0
sel(s(z0), cons(z1, z2)) -> sel(z0, z2)
minus(z0, 0') -> 0'
minus(s(z0), s(z1)) -> minus(z0, z1)
quot(0', s(z0)) -> 0'
quot(s(z0), s(z1)) -> s(quot(minus(z0, z1), s(z1)))
zWquot(z0, nil) -> nil
zWquot(nil, z0) -> nil
zWquot(cons(z0, z1), cons(z2, z3)) -> cons(quot(z0, z2), zWquot(z1, z3))

Types:
FROM :: s:0' -> c
c :: c -> c
s :: s:0' -> s:0'
SEL :: s:0' -> cons:nil -> c1:c2
0' :: s:0'
cons :: s:0' -> cons:nil -> cons:nil
c1 :: c1:c2
c2 :: c1:c2 -> c1:c2
MINUS :: s:0' -> s:0' -> c3:c4
c3 :: c3:c4
c4 :: c3:c4 -> c3:c4
QUOT :: s:0' -> s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c3:c4 -> c5:c6
minus :: s:0' -> s:0' -> s:0'
ZWQUOT :: cons:nil -> cons:nil -> c7:c8:c9:c10
nil :: cons:nil
c7 :: c7:c8:c9:c10
c8 :: c7:c8:c9:c10
c9 :: c5:c6 -> c7:c8:c9:c10
c10 :: c7:c8:c9:c10 -> c7:c8:c9:c10
from :: s:0' -> cons:nil
sel :: s:0' -> cons:nil -> s:0'
quot :: s:0' -> s:0' -> s:0'
zWquot :: cons:nil -> cons:nil -> cons:nil
hole_c1_11 :: c
hole_s:0'2_11 :: s:0'
hole_c1:c23_11 :: c1:c2
hole_cons:nil4_11 :: cons:nil
hole_c3:c45_11 :: c3:c4
hole_c5:c66_11 :: c5:c6
hole_c7:c8:c9:c107_11 :: c7:c8:c9:c10
gen_c8_11 :: Nat -> c
gen_s:0'9_11 :: Nat -> s:0'
gen_c1:c210_11 :: Nat -> c1:c2
gen_cons:nil11_11 :: Nat -> cons:nil
gen_c3:c412_11 :: Nat -> c3:c4
gen_c5:c613_11 :: Nat -> c5:c6
gen_c7:c8:c9:c1014_11 :: Nat -> c7:c8:c9:c10


Lemmas:
SEL(gen_s:0'9_11(n165_11), gen_cons:nil11_11(+(1, n165_11))) -> gen_c1:c210_11(n165_11), rt in Omega(1 + n165_11)
MINUS(gen_s:0'9_11(n693_11), gen_s:0'9_11(n693_11)) -> gen_c3:c412_11(n693_11), rt in Omega(1 + n693_11)
minus(gen_s:0'9_11(n1270_11), gen_s:0'9_11(n1270_11)) -> gen_s:0'9_11(0), rt in Omega(0)
ZWQUOT(gen_cons:nil11_11(n2873_11), gen_cons:nil11_11(n2873_11)) -> gen_c7:c8:c9:c1014_11(n2873_11), rt in Omega(1 + n2873_11)
sel(gen_s:0'9_11(n4111_11), gen_cons:nil11_11(+(1, n4111_11))) -> gen_s:0'9_11(0), rt in Omega(0)


Generator Equations:
gen_c8_11(0) <=> hole_c1_11
gen_c8_11(+(x, 1)) <=> c(gen_c8_11(x))
gen_s:0'9_11(0) <=> 0'
gen_s:0'9_11(+(x, 1)) <=> s(gen_s:0'9_11(x))
gen_c1:c210_11(0) <=> c1
gen_c1:c210_11(+(x, 1)) <=> c2(gen_c1:c210_11(x))
gen_cons:nil11_11(0) <=> nil
gen_cons:nil11_11(+(x, 1)) <=> cons(0', gen_cons:nil11_11(x))
gen_c3:c412_11(0) <=> c3
gen_c3:c412_11(+(x, 1)) <=> c4(gen_c3:c412_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x), c3)
gen_c7:c8:c9:c1014_11(0) <=> c7
gen_c7:c8:c9:c1014_11(+(x, 1)) <=> c10(gen_c7:c8:c9:c1014_11(x))


The following defined symbols remain to be analysed:
quot, zWquot

They will be analysed ascendingly in the following order:
quot < zWquot

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
zWquot(gen_cons:nil11_11(+(1, n5050_11)), gen_cons:nil11_11(+(1, n5050_11))) -> *15_11, rt in Omega(0)

Induction Base:
zWquot(gen_cons:nil11_11(+(1, 0)), gen_cons:nil11_11(+(1, 0)))

Induction Step:
zWquot(gen_cons:nil11_11(+(1, +(n5050_11, 1))), gen_cons:nil11_11(+(1, +(n5050_11, 1)))) ->_R^Omega(0)
cons(quot(0', 0'), zWquot(gen_cons:nil11_11(+(1, n5050_11)), gen_cons:nil11_11(+(1, n5050_11)))) ->_IH
cons(quot(0', 0'), *15_11)

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

(26)
BOUNDS(1, INF)