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


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^3, 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), 10 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 272 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), 100 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 41 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 83 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 60 ms]
        (24) typed CpxTrs
        (25) RewriteLemmaProof [LOWER BOUND(ID), 133 ms]
        (26) typed CpxTrs
        (27) RewriteLemmaProof [LOWER BOUND(ID), 611 ms]
        (28) BEST
            (29) proven lower bound
                (30) LowerBoundPropagationProof [FINISHED, 0 ms]
                (31) BOUNDS(n^3, INF)
            (32) typed CpxTrs
                (33) RewriteLemmaProof [LOWER BOUND(ID), 944 ms]
                (34) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   terms(N) -> cons(recip(sqr(N)), terms(s(N)))
   sqr(0) -> 0
   sqr(s(X)) -> s(add(sqr(X), dbl(X)))
   dbl(0) -> 0
   dbl(s(X)) -> s(s(dbl(X)))
   add(0, X) -> X
   add(s(X), Y) -> s(add(X, Y))
   first(0, X) -> nil
   first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z))

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:
   terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   first(0, z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))
Tuples:
   TERMS(z0) -> c(SQR(z0))
   TERMS(z0) -> c1(TERMS(s(z0)))
   SQR(0) -> c2
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c5
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(0, z0) -> c7
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(0, z0) -> c9
   FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
S tuples:
   TERMS(z0) -> c(SQR(z0))
   TERMS(z0) -> c1(TERMS(s(z0)))
   SQR(0) -> c2
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c5
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(0, z0) -> c7
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(0, z0) -> c9
   FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
K tuples:none
Defined Rule Symbols:   terms_1, sqr_1, dbl_1, add_2, first_2

Defined Pair Symbols:   TERMS_1, SQR_1, DBL_1, ADD_2, FIRST_2

Compound Symbols:   c_1, c1_1, c2, c3_2, c4_2, c5, c6_1, c7, c8_1, c9, 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^3, INF).


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0))
   TERMS(z0) -> c1(TERMS(s(z0)))
   SQR(0) -> c2
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0) -> c5
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(0, z0) -> c7
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(0, z0) -> c9
   FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))

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

   terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
   sqr(0) -> 0
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   dbl(0) -> 0
   dbl(s(z0)) -> s(s(dbl(z0)))
   add(0, z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   first(0, z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

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^3, INF).


The TRS R consists of the following rules:

   TERMS(z0) -> c(SQR(z0))
   TERMS(z0) -> c1(TERMS(s(z0)))
   SQR(0') -> c2
   SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
   SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
   DBL(0') -> c5
   DBL(s(z0)) -> c6(DBL(z0))
   ADD(0', z0) -> c7
   ADD(s(z0), z1) -> c8(ADD(z0, z1))
   FIRST(0', z0) -> c9
   FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))

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

   terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
   sqr(0') -> 0'
   sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
   dbl(0') -> 0'
   dbl(s(z0)) -> s(s(dbl(z0)))
   add(0', z0) -> z0
   add(s(z0), z1) -> s(add(z0, z1))
   first(0', z0) -> nil
   first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
TERMS, SQR, ADD, sqr, dbl, DBL, FIRST, terms, add, first

They will be analysed ascendingly in the following order:
SQR < TERMS
ADD < SQR
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
sqr < terms
add < sqr

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

(10)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
ADD, TERMS, SQR, sqr, dbl, DBL, FIRST, terms, add, first

They will be analysed ascendingly in the following order:
SQR < TERMS
ADD < SQR
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
sqr < terms
add < sqr

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)

Induction Base:
ADD(gen_s:0'10_11(0), gen_s:0'10_11(b)) ->_R^Omega(1)
c7

Induction Step:
ADD(gen_s:0'10_11(+(n17_11, 1)), gen_s:0'10_11(b)) ->_R^Omega(1)
c8(ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b))) ->_IH
c8(gen_c7:c812_11(c18_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:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
ADD, TERMS, SQR, sqr, dbl, DBL, FIRST, terms, add, first

They will be analysed ascendingly in the following order:
SQR < TERMS
ADD < SQR
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
sqr < terms
add < sqr

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
dbl, TERMS, SQR, sqr, DBL, FIRST, terms, add, first

They will be analysed ascendingly in the following order:
SQR < TERMS
sqr < SQR
dbl < SQR
DBL < SQR
dbl < sqr
sqr < terms
add < sqr

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)

Induction Base:
dbl(gen_s:0'10_11(0)) ->_R^Omega(0)
0'

Induction Step:
dbl(gen_s:0'10_11(+(n700_11, 1))) ->_R^Omega(0)
s(s(dbl(gen_s:0'10_11(n700_11)))) ->_IH
s(s(gen_s:0'10_11(*(2, c701_11))))

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

(18)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
DBL, TERMS, SQR, sqr, FIRST, terms, add, first

They will be analysed ascendingly in the following order:
SQR < TERMS
sqr < SQR
DBL < SQR
sqr < terms
add < sqr

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)

Induction Base:
DBL(gen_s:0'10_11(0)) ->_R^Omega(1)
c5

Induction Step:
DBL(gen_s:0'10_11(+(n1094_11, 1))) ->_R^Omega(1)
c6(DBL(gen_s:0'10_11(n1094_11))) ->_IH
c6(gen_c5:c613_11(c1095_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:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
FIRST, TERMS, SQR, sqr, terms, add, first

They will be analysed ascendingly in the following order:
SQR < TERMS
sqr < SQR
sqr < terms
add < sqr

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11)) -> gen_c9:c1014_11(n1532_11), rt in Omega(1 + n1532_11)

Induction Base:
FIRST(gen_s:0'10_11(0), gen_cons:nil15_11(0)) ->_R^Omega(1)
c9

Induction Step:
FIRST(gen_s:0'10_11(+(n1532_11, 1)), gen_cons:nil15_11(+(n1532_11, 1))) ->_R^Omega(1)
c10(FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11))) ->_IH
c10(gen_c9:c1014_11(c1533_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:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)
FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11)) -> gen_c9:c1014_11(n1532_11), rt in Omega(1 + n1532_11)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
add, TERMS, SQR, sqr, terms, first

They will be analysed ascendingly in the following order:
SQR < TERMS
sqr < SQR
sqr < terms
add < sqr

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
add(gen_s:0'10_11(n2159_11), gen_s:0'10_11(b)) -> gen_s:0'10_11(+(n2159_11, b)), rt in Omega(0)

Induction Base:
add(gen_s:0'10_11(0), gen_s:0'10_11(b)) ->_R^Omega(0)
gen_s:0'10_11(b)

Induction Step:
add(gen_s:0'10_11(+(n2159_11, 1)), gen_s:0'10_11(b)) ->_R^Omega(0)
s(add(gen_s:0'10_11(n2159_11), gen_s:0'10_11(b))) ->_IH
s(gen_s:0'10_11(+(b, c2160_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:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)
FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11)) -> gen_c9:c1014_11(n1532_11), rt in Omega(1 + n1532_11)
add(gen_s:0'10_11(n2159_11), gen_s:0'10_11(b)) -> gen_s:0'10_11(+(n2159_11, b)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
sqr, TERMS, SQR, terms, first

They will be analysed ascendingly in the following order:
SQR < TERMS
sqr < SQR
sqr < terms

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

(25) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sqr(gen_s:0'10_11(n3678_11)) -> gen_s:0'10_11(*(n3678_11, n3678_11)), rt in Omega(0)

Induction Base:
sqr(gen_s:0'10_11(0)) ->_R^Omega(0)
0'

Induction Step:
sqr(gen_s:0'10_11(+(n3678_11, 1))) ->_R^Omega(0)
s(add(sqr(gen_s:0'10_11(n3678_11)), dbl(gen_s:0'10_11(n3678_11)))) ->_IH
s(add(gen_s:0'10_11(*(c3679_11, c3679_11)), dbl(gen_s:0'10_11(n3678_11)))) ->_L^Omega(0)
s(add(gen_s:0'10_11(*(n3678_11, n3678_11)), gen_s:0'10_11(*(2, n3678_11)))) ->_L^Omega(0)
s(gen_s:0'10_11(+(*(n3678_11, n3678_11), *(2, n3678_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:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)
FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11)) -> gen_c9:c1014_11(n1532_11), rt in Omega(1 + n1532_11)
add(gen_s:0'10_11(n2159_11), gen_s:0'10_11(b)) -> gen_s:0'10_11(+(n2159_11, b)), rt in Omega(0)
sqr(gen_s:0'10_11(n3678_11)) -> gen_s:0'10_11(*(n3678_11, n3678_11)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
SQR, TERMS, terms, first

They will be analysed ascendingly in the following order:
SQR < TERMS

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SQR(gen_s:0'10_11(n4209_11)) -> *16_11, rt in Omega(n4209_11 + n4209_11^3)

Induction Base:
SQR(gen_s:0'10_11(0))

Induction Step:
SQR(gen_s:0'10_11(+(n4209_11, 1))) ->_R^Omega(1)
c3(ADD(sqr(gen_s:0'10_11(n4209_11)), dbl(gen_s:0'10_11(n4209_11))), SQR(gen_s:0'10_11(n4209_11))) ->_L^Omega(0)
c3(ADD(gen_s:0'10_11(*(n4209_11, n4209_11)), dbl(gen_s:0'10_11(n4209_11))), SQR(gen_s:0'10_11(n4209_11))) ->_L^Omega(0)
c3(ADD(gen_s:0'10_11(*(n4209_11, n4209_11)), gen_s:0'10_11(*(2, n4209_11))), SQR(gen_s:0'10_11(n4209_11))) ->_L^Omega(1 + n4209_11^2)
c3(gen_c7:c812_11(*(n4209_11, n4209_11)), SQR(gen_s:0'10_11(n4209_11))) ->_IH
c3(gen_c7:c812_11(*(n4209_11, n4209_11)), *16_11)

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

(28)
Complex Obligation (BEST)

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

(29)
Obligation:
Proved the lower bound n^3 for the following obligation:

Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)
FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11)) -> gen_c9:c1014_11(n1532_11), rt in Omega(1 + n1532_11)
add(gen_s:0'10_11(n2159_11), gen_s:0'10_11(b)) -> gen_s:0'10_11(+(n2159_11, b)), rt in Omega(0)
sqr(gen_s:0'10_11(n3678_11)) -> gen_s:0'10_11(*(n3678_11, n3678_11)), rt in Omega(0)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
SQR, TERMS, terms, first

They will be analysed ascendingly in the following order:
SQR < TERMS

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

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

(31)
BOUNDS(n^3, INF)

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

(32)
Obligation:
Innermost TRS:
Rules:
TERMS(z0) -> c(SQR(z0))
TERMS(z0) -> c1(TERMS(s(z0)))
SQR(0') -> c2
SQR(s(z0)) -> c3(ADD(sqr(z0), dbl(z0)), SQR(z0))
SQR(s(z0)) -> c4(ADD(sqr(z0), dbl(z0)), DBL(z0))
DBL(0') -> c5
DBL(s(z0)) -> c6(DBL(z0))
ADD(0', z0) -> c7
ADD(s(z0), z1) -> c8(ADD(z0, z1))
FIRST(0', z0) -> c9
FIRST(s(z0), cons(z1, z2)) -> c10(FIRST(z0, z2))
terms(z0) -> cons(recip(sqr(z0)), terms(s(z0)))
sqr(0') -> 0'
sqr(s(z0)) -> s(add(sqr(z0), dbl(z0)))
dbl(0') -> 0'
dbl(s(z0)) -> s(s(dbl(z0)))
add(0', z0) -> z0
add(s(z0), z1) -> s(add(z0, z1))
first(0', z0) -> nil
first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2))

Types:
TERMS :: s:0' -> c:c1
c :: c2:c3:c4 -> c:c1
SQR :: s:0' -> c2:c3:c4
c1 :: c:c1 -> c:c1
s :: s:0' -> s:0'
0' :: s:0'
c2 :: c2:c3:c4
c3 :: c7:c8 -> c2:c3:c4 -> c2:c3:c4
ADD :: s:0' -> s:0' -> c7:c8
sqr :: s:0' -> s:0'
dbl :: s:0' -> s:0'
c4 :: c7:c8 -> c5:c6 -> c2:c3:c4
DBL :: s:0' -> c5:c6
c5 :: c5:c6
c6 :: c5:c6 -> c5:c6
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
FIRST :: s:0' -> cons:nil -> c9:c10
c9 :: c9:c10
cons :: recip -> cons:nil -> cons:nil
c10 :: c9:c10 -> c9:c10
terms :: s:0' -> cons:nil
recip :: s:0' -> recip
add :: s:0' -> s:0' -> s:0'
first :: s:0' -> cons:nil -> cons:nil
nil :: cons:nil
hole_c:c11_11 :: c:c1
hole_s:0'2_11 :: s:0'
hole_c2:c3:c43_11 :: c2:c3:c4
hole_c7:c84_11 :: c7:c8
hole_c5:c65_11 :: c5:c6
hole_c9:c106_11 :: c9:c10
hole_cons:nil7_11 :: cons:nil
hole_recip8_11 :: recip
gen_c:c19_11 :: Nat -> c:c1
gen_s:0'10_11 :: Nat -> s:0'
gen_c2:c3:c411_11 :: Nat -> c2:c3:c4
gen_c7:c812_11 :: Nat -> c7:c8
gen_c5:c613_11 :: Nat -> c5:c6
gen_c9:c1014_11 :: Nat -> c9:c10
gen_cons:nil15_11 :: Nat -> cons:nil


Lemmas:
ADD(gen_s:0'10_11(n17_11), gen_s:0'10_11(b)) -> gen_c7:c812_11(n17_11), rt in Omega(1 + n17_11)
dbl(gen_s:0'10_11(n700_11)) -> gen_s:0'10_11(*(2, n700_11)), rt in Omega(0)
DBL(gen_s:0'10_11(n1094_11)) -> gen_c5:c613_11(n1094_11), rt in Omega(1 + n1094_11)
FIRST(gen_s:0'10_11(n1532_11), gen_cons:nil15_11(n1532_11)) -> gen_c9:c1014_11(n1532_11), rt in Omega(1 + n1532_11)
add(gen_s:0'10_11(n2159_11), gen_s:0'10_11(b)) -> gen_s:0'10_11(+(n2159_11, b)), rt in Omega(0)
sqr(gen_s:0'10_11(n3678_11)) -> gen_s:0'10_11(*(n3678_11, n3678_11)), rt in Omega(0)
SQR(gen_s:0'10_11(n4209_11)) -> *16_11, rt in Omega(n4209_11 + n4209_11^3)


Generator Equations:
gen_c:c19_11(0) <=> c(c2)
gen_c:c19_11(+(x, 1)) <=> c1(gen_c:c19_11(x))
gen_s:0'10_11(0) <=> 0'
gen_s:0'10_11(+(x, 1)) <=> s(gen_s:0'10_11(x))
gen_c2:c3:c411_11(0) <=> c2
gen_c2:c3:c411_11(+(x, 1)) <=> c3(c7, gen_c2:c3:c411_11(x))
gen_c7:c812_11(0) <=> c7
gen_c7:c812_11(+(x, 1)) <=> c8(gen_c7:c812_11(x))
gen_c5:c613_11(0) <=> c5
gen_c5:c613_11(+(x, 1)) <=> c6(gen_c5:c613_11(x))
gen_c9:c1014_11(0) <=> c9
gen_c9:c1014_11(+(x, 1)) <=> c10(gen_c9:c1014_11(x))
gen_cons:nil15_11(0) <=> nil
gen_cons:nil15_11(+(x, 1)) <=> cons(recip(0'), gen_cons:nil15_11(x))


The following defined symbols remain to be analysed:
TERMS, terms, first
----------------------------------------

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
first(gen_s:0'10_11(n16535_11), gen_cons:nil15_11(n16535_11)) -> gen_cons:nil15_11(n16535_11), rt in Omega(0)

Induction Base:
first(gen_s:0'10_11(0), gen_cons:nil15_11(0)) ->_R^Omega(0)
nil

Induction Step:
first(gen_s:0'10_11(+(n16535_11, 1)), gen_cons:nil15_11(+(n16535_11, 1))) ->_R^Omega(0)
cons(recip(0'), first(gen_s:0'10_11(n16535_11), gen_cons:nil15_11(n16535_11))) ->_IH
cons(recip(0'), gen_cons:nil15_11(c16536_11))

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

(34)
BOUNDS(1, INF)