WORST_CASE(Omega(n^1),?)
proof of input_xIwELFTOih.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), 18 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 319 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), 55 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 119 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 53 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:

   times(x, y) -> sum(generate(x, y))
   generate(x, y) -> gen(x, y, 0)
   gen(x, y, z) -> if(ge(z, x), x, y, z)
   if(true, x, y, z) -> nil
   if(false, x, y, z) -> cons(y, gen(x, y, s(z)))
   sum(nil) -> 0
   sum(cons(0, xs)) -> sum(xs)
   sum(cons(s(x), xs)) -> s(sum(cons(x, xs)))
   ge(x, 0) -> true
   ge(0, s(y)) -> false
   ge(s(x), s(y)) -> ge(x, y)

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:
   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(nil) -> 0
   sum(cons(0, z0)) -> sum(z0)
   sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
Tuples:
   TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c1(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c3
   IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
   SUM(nil) -> c5
   SUM(cons(0, z0)) -> c6(SUM(z0))
   SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
   GE(z0, 0) -> c8
   GE(0, s(z0)) -> c9
   GE(s(z0), s(z1)) -> c10(GE(z0, z1))
S tuples:
   TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c1(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c3
   IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
   SUM(nil) -> c5
   SUM(cons(0, z0)) -> c6(SUM(z0))
   SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
   GE(z0, 0) -> c8
   GE(0, s(z0)) -> c9
   GE(s(z0), s(z1)) -> c10(GE(z0, z1))
K tuples:none
Defined Rule Symbols:   times_2, generate_2, gen_3, if_4, sum_1, ge_2

Defined Pair Symbols:   TIMES_2, GENERATE_2, GEN_3, IF_4, SUM_1, GE_2

Compound Symbols:   c_2, c1_1, c2_2, c3, c4_1, c5, c6_1, c7_1, c8, 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^1, INF).


The TRS R consists of the following rules:

   TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c1(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c3
   IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
   SUM(nil) -> c5
   SUM(cons(0, z0)) -> c6(SUM(z0))
   SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
   GE(z0, 0) -> c8
   GE(0, s(z0)) -> c9
   GE(s(z0), s(z1)) -> c10(GE(z0, z1))

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0)
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(nil) -> 0
   sum(cons(0, z0)) -> sum(z0)
   sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)

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:

   TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
   GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c3
   IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
   SUM(nil) -> c5
   SUM(cons(0', z0)) -> c6(SUM(z0))
   SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
   GE(z0, 0') -> c8
   GE(0', s(z0)) -> c9
   GE(s(z0), s(z1)) -> c10(GE(z0, z1))

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

   times(z0, z1) -> sum(generate(z0, z1))
   generate(z0, z1) -> gen(z0, z1, 0')
   gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
   if(true, z0, z1, z2) -> nil
   if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
   sum(nil) -> 0'
   sum(cons(0', z0)) -> sum(z0)
   sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)

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

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

(8)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
SUM, GEN, ge, GE, sum, gen

They will be analysed ascendingly in the following order:
ge < GEN
GE < GEN
ge < gen

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

(10)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c5:c6:c711_11(0) <=> c5
gen_c5:c6:c711_11(+(x, 1)) <=> c6(gen_c5:c6:c711_11(x))
gen_nil:cons12_11(0) <=> nil
gen_nil:cons12_11(+(x, 1)) <=> cons(0', gen_nil:cons12_11(x))
gen_c8:c9:c1013_11(0) <=> c8
gen_c8:c9:c1013_11(+(x, 1)) <=> c10(gen_c8:c9:c1013_11(x))


The following defined symbols remain to be analysed:
SUM, GEN, ge, GE, sum, gen

They will be analysed ascendingly in the following order:
ge < GEN
GE < GEN
ge < gen

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SUM(gen_nil:cons12_11(n15_11)) -> gen_c5:c6:c711_11(n15_11), rt in Omega(1 + n15_11)

Induction Base:
SUM(gen_nil:cons12_11(0)) ->_R^Omega(1)
c5

Induction Step:
SUM(gen_nil:cons12_11(+(n15_11, 1))) ->_R^Omega(1)
c6(SUM(gen_nil:cons12_11(n15_11))) ->_IH
c6(gen_c5:c6:c711_11(c16_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:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c5:c6:c711_11(0) <=> c5
gen_c5:c6:c711_11(+(x, 1)) <=> c6(gen_c5:c6:c711_11(x))
gen_nil:cons12_11(0) <=> nil
gen_nil:cons12_11(+(x, 1)) <=> cons(0', gen_nil:cons12_11(x))
gen_c8:c9:c1013_11(0) <=> c8
gen_c8:c9:c1013_11(+(x, 1)) <=> c10(gen_c8:c9:c1013_11(x))


The following defined symbols remain to be analysed:
SUM, GEN, ge, GE, sum, gen

They will be analysed ascendingly in the following order:
ge < GEN
GE < GEN
ge < gen

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10


Lemmas:
SUM(gen_nil:cons12_11(n15_11)) -> gen_c5:c6:c711_11(n15_11), rt in Omega(1 + n15_11)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c5:c6:c711_11(0) <=> c5
gen_c5:c6:c711_11(+(x, 1)) <=> c6(gen_c5:c6:c711_11(x))
gen_nil:cons12_11(0) <=> nil
gen_nil:cons12_11(+(x, 1)) <=> cons(0', gen_nil:cons12_11(x))
gen_c8:c9:c1013_11(0) <=> c8
gen_c8:c9:c1013_11(+(x, 1)) <=> c10(gen_c8:c9:c1013_11(x))


The following defined symbols remain to be analysed:
ge, GEN, GE, sum, gen

They will be analysed ascendingly in the following order:
ge < GEN
GE < GEN
ge < gen

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s10_11(n424_11), gen_0':s10_11(n424_11)) -> true, rt in Omega(0)

Induction Base:
ge(gen_0':s10_11(0), gen_0':s10_11(0)) ->_R^Omega(0)
true

Induction Step:
ge(gen_0':s10_11(+(n424_11, 1)), gen_0':s10_11(+(n424_11, 1))) ->_R^Omega(0)
ge(gen_0':s10_11(n424_11), gen_0':s10_11(n424_11)) ->_IH
true

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:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10


Lemmas:
SUM(gen_nil:cons12_11(n15_11)) -> gen_c5:c6:c711_11(n15_11), rt in Omega(1 + n15_11)
ge(gen_0':s10_11(n424_11), gen_0':s10_11(n424_11)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c5:c6:c711_11(0) <=> c5
gen_c5:c6:c711_11(+(x, 1)) <=> c6(gen_c5:c6:c711_11(x))
gen_nil:cons12_11(0) <=> nil
gen_nil:cons12_11(+(x, 1)) <=> cons(0', gen_nil:cons12_11(x))
gen_c8:c9:c1013_11(0) <=> c8
gen_c8:c9:c1013_11(+(x, 1)) <=> c10(gen_c8:c9:c1013_11(x))


The following defined symbols remain to be analysed:
GE, GEN, sum, gen

They will be analysed ascendingly in the following order:
GE < GEN

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s10_11(n784_11), gen_0':s10_11(n784_11)) -> gen_c8:c9:c1013_11(n784_11), rt in Omega(1 + n784_11)

Induction Base:
GE(gen_0':s10_11(0), gen_0':s10_11(0)) ->_R^Omega(1)
c8

Induction Step:
GE(gen_0':s10_11(+(n784_11, 1)), gen_0':s10_11(+(n784_11, 1))) ->_R^Omega(1)
c10(GE(gen_0':s10_11(n784_11), gen_0':s10_11(n784_11))) ->_IH
c10(gen_c8:c9:c1013_11(c785_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:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10


Lemmas:
SUM(gen_nil:cons12_11(n15_11)) -> gen_c5:c6:c711_11(n15_11), rt in Omega(1 + n15_11)
ge(gen_0':s10_11(n424_11), gen_0':s10_11(n424_11)) -> true, rt in Omega(0)
GE(gen_0':s10_11(n784_11), gen_0':s10_11(n784_11)) -> gen_c8:c9:c1013_11(n784_11), rt in Omega(1 + n784_11)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c5:c6:c711_11(0) <=> c5
gen_c5:c6:c711_11(+(x, 1)) <=> c6(gen_c5:c6:c711_11(x))
gen_nil:cons12_11(0) <=> nil
gen_nil:cons12_11(+(x, 1)) <=> cons(0', gen_nil:cons12_11(x))
gen_c8:c9:c1013_11(0) <=> c8
gen_c8:c9:c1013_11(+(x, 1)) <=> c10(gen_c8:c9:c1013_11(x))


The following defined symbols remain to be analysed:
GEN, sum, gen
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sum(gen_nil:cons12_11(n1811_11)) -> gen_0':s10_11(0), rt in Omega(0)

Induction Base:
sum(gen_nil:cons12_11(0)) ->_R^Omega(0)
0'

Induction Step:
sum(gen_nil:cons12_11(+(n1811_11, 1))) ->_R^Omega(0)
sum(gen_nil:cons12_11(n1811_11)) ->_IH
gen_0':s10_11(0)

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:
TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c1(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c3
IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2)))
SUM(nil) -> c5
SUM(cons(0', z0)) -> c6(SUM(z0))
SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1)))
GE(z0, 0') -> c8
GE(0', s(z0)) -> c9
GE(s(z0), s(z1)) -> c10(GE(z0, z1))
times(z0, z1) -> sum(generate(z0, z1))
generate(z0, z1) -> gen(z0, z1, 0')
gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2)
if(true, z0, z1, z2) -> nil
if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2)))
sum(nil) -> 0'
sum(cons(0', z0)) -> sum(z0)
sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)

Types:
TIMES :: 0':s -> 0':s -> c
c :: c5:c6:c7 -> c1 -> c
SUM :: nil:cons -> c5:c6:c7
generate :: 0':s -> 0':s -> nil:cons
GENERATE :: 0':s -> 0':s -> c1
c1 :: c2 -> c1
GEN :: 0':s -> 0':s -> 0':s -> c2
0' :: 0':s
c2 :: c3:c4 -> c8:c9:c10 -> c2
IF :: true:false -> 0':s -> 0':s -> 0':s -> c3:c4
ge :: 0':s -> 0':s -> true:false
GE :: 0':s -> 0':s -> c8:c9:c10
true :: true:false
c3 :: c3:c4
false :: true:false
c4 :: c2 -> c3:c4
s :: 0':s -> 0':s
nil :: nil:cons
c5 :: c5:c6:c7
cons :: 0':s -> nil:cons -> nil:cons
c6 :: c5:c6:c7 -> c5:c6:c7
c7 :: c5:c6:c7 -> c5:c6:c7
c8 :: c8:c9:c10
c9 :: c8:c9:c10
c10 :: c8:c9:c10 -> c8:c9:c10
times :: 0':s -> 0':s -> 0':s
sum :: nil:cons -> 0':s
gen :: 0':s -> 0':s -> 0':s -> nil:cons
if :: true:false -> 0':s -> 0':s -> 0':s -> nil:cons
hole_c1_11 :: c
hole_0':s2_11 :: 0':s
hole_c5:c6:c73_11 :: c5:c6:c7
hole_c14_11 :: c1
hole_nil:cons5_11 :: nil:cons
hole_c26_11 :: c2
hole_c3:c47_11 :: c3:c4
hole_c8:c9:c108_11 :: c8:c9:c10
hole_true:false9_11 :: true:false
gen_0':s10_11 :: Nat -> 0':s
gen_c5:c6:c711_11 :: Nat -> c5:c6:c7
gen_nil:cons12_11 :: Nat -> nil:cons
gen_c8:c9:c1013_11 :: Nat -> c8:c9:c10


Lemmas:
SUM(gen_nil:cons12_11(n15_11)) -> gen_c5:c6:c711_11(n15_11), rt in Omega(1 + n15_11)
ge(gen_0':s10_11(n424_11), gen_0':s10_11(n424_11)) -> true, rt in Omega(0)
GE(gen_0':s10_11(n784_11), gen_0':s10_11(n784_11)) -> gen_c8:c9:c1013_11(n784_11), rt in Omega(1 + n784_11)
sum(gen_nil:cons12_11(n1811_11)) -> gen_0':s10_11(0), rt in Omega(0)


Generator Equations:
gen_0':s10_11(0) <=> 0'
gen_0':s10_11(+(x, 1)) <=> s(gen_0':s10_11(x))
gen_c5:c6:c711_11(0) <=> c5
gen_c5:c6:c711_11(+(x, 1)) <=> c6(gen_c5:c6:c711_11(x))
gen_nil:cons12_11(0) <=> nil
gen_nil:cons12_11(+(x, 1)) <=> cons(0', gen_nil:cons12_11(x))
gen_c8:c9:c1013_11(0) <=> c8
gen_c8:c9:c1013_11(+(x, 1)) <=> c10(gen_c8:c9:c1013_11(x))


The following defined symbols remain to be analysed:
gen