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

   sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
   sum(cons(0, x), y) -> sum(x, y)
   sum(nil, y) -> y
   empty(nil) -> true
   empty(cons(n, x)) -> false
   tail(nil) -> nil
   tail(cons(n, x)) -> x
   head(cons(n, x)) -> n
   weight(x) -> if(empty(x), empty(tail(x)), x)
   if(true, b, x) -> weight_undefined_error
   if(false, b, x) -> if2(b, x)
   if2(true, x) -> head(x)
   if2(false, x) -> weight(sum(x, cons(0, tail(tail(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:
   sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
   sum(cons(0, z0), z1) -> sum(z0, z1)
   sum(nil, z0) -> z0
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
   if(true, z0, z1) -> weight_undefined_error
   if(false, z0, z1) -> if2(z0, z1)
   if2(true, z0) -> head(z0)
   if2(false, z0) -> weight(sum(z0, cons(0, tail(tail(z0)))))
Tuples:
   SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
   SUM(cons(0, z0), z1) -> c1(SUM(z0, z1))
   SUM(nil, z0) -> c2
   EMPTY(nil) -> c3
   EMPTY(cons(z0, z1)) -> c4
   TAIL(nil) -> c5
   TAIL(cons(z0, z1)) -> c6
   HEAD(cons(z0, z1)) -> c7
   WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
   WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(IF2(z0, z1))
   IF2(true, z0) -> c12(HEAD(z0))
   IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0, tail(tail(z0))))), SUM(z0, cons(0, tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
S tuples:
   SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
   SUM(cons(0, z0), z1) -> c1(SUM(z0, z1))
   SUM(nil, z0) -> c2
   EMPTY(nil) -> c3
   EMPTY(cons(z0, z1)) -> c4
   TAIL(nil) -> c5
   TAIL(cons(z0, z1)) -> c6
   HEAD(cons(z0, z1)) -> c7
   WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
   WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(IF2(z0, z1))
   IF2(true, z0) -> c12(HEAD(z0))
   IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0, tail(tail(z0))))), SUM(z0, cons(0, tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
K tuples:none
Defined Rule Symbols:   sum_2, empty_1, tail_1, head_1, weight_1, if_3, if2_2

Defined Pair Symbols:   SUM_2, EMPTY_1, TAIL_1, HEAD_1, WEIGHT_1, IF_3, IF2_2

Compound Symbols:   c_1, c1_1, c2, c3, c4, c5, c6, c7, c8_2, c9_3, c10, c11_1, c12_1, c13_4


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

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

   SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
   SUM(cons(0, z0), z1) -> c1(SUM(z0, z1))
   SUM(nil, z0) -> c2
   EMPTY(nil) -> c3
   EMPTY(cons(z0, z1)) -> c4
   TAIL(nil) -> c5
   TAIL(cons(z0, z1)) -> c6
   HEAD(cons(z0, z1)) -> c7
   WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
   WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(IF2(z0, z1))
   IF2(true, z0) -> c12(HEAD(z0))
   IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0, tail(tail(z0))))), SUM(z0, cons(0, tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))

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

   sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
   sum(cons(0, z0), z1) -> sum(z0, z1)
   sum(nil, z0) -> z0
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
   if(true, z0, z1) -> weight_undefined_error
   if(false, z0, z1) -> if2(z0, z1)
   if2(true, z0) -> head(z0)
   if2(false, z0) -> weight(sum(z0, cons(0, tail(tail(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:

   SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
   SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
   SUM(nil, z0) -> c2
   EMPTY(nil) -> c3
   EMPTY(cons(z0, z1)) -> c4
   TAIL(nil) -> c5
   TAIL(cons(z0, z1)) -> c6
   HEAD(cons(z0, z1)) -> c7
   WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
   WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
   IF(true, z0, z1) -> c10
   IF(false, z0, z1) -> c11(IF2(z0, z1))
   IF2(true, z0) -> c12(HEAD(z0))
   IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))

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

   sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
   sum(cons(0', z0), z1) -> sum(z0, z1)
   sum(nil, z0) -> z0
   empty(nil) -> true
   empty(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
   if(true, z0, z1) -> weight_undefined_error
   if(false, z0, z1) -> if2(z0, z1)
   if2(true, z0) -> head(z0)
   if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

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

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

(8)
Obligation:
Innermost TRS:
Rules:
SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
SUM(nil, z0) -> c2
EMPTY(nil) -> c3
EMPTY(cons(z0, z1)) -> c4
TAIL(nil) -> c5
TAIL(cons(z0, z1)) -> c6
HEAD(cons(z0, z1)) -> c7
WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(IF2(z0, z1))
IF2(true, z0) -> c12(HEAD(z0))
IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
sum(cons(0', z0), z1) -> sum(z0, z1)
sum(nil, z0) -> z0
empty(nil) -> true
empty(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
if(true, z0, z1) -> weight_undefined_error
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> head(z0)
if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

Types:
SUM :: cons:nil -> cons:nil -> c:c1:c2
cons :: s:0':weight_undefined_error -> cons:nil -> cons:nil
s :: s:0':weight_undefined_error -> s:0':weight_undefined_error
c :: c:c1:c2 -> c:c1:c2
0' :: s:0':weight_undefined_error
c1 :: c:c1:c2 -> c:c1:c2
nil :: cons:nil
c2 :: c:c1:c2
EMPTY :: cons:nil -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
HEAD :: cons:nil -> c7
c7 :: c7
WEIGHT :: cons:nil -> c8:c9
c8 :: c10:c11 -> c3:c4 -> c8:c9
IF :: true:false -> true:false -> cons:nil -> c10:c11
empty :: cons:nil -> true:false
tail :: cons:nil -> cons:nil
c9 :: c10:c11 -> c3:c4 -> c5:c6 -> c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c12:c13 -> c10:c11
IF2 :: true:false -> cons:nil -> c12:c13
c12 :: c7 -> c12:c13
c13 :: c8:c9 -> c:c1:c2 -> c5:c6 -> c5:c6 -> c12:c13
sum :: cons:nil -> cons:nil -> cons:nil
head :: cons:nil -> s:0':weight_undefined_error
weight :: cons:nil -> s:0':weight_undefined_error
if :: true:false -> true:false -> cons:nil -> s:0':weight_undefined_error
weight_undefined_error :: s:0':weight_undefined_error
if2 :: true:false -> cons:nil -> s:0':weight_undefined_error
hole_c:c1:c21_14 :: c:c1:c2
hole_cons:nil2_14 :: cons:nil
hole_s:0':weight_undefined_error3_14 :: s:0':weight_undefined_error
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c76_14 :: c7
hole_c8:c97_14 :: c8:c9
hole_c10:c118_14 :: c10:c11
hole_true:false9_14 :: true:false
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_cons:nil12_14 :: Nat -> cons:nil
gen_s:0':weight_undefined_error13_14 :: Nat -> s:0':weight_undefined_error

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
SUM, WEIGHT, sum, weight

They will be analysed ascendingly in the following order:
SUM < WEIGHT
sum < WEIGHT
sum < weight

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

(10)
Obligation:
Innermost TRS:
Rules:
SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
SUM(nil, z0) -> c2
EMPTY(nil) -> c3
EMPTY(cons(z0, z1)) -> c4
TAIL(nil) -> c5
TAIL(cons(z0, z1)) -> c6
HEAD(cons(z0, z1)) -> c7
WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(IF2(z0, z1))
IF2(true, z0) -> c12(HEAD(z0))
IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
sum(cons(0', z0), z1) -> sum(z0, z1)
sum(nil, z0) -> z0
empty(nil) -> true
empty(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
if(true, z0, z1) -> weight_undefined_error
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> head(z0)
if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

Types:
SUM :: cons:nil -> cons:nil -> c:c1:c2
cons :: s:0':weight_undefined_error -> cons:nil -> cons:nil
s :: s:0':weight_undefined_error -> s:0':weight_undefined_error
c :: c:c1:c2 -> c:c1:c2
0' :: s:0':weight_undefined_error
c1 :: c:c1:c2 -> c:c1:c2
nil :: cons:nil
c2 :: c:c1:c2
EMPTY :: cons:nil -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
HEAD :: cons:nil -> c7
c7 :: c7
WEIGHT :: cons:nil -> c8:c9
c8 :: c10:c11 -> c3:c4 -> c8:c9
IF :: true:false -> true:false -> cons:nil -> c10:c11
empty :: cons:nil -> true:false
tail :: cons:nil -> cons:nil
c9 :: c10:c11 -> c3:c4 -> c5:c6 -> c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c12:c13 -> c10:c11
IF2 :: true:false -> cons:nil -> c12:c13
c12 :: c7 -> c12:c13
c13 :: c8:c9 -> c:c1:c2 -> c5:c6 -> c5:c6 -> c12:c13
sum :: cons:nil -> cons:nil -> cons:nil
head :: cons:nil -> s:0':weight_undefined_error
weight :: cons:nil -> s:0':weight_undefined_error
if :: true:false -> true:false -> cons:nil -> s:0':weight_undefined_error
weight_undefined_error :: s:0':weight_undefined_error
if2 :: true:false -> cons:nil -> s:0':weight_undefined_error
hole_c:c1:c21_14 :: c:c1:c2
hole_cons:nil2_14 :: cons:nil
hole_s:0':weight_undefined_error3_14 :: s:0':weight_undefined_error
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c76_14 :: c7
hole_c8:c97_14 :: c8:c9
hole_c10:c118_14 :: c10:c11
hole_true:false9_14 :: true:false
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_cons:nil12_14 :: Nat -> cons:nil
gen_s:0':weight_undefined_error13_14 :: Nat -> s:0':weight_undefined_error


Generator Equations:
gen_c:c1:c211_14(0) <=> c2
gen_c:c1:c211_14(+(x, 1)) <=> c(gen_c:c1:c211_14(x))
gen_cons:nil12_14(0) <=> nil
gen_cons:nil12_14(+(x, 1)) <=> cons(0', gen_cons:nil12_14(x))
gen_s:0':weight_undefined_error13_14(0) <=> 0'
gen_s:0':weight_undefined_error13_14(+(x, 1)) <=> s(gen_s:0':weight_undefined_error13_14(x))


The following defined symbols remain to be analysed:
SUM, WEIGHT, sum, weight

They will be analysed ascendingly in the following order:
SUM < WEIGHT
sum < WEIGHT
sum < weight

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SUM(gen_cons:nil12_14(+(1, n15_14)), gen_cons:nil12_14(b)) -> *14_14, rt in Omega(n15_14)

Induction Base:
SUM(gen_cons:nil12_14(+(1, 0)), gen_cons:nil12_14(b))

Induction Step:
SUM(gen_cons:nil12_14(+(1, +(n15_14, 1))), gen_cons:nil12_14(b)) ->_R^Omega(1)
c1(SUM(gen_cons:nil12_14(+(1, n15_14)), gen_cons:nil12_14(b))) ->_IH
c1(*14_14)

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:
SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
SUM(nil, z0) -> c2
EMPTY(nil) -> c3
EMPTY(cons(z0, z1)) -> c4
TAIL(nil) -> c5
TAIL(cons(z0, z1)) -> c6
HEAD(cons(z0, z1)) -> c7
WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(IF2(z0, z1))
IF2(true, z0) -> c12(HEAD(z0))
IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
sum(cons(0', z0), z1) -> sum(z0, z1)
sum(nil, z0) -> z0
empty(nil) -> true
empty(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
if(true, z0, z1) -> weight_undefined_error
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> head(z0)
if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

Types:
SUM :: cons:nil -> cons:nil -> c:c1:c2
cons :: s:0':weight_undefined_error -> cons:nil -> cons:nil
s :: s:0':weight_undefined_error -> s:0':weight_undefined_error
c :: c:c1:c2 -> c:c1:c2
0' :: s:0':weight_undefined_error
c1 :: c:c1:c2 -> c:c1:c2
nil :: cons:nil
c2 :: c:c1:c2
EMPTY :: cons:nil -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
HEAD :: cons:nil -> c7
c7 :: c7
WEIGHT :: cons:nil -> c8:c9
c8 :: c10:c11 -> c3:c4 -> c8:c9
IF :: true:false -> true:false -> cons:nil -> c10:c11
empty :: cons:nil -> true:false
tail :: cons:nil -> cons:nil
c9 :: c10:c11 -> c3:c4 -> c5:c6 -> c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c12:c13 -> c10:c11
IF2 :: true:false -> cons:nil -> c12:c13
c12 :: c7 -> c12:c13
c13 :: c8:c9 -> c:c1:c2 -> c5:c6 -> c5:c6 -> c12:c13
sum :: cons:nil -> cons:nil -> cons:nil
head :: cons:nil -> s:0':weight_undefined_error
weight :: cons:nil -> s:0':weight_undefined_error
if :: true:false -> true:false -> cons:nil -> s:0':weight_undefined_error
weight_undefined_error :: s:0':weight_undefined_error
if2 :: true:false -> cons:nil -> s:0':weight_undefined_error
hole_c:c1:c21_14 :: c:c1:c2
hole_cons:nil2_14 :: cons:nil
hole_s:0':weight_undefined_error3_14 :: s:0':weight_undefined_error
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c76_14 :: c7
hole_c8:c97_14 :: c8:c9
hole_c10:c118_14 :: c10:c11
hole_true:false9_14 :: true:false
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_cons:nil12_14 :: Nat -> cons:nil
gen_s:0':weight_undefined_error13_14 :: Nat -> s:0':weight_undefined_error


Generator Equations:
gen_c:c1:c211_14(0) <=> c2
gen_c:c1:c211_14(+(x, 1)) <=> c(gen_c:c1:c211_14(x))
gen_cons:nil12_14(0) <=> nil
gen_cons:nil12_14(+(x, 1)) <=> cons(0', gen_cons:nil12_14(x))
gen_s:0':weight_undefined_error13_14(0) <=> 0'
gen_s:0':weight_undefined_error13_14(+(x, 1)) <=> s(gen_s:0':weight_undefined_error13_14(x))


The following defined symbols remain to be analysed:
SUM, WEIGHT, sum, weight

They will be analysed ascendingly in the following order:
SUM < WEIGHT
sum < WEIGHT
sum < weight

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
SUM(nil, z0) -> c2
EMPTY(nil) -> c3
EMPTY(cons(z0, z1)) -> c4
TAIL(nil) -> c5
TAIL(cons(z0, z1)) -> c6
HEAD(cons(z0, z1)) -> c7
WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(IF2(z0, z1))
IF2(true, z0) -> c12(HEAD(z0))
IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
sum(cons(0', z0), z1) -> sum(z0, z1)
sum(nil, z0) -> z0
empty(nil) -> true
empty(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
if(true, z0, z1) -> weight_undefined_error
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> head(z0)
if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

Types:
SUM :: cons:nil -> cons:nil -> c:c1:c2
cons :: s:0':weight_undefined_error -> cons:nil -> cons:nil
s :: s:0':weight_undefined_error -> s:0':weight_undefined_error
c :: c:c1:c2 -> c:c1:c2
0' :: s:0':weight_undefined_error
c1 :: c:c1:c2 -> c:c1:c2
nil :: cons:nil
c2 :: c:c1:c2
EMPTY :: cons:nil -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
HEAD :: cons:nil -> c7
c7 :: c7
WEIGHT :: cons:nil -> c8:c9
c8 :: c10:c11 -> c3:c4 -> c8:c9
IF :: true:false -> true:false -> cons:nil -> c10:c11
empty :: cons:nil -> true:false
tail :: cons:nil -> cons:nil
c9 :: c10:c11 -> c3:c4 -> c5:c6 -> c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c12:c13 -> c10:c11
IF2 :: true:false -> cons:nil -> c12:c13
c12 :: c7 -> c12:c13
c13 :: c8:c9 -> c:c1:c2 -> c5:c6 -> c5:c6 -> c12:c13
sum :: cons:nil -> cons:nil -> cons:nil
head :: cons:nil -> s:0':weight_undefined_error
weight :: cons:nil -> s:0':weight_undefined_error
if :: true:false -> true:false -> cons:nil -> s:0':weight_undefined_error
weight_undefined_error :: s:0':weight_undefined_error
if2 :: true:false -> cons:nil -> s:0':weight_undefined_error
hole_c:c1:c21_14 :: c:c1:c2
hole_cons:nil2_14 :: cons:nil
hole_s:0':weight_undefined_error3_14 :: s:0':weight_undefined_error
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c76_14 :: c7
hole_c8:c97_14 :: c8:c9
hole_c10:c118_14 :: c10:c11
hole_true:false9_14 :: true:false
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_cons:nil12_14 :: Nat -> cons:nil
gen_s:0':weight_undefined_error13_14 :: Nat -> s:0':weight_undefined_error


Lemmas:
SUM(gen_cons:nil12_14(+(1, n15_14)), gen_cons:nil12_14(b)) -> *14_14, rt in Omega(n15_14)


Generator Equations:
gen_c:c1:c211_14(0) <=> c2
gen_c:c1:c211_14(+(x, 1)) <=> c(gen_c:c1:c211_14(x))
gen_cons:nil12_14(0) <=> nil
gen_cons:nil12_14(+(x, 1)) <=> cons(0', gen_cons:nil12_14(x))
gen_s:0':weight_undefined_error13_14(0) <=> 0'
gen_s:0':weight_undefined_error13_14(+(x, 1)) <=> s(gen_s:0':weight_undefined_error13_14(x))


The following defined symbols remain to be analysed:
sum, WEIGHT, weight

They will be analysed ascendingly in the following order:
sum < WEIGHT
sum < weight

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sum(gen_cons:nil12_14(n3053_14), gen_cons:nil12_14(b)) -> gen_cons:nil12_14(b), rt in Omega(0)

Induction Base:
sum(gen_cons:nil12_14(0), gen_cons:nil12_14(b)) ->_R^Omega(0)
gen_cons:nil12_14(b)

Induction Step:
sum(gen_cons:nil12_14(+(n3053_14, 1)), gen_cons:nil12_14(b)) ->_R^Omega(0)
sum(gen_cons:nil12_14(n3053_14), gen_cons:nil12_14(b)) ->_IH
gen_cons:nil12_14(b)

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:
SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
SUM(nil, z0) -> c2
EMPTY(nil) -> c3
EMPTY(cons(z0, z1)) -> c4
TAIL(nil) -> c5
TAIL(cons(z0, z1)) -> c6
HEAD(cons(z0, z1)) -> c7
WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(IF2(z0, z1))
IF2(true, z0) -> c12(HEAD(z0))
IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
sum(cons(0', z0), z1) -> sum(z0, z1)
sum(nil, z0) -> z0
empty(nil) -> true
empty(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
if(true, z0, z1) -> weight_undefined_error
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> head(z0)
if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

Types:
SUM :: cons:nil -> cons:nil -> c:c1:c2
cons :: s:0':weight_undefined_error -> cons:nil -> cons:nil
s :: s:0':weight_undefined_error -> s:0':weight_undefined_error
c :: c:c1:c2 -> c:c1:c2
0' :: s:0':weight_undefined_error
c1 :: c:c1:c2 -> c:c1:c2
nil :: cons:nil
c2 :: c:c1:c2
EMPTY :: cons:nil -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
HEAD :: cons:nil -> c7
c7 :: c7
WEIGHT :: cons:nil -> c8:c9
c8 :: c10:c11 -> c3:c4 -> c8:c9
IF :: true:false -> true:false -> cons:nil -> c10:c11
empty :: cons:nil -> true:false
tail :: cons:nil -> cons:nil
c9 :: c10:c11 -> c3:c4 -> c5:c6 -> c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c12:c13 -> c10:c11
IF2 :: true:false -> cons:nil -> c12:c13
c12 :: c7 -> c12:c13
c13 :: c8:c9 -> c:c1:c2 -> c5:c6 -> c5:c6 -> c12:c13
sum :: cons:nil -> cons:nil -> cons:nil
head :: cons:nil -> s:0':weight_undefined_error
weight :: cons:nil -> s:0':weight_undefined_error
if :: true:false -> true:false -> cons:nil -> s:0':weight_undefined_error
weight_undefined_error :: s:0':weight_undefined_error
if2 :: true:false -> cons:nil -> s:0':weight_undefined_error
hole_c:c1:c21_14 :: c:c1:c2
hole_cons:nil2_14 :: cons:nil
hole_s:0':weight_undefined_error3_14 :: s:0':weight_undefined_error
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c76_14 :: c7
hole_c8:c97_14 :: c8:c9
hole_c10:c118_14 :: c10:c11
hole_true:false9_14 :: true:false
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_cons:nil12_14 :: Nat -> cons:nil
gen_s:0':weight_undefined_error13_14 :: Nat -> s:0':weight_undefined_error


Lemmas:
SUM(gen_cons:nil12_14(+(1, n15_14)), gen_cons:nil12_14(b)) -> *14_14, rt in Omega(n15_14)
sum(gen_cons:nil12_14(n3053_14), gen_cons:nil12_14(b)) -> gen_cons:nil12_14(b), rt in Omega(0)


Generator Equations:
gen_c:c1:c211_14(0) <=> c2
gen_c:c1:c211_14(+(x, 1)) <=> c(gen_c:c1:c211_14(x))
gen_cons:nil12_14(0) <=> nil
gen_cons:nil12_14(+(x, 1)) <=> cons(0', gen_cons:nil12_14(x))
gen_s:0':weight_undefined_error13_14(0) <=> 0'
gen_s:0':weight_undefined_error13_14(+(x, 1)) <=> s(gen_s:0':weight_undefined_error13_14(x))


The following defined symbols remain to be analysed:
WEIGHT, weight
----------------------------------------

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
WEIGHT(gen_cons:nil12_14(+(1, n4171_14))) -> *14_14, rt in Omega(n4171_14)

Induction Base:
WEIGHT(gen_cons:nil12_14(+(1, 0)))

Induction Step:
WEIGHT(gen_cons:nil12_14(+(1, +(n4171_14, 1)))) ->_R^Omega(1)
c8(IF(empty(gen_cons:nil12_14(+(1, +(n4171_14, 1)))), empty(tail(gen_cons:nil12_14(+(1, +(n4171_14, 1))))), gen_cons:nil12_14(+(1, +(n4171_14, 1)))), EMPTY(gen_cons:nil12_14(+(1, +(n4171_14, 1))))) ->_R^Omega(0)
c8(IF(false, empty(tail(gen_cons:nil12_14(+(2, n4171_14)))), gen_cons:nil12_14(+(2, n4171_14))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(IF(false, empty(gen_cons:nil12_14(+(1, n4171_14))), gen_cons:nil12_14(+(2, n4171_14))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(IF(false, false, gen_cons:nil12_14(+(2, n4171_14))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(IF2(false, gen_cons:nil12_14(+(2, n4171_14)))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(c13(WEIGHT(sum(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n4171_14))))))), SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n4171_14)))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(c11(c13(WEIGHT(sum(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(gen_cons:nil12_14(+(1, n4171_14)))))), SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n4171_14)))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(c11(c13(WEIGHT(sum(gen_cons:nil12_14(+(2, n4171_14)), cons(0', gen_cons:nil12_14(n4171_14)))), SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n4171_14)))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_L^Omega(0)
c8(c11(c13(WEIGHT(gen_cons:nil12_14(+(n4171_14, 1))), SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n4171_14)))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_IH
c8(c11(c13(*14_14, SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n4171_14)))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(c11(c13(*14_14, SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', tail(gen_cons:nil12_14(+(1, n4171_14))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(c11(c13(*14_14, SUM(gen_cons:nil12_14(+(2, n4171_14)), cons(0', gen_cons:nil12_14(n4171_14))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(c13(*14_14, c1(SUM(gen_cons:nil12_14(+(1, n4171_14)), cons(0', gen_cons:nil12_14(n4171_14)))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(c13(*14_14, c1(c1(SUM(gen_cons:nil12_14(n4171_14), cons(0', gen_cons:nil12_14(n4171_14))))), TAIL(tail(gen_cons:nil12_14(+(2, n4171_14)))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(0)
c8(c11(c13(*14_14, c1(c1(SUM(gen_cons:nil12_14(n4171_14), cons(0', gen_cons:nil12_14(n4171_14))))), TAIL(gen_cons:nil12_14(+(1, n4171_14))), TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(c13(*14_14, c1(c1(SUM(gen_cons:nil12_14(n4171_14), cons(0', gen_cons:nil12_14(n4171_14))))), c6, TAIL(gen_cons:nil12_14(+(2, n4171_14))))), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(c13(*14_14, c1(c1(SUM(gen_cons:nil12_14(n4171_14), cons(0', gen_cons:nil12_14(n4171_14))))), c6, c6)), EMPTY(gen_cons:nil12_14(+(2, n4171_14)))) ->_R^Omega(1)
c8(c11(c13(*14_14, c1(c1(SUM(gen_cons:nil12_14(n4171_14), cons(0', gen_cons:nil12_14(n4171_14))))), c6, c6)), c4)

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:
SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3)))
SUM(cons(0', z0), z1) -> c1(SUM(z0, z1))
SUM(nil, z0) -> c2
EMPTY(nil) -> c3
EMPTY(cons(z0, z1)) -> c4
TAIL(nil) -> c5
TAIL(cons(z0, z1)) -> c6
HEAD(cons(z0, z1)) -> c7
WEIGHT(z0) -> c8(IF(empty(z0), empty(tail(z0)), z0), EMPTY(z0))
WEIGHT(z0) -> c9(IF(empty(z0), empty(tail(z0)), z0), EMPTY(tail(z0)), TAIL(z0))
IF(true, z0, z1) -> c10
IF(false, z0, z1) -> c11(IF2(z0, z1))
IF2(true, z0) -> c12(HEAD(z0))
IF2(false, z0) -> c13(WEIGHT(sum(z0, cons(0', tail(tail(z0))))), SUM(z0, cons(0', tail(tail(z0)))), TAIL(tail(z0)), TAIL(z0))
sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3))
sum(cons(0', z0), z1) -> sum(z0, z1)
sum(nil, z0) -> z0
empty(nil) -> true
empty(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
weight(z0) -> if(empty(z0), empty(tail(z0)), z0)
if(true, z0, z1) -> weight_undefined_error
if(false, z0, z1) -> if2(z0, z1)
if2(true, z0) -> head(z0)
if2(false, z0) -> weight(sum(z0, cons(0', tail(tail(z0)))))

Types:
SUM :: cons:nil -> cons:nil -> c:c1:c2
cons :: s:0':weight_undefined_error -> cons:nil -> cons:nil
s :: s:0':weight_undefined_error -> s:0':weight_undefined_error
c :: c:c1:c2 -> c:c1:c2
0' :: s:0':weight_undefined_error
c1 :: c:c1:c2 -> c:c1:c2
nil :: cons:nil
c2 :: c:c1:c2
EMPTY :: cons:nil -> c3:c4
c3 :: c3:c4
c4 :: c3:c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
HEAD :: cons:nil -> c7
c7 :: c7
WEIGHT :: cons:nil -> c8:c9
c8 :: c10:c11 -> c3:c4 -> c8:c9
IF :: true:false -> true:false -> cons:nil -> c10:c11
empty :: cons:nil -> true:false
tail :: cons:nil -> cons:nil
c9 :: c10:c11 -> c3:c4 -> c5:c6 -> c8:c9
true :: true:false
c10 :: c10:c11
false :: true:false
c11 :: c12:c13 -> c10:c11
IF2 :: true:false -> cons:nil -> c12:c13
c12 :: c7 -> c12:c13
c13 :: c8:c9 -> c:c1:c2 -> c5:c6 -> c5:c6 -> c12:c13
sum :: cons:nil -> cons:nil -> cons:nil
head :: cons:nil -> s:0':weight_undefined_error
weight :: cons:nil -> s:0':weight_undefined_error
if :: true:false -> true:false -> cons:nil -> s:0':weight_undefined_error
weight_undefined_error :: s:0':weight_undefined_error
if2 :: true:false -> cons:nil -> s:0':weight_undefined_error
hole_c:c1:c21_14 :: c:c1:c2
hole_cons:nil2_14 :: cons:nil
hole_s:0':weight_undefined_error3_14 :: s:0':weight_undefined_error
hole_c3:c44_14 :: c3:c4
hole_c5:c65_14 :: c5:c6
hole_c76_14 :: c7
hole_c8:c97_14 :: c8:c9
hole_c10:c118_14 :: c10:c11
hole_true:false9_14 :: true:false
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_cons:nil12_14 :: Nat -> cons:nil
gen_s:0':weight_undefined_error13_14 :: Nat -> s:0':weight_undefined_error


Lemmas:
SUM(gen_cons:nil12_14(+(1, n15_14)), gen_cons:nil12_14(b)) -> *14_14, rt in Omega(n15_14)
sum(gen_cons:nil12_14(n3053_14), gen_cons:nil12_14(b)) -> gen_cons:nil12_14(b), rt in Omega(0)
WEIGHT(gen_cons:nil12_14(+(1, n4171_14))) -> *14_14, rt in Omega(n4171_14)


Generator Equations:
gen_c:c1:c211_14(0) <=> c2
gen_c:c1:c211_14(+(x, 1)) <=> c(gen_c:c1:c211_14(x))
gen_cons:nil12_14(0) <=> nil
gen_cons:nil12_14(+(x, 1)) <=> cons(0', gen_cons:nil12_14(x))
gen_s:0':weight_undefined_error13_14(0) <=> 0'
gen_s:0':weight_undefined_error13_14(+(x, 1)) <=> s(gen_s:0':weight_undefined_error13_14(x))


The following defined symbols remain to be analysed:
weight
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
weight(gen_cons:nil12_14(+(1, n41190_14))) -> gen_s:0':weight_undefined_error13_14(0), rt in Omega(0)

Induction Base:
weight(gen_cons:nil12_14(+(1, 0))) ->_R^Omega(0)
if(empty(gen_cons:nil12_14(+(1, 0))), empty(tail(gen_cons:nil12_14(+(1, 0)))), gen_cons:nil12_14(+(1, 0))) ->_R^Omega(0)
if(false, empty(tail(gen_cons:nil12_14(1))), gen_cons:nil12_14(1)) ->_R^Omega(0)
if(false, empty(gen_cons:nil12_14(0)), gen_cons:nil12_14(1)) ->_R^Omega(0)
if(false, true, gen_cons:nil12_14(1)) ->_R^Omega(0)
if2(true, gen_cons:nil12_14(1)) ->_R^Omega(0)
head(gen_cons:nil12_14(1)) ->_R^Omega(0)
0'

Induction Step:
weight(gen_cons:nil12_14(+(1, +(n41190_14, 1)))) ->_R^Omega(0)
if(empty(gen_cons:nil12_14(+(1, +(n41190_14, 1)))), empty(tail(gen_cons:nil12_14(+(1, +(n41190_14, 1))))), gen_cons:nil12_14(+(1, +(n41190_14, 1)))) ->_R^Omega(0)
if(false, empty(tail(gen_cons:nil12_14(+(2, n41190_14)))), gen_cons:nil12_14(+(2, n41190_14))) ->_R^Omega(0)
if(false, empty(gen_cons:nil12_14(+(1, n41190_14))), gen_cons:nil12_14(+(2, n41190_14))) ->_R^Omega(0)
if(false, false, gen_cons:nil12_14(+(2, n41190_14))) ->_R^Omega(0)
if2(false, gen_cons:nil12_14(+(2, n41190_14))) ->_R^Omega(0)
weight(sum(gen_cons:nil12_14(+(2, n41190_14)), cons(0', tail(tail(gen_cons:nil12_14(+(2, n41190_14))))))) ->_R^Omega(0)
weight(sum(gen_cons:nil12_14(+(2, n41190_14)), cons(0', tail(gen_cons:nil12_14(+(1, n41190_14)))))) ->_R^Omega(0)
weight(sum(gen_cons:nil12_14(+(2, n41190_14)), cons(0', gen_cons:nil12_14(n41190_14)))) ->_L^Omega(0)
weight(gen_cons:nil12_14(+(n41190_14, 1))) ->_IH
gen_s:0':weight_undefined_error13_14(0)

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

(22)
BOUNDS(1, INF)