WORST_CASE(Omega(n^1),?)
proof of input_UkCbJPW4DP.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), 9 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 292 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), 76 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 166 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 63 ms]
        (22) 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:

   and(true, X) -> X
   and(false, Y) -> false
   if(true, X, Y) -> X
   if(false, X, Y) -> Y
   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))
   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:
   and(true, z0) -> z0
   and(false, z0) -> false
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   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))
   from(z0) -> cons(z0, from(s(z0)))
Tuples:
   AND(true, z0) -> c
   AND(false, z0) -> c1
   IF(true, z0, z1) -> c2
   IF(false, z0, z1) -> c3
   ADD(0, z0) -> c4
   ADD(s(z0), z1) -> c5(ADD(z0, z1))
   FIRST(0, z0) -> c6
   FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
   FROM(z0) -> c8(FROM(s(z0)))
S tuples:
   AND(true, z0) -> c
   AND(false, z0) -> c1
   IF(true, z0, z1) -> c2
   IF(false, z0, z1) -> c3
   ADD(0, z0) -> c4
   ADD(s(z0), z1) -> c5(ADD(z0, z1))
   FIRST(0, z0) -> c6
   FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
   FROM(z0) -> c8(FROM(s(z0)))
K tuples:none
Defined Rule Symbols:   and_2, if_3, add_2, first_2, from_1

Defined Pair Symbols:   AND_2, IF_3, ADD_2, FIRST_2, FROM_1

Compound Symbols:   c, c1, c2, c3, c4, c5_1, c6, c7_1, c8_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:

   AND(true, z0) -> c
   AND(false, z0) -> c1
   IF(true, z0, z1) -> c2
   IF(false, z0, z1) -> c3
   ADD(0, z0) -> c4
   ADD(s(z0), z1) -> c5(ADD(z0, z1))
   FIRST(0, z0) -> c6
   FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
   FROM(z0) -> c8(FROM(s(z0)))

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

   and(true, z0) -> z0
   and(false, z0) -> false
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   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))
   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:

   AND(true, z0) -> c
   AND(false, z0) -> c1
   IF(true, z0, z1) -> c2
   IF(false, z0, z1) -> c3
   ADD(0', z0) -> c4
   ADD(s(z0), z1) -> c5(ADD(z0, z1))
   FIRST(0', z0) -> c6
   FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
   FROM(z0) -> c8(FROM(s(z0)))

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

   and(true, z0) -> z0
   and(false, z0) -> false
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   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))
   from(z0) -> cons(z0, from(s(z0)))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
ADD, FIRST, FROM, add, first, from
----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8


Generator Equations:
gen_c4:c514_9(0) <=> c4
gen_c4:c514_9(+(x, 1)) <=> c5(gen_c4:c514_9(x))
gen_0':s15_9(0) <=> 0'
gen_0':s15_9(+(x, 1)) <=> s(gen_0':s15_9(x))
gen_c6:c716_9(0) <=> c6
gen_c6:c716_9(+(x, 1)) <=> c7(gen_c6:c716_9(x))
gen_cons:nil17_9(0) <=> nil
gen_cons:nil17_9(+(x, 1)) <=> cons(0', gen_cons:nil17_9(x))
gen_c818_9(0) <=> hole_c812_9
gen_c818_9(+(x, 1)) <=> c8(gen_c818_9(x))


The following defined symbols remain to be analysed:
ADD, FIRST, FROM, add, first, from
----------------------------------------

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ADD(gen_0':s15_9(n20_9), hole_d9_9) -> gen_c4:c514_9(n20_9), rt in Omega(1 + n20_9)

Induction Base:
ADD(gen_0':s15_9(0), hole_d9_9) ->_R^Omega(1)
c4

Induction Step:
ADD(gen_0':s15_9(+(n20_9, 1)), hole_d9_9) ->_R^Omega(1)
c5(ADD(gen_0':s15_9(n20_9), hole_d9_9)) ->_IH
c5(gen_c4:c514_9(c21_9))

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:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8


Generator Equations:
gen_c4:c514_9(0) <=> c4
gen_c4:c514_9(+(x, 1)) <=> c5(gen_c4:c514_9(x))
gen_0':s15_9(0) <=> 0'
gen_0':s15_9(+(x, 1)) <=> s(gen_0':s15_9(x))
gen_c6:c716_9(0) <=> c6
gen_c6:c716_9(+(x, 1)) <=> c7(gen_c6:c716_9(x))
gen_cons:nil17_9(0) <=> nil
gen_cons:nil17_9(+(x, 1)) <=> cons(0', gen_cons:nil17_9(x))
gen_c818_9(0) <=> hole_c812_9
gen_c818_9(+(x, 1)) <=> c8(gen_c818_9(x))


The following defined symbols remain to be analysed:
ADD, FIRST, FROM, add, first, from
----------------------------------------

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8


Lemmas:
ADD(gen_0':s15_9(n20_9), hole_d9_9) -> gen_c4:c514_9(n20_9), rt in Omega(1 + n20_9)


Generator Equations:
gen_c4:c514_9(0) <=> c4
gen_c4:c514_9(+(x, 1)) <=> c5(gen_c4:c514_9(x))
gen_0':s15_9(0) <=> 0'
gen_0':s15_9(+(x, 1)) <=> s(gen_0':s15_9(x))
gen_c6:c716_9(0) <=> c6
gen_c6:c716_9(+(x, 1)) <=> c7(gen_c6:c716_9(x))
gen_cons:nil17_9(0) <=> nil
gen_cons:nil17_9(+(x, 1)) <=> cons(0', gen_cons:nil17_9(x))
gen_c818_9(0) <=> hole_c812_9
gen_c818_9(+(x, 1)) <=> c8(gen_c818_9(x))


The following defined symbols remain to be analysed:
FIRST, FROM, add, first, from
----------------------------------------

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
FIRST(gen_0':s15_9(n305_9), gen_cons:nil17_9(n305_9)) -> gen_c6:c716_9(n305_9), rt in Omega(1 + n305_9)

Induction Base:
FIRST(gen_0':s15_9(0), gen_cons:nil17_9(0)) ->_R^Omega(1)
c6

Induction Step:
FIRST(gen_0':s15_9(+(n305_9, 1)), gen_cons:nil17_9(+(n305_9, 1))) ->_R^Omega(1)
c7(FIRST(gen_0':s15_9(n305_9), gen_cons:nil17_9(n305_9))) ->_IH
c7(gen_c6:c716_9(c306_9))

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:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8


Lemmas:
ADD(gen_0':s15_9(n20_9), hole_d9_9) -> gen_c4:c514_9(n20_9), rt in Omega(1 + n20_9)
FIRST(gen_0':s15_9(n305_9), gen_cons:nil17_9(n305_9)) -> gen_c6:c716_9(n305_9), rt in Omega(1 + n305_9)


Generator Equations:
gen_c4:c514_9(0) <=> c4
gen_c4:c514_9(+(x, 1)) <=> c5(gen_c4:c514_9(x))
gen_0':s15_9(0) <=> 0'
gen_0':s15_9(+(x, 1)) <=> s(gen_0':s15_9(x))
gen_c6:c716_9(0) <=> c6
gen_c6:c716_9(+(x, 1)) <=> c7(gen_c6:c716_9(x))
gen_cons:nil17_9(0) <=> nil
gen_cons:nil17_9(+(x, 1)) <=> cons(0', gen_cons:nil17_9(x))
gen_c818_9(0) <=> hole_c812_9
gen_c818_9(+(x, 1)) <=> c8(gen_c818_9(x))


The following defined symbols remain to be analysed:
FROM, add, first, from
----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
add(gen_0':s15_9(n895_9), gen_0':s15_9(b)) -> gen_0':s15_9(+(n895_9, b)), rt in Omega(0)

Induction Base:
add(gen_0':s15_9(0), gen_0':s15_9(b)) ->_R^Omega(0)
gen_0':s15_9(b)

Induction Step:
add(gen_0':s15_9(+(n895_9, 1)), gen_0':s15_9(b)) ->_R^Omega(0)
s(add(gen_0':s15_9(n895_9), gen_0':s15_9(b))) ->_IH
s(gen_0':s15_9(+(b, c896_9)))

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:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8


Lemmas:
ADD(gen_0':s15_9(n20_9), hole_d9_9) -> gen_c4:c514_9(n20_9), rt in Omega(1 + n20_9)
FIRST(gen_0':s15_9(n305_9), gen_cons:nil17_9(n305_9)) -> gen_c6:c716_9(n305_9), rt in Omega(1 + n305_9)
add(gen_0':s15_9(n895_9), gen_0':s15_9(b)) -> gen_0':s15_9(+(n895_9, b)), rt in Omega(0)


Generator Equations:
gen_c4:c514_9(0) <=> c4
gen_c4:c514_9(+(x, 1)) <=> c5(gen_c4:c514_9(x))
gen_0':s15_9(0) <=> 0'
gen_0':s15_9(+(x, 1)) <=> s(gen_0':s15_9(x))
gen_c6:c716_9(0) <=> c6
gen_c6:c716_9(+(x, 1)) <=> c7(gen_c6:c716_9(x))
gen_cons:nil17_9(0) <=> nil
gen_cons:nil17_9(+(x, 1)) <=> cons(0', gen_cons:nil17_9(x))
gen_c818_9(0) <=> hole_c812_9
gen_c818_9(+(x, 1)) <=> c8(gen_c818_9(x))


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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
first(gen_0':s15_9(n2106_9), gen_cons:nil17_9(n2106_9)) -> gen_cons:nil17_9(n2106_9), rt in Omega(0)

Induction Base:
first(gen_0':s15_9(0), gen_cons:nil17_9(0)) ->_R^Omega(0)
nil

Induction Step:
first(gen_0':s15_9(+(n2106_9, 1)), gen_cons:nil17_9(+(n2106_9, 1))) ->_R^Omega(0)
cons(0', first(gen_0':s15_9(n2106_9), gen_cons:nil17_9(n2106_9))) ->_IH
cons(0', gen_cons:nil17_9(c2107_9))

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

(22)
Obligation:
Innermost TRS:
Rules:
AND(true, z0) -> c
AND(false, z0) -> c1
IF(true, z0, z1) -> c2
IF(false, z0, z1) -> c3
ADD(0', z0) -> c4
ADD(s(z0), z1) -> c5(ADD(z0, z1))
FIRST(0', z0) -> c6
FIRST(s(z0), cons(z1, z2)) -> c7(FIRST(z0, z2))
FROM(z0) -> c8(FROM(s(z0)))
and(true, z0) -> z0
and(false, z0) -> false
if(true, z0, z1) -> z0
if(false, z0, z1) -> z1
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))
from(z0) -> cons(z0, from(s(z0)))

Types:
AND :: true:false -> a -> c:c1
true :: true:false
c :: c:c1
false :: true:false
c1 :: c:c1
IF :: true:false -> b -> c -> c2:c3
c2 :: c2:c3
c3 :: c2:c3
ADD :: 0':s -> d -> c4:c5
0' :: 0':s
c4 :: c4:c5
s :: 0':s -> 0':s
c5 :: c4:c5 -> c4:c5
FIRST :: 0':s -> cons:nil -> c6:c7
c6 :: c6:c7
cons :: 0':s -> cons:nil -> cons:nil
c7 :: c6:c7 -> c6:c7
FROM :: 0':s -> c8
c8 :: c8 -> c8
and :: true:false -> true:false -> true:false
if :: true:false -> if -> if -> if
add :: 0':s -> 0':s -> 0':s
first :: 0':s -> cons:nil -> cons:nil
nil :: cons:nil
from :: 0':s -> cons:nil
hole_c:c11_9 :: c:c1
hole_true:false2_9 :: true:false
hole_a3_9 :: a
hole_c2:c34_9 :: c2:c3
hole_b5_9 :: b
hole_c6_9 :: c
hole_c4:c57_9 :: c4:c5
hole_0':s8_9 :: 0':s
hole_d9_9 :: d
hole_c6:c710_9 :: c6:c7
hole_cons:nil11_9 :: cons:nil
hole_c812_9 :: c8
hole_if13_9 :: if
gen_c4:c514_9 :: Nat -> c4:c5
gen_0':s15_9 :: Nat -> 0':s
gen_c6:c716_9 :: Nat -> c6:c7
gen_cons:nil17_9 :: Nat -> cons:nil
gen_c818_9 :: Nat -> c8


Lemmas:
ADD(gen_0':s15_9(n20_9), hole_d9_9) -> gen_c4:c514_9(n20_9), rt in Omega(1 + n20_9)
FIRST(gen_0':s15_9(n305_9), gen_cons:nil17_9(n305_9)) -> gen_c6:c716_9(n305_9), rt in Omega(1 + n305_9)
add(gen_0':s15_9(n895_9), gen_0':s15_9(b)) -> gen_0':s15_9(+(n895_9, b)), rt in Omega(0)
first(gen_0':s15_9(n2106_9), gen_cons:nil17_9(n2106_9)) -> gen_cons:nil17_9(n2106_9), rt in Omega(0)


Generator Equations:
gen_c4:c514_9(0) <=> c4
gen_c4:c514_9(+(x, 1)) <=> c5(gen_c4:c514_9(x))
gen_0':s15_9(0) <=> 0'
gen_0':s15_9(+(x, 1)) <=> s(gen_0':s15_9(x))
gen_c6:c716_9(0) <=> c6
gen_c6:c716_9(+(x, 1)) <=> c7(gen_c6:c716_9(x))
gen_cons:nil17_9(0) <=> nil
gen_cons:nil17_9(+(x, 1)) <=> cons(0', gen_cons:nil17_9(x))
gen_c818_9(0) <=> hole_c812_9
gen_c818_9(+(x, 1)) <=> c8(gen_c818_9(x))


The following defined symbols remain to be analysed:
from