WORST_CASE(Omega(n^1),?)
proof of input_DnCc5xc3hO.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), 0 ms]
(10) typed CpxTrs
(11) RewriteLemmaProof [LOWER BOUND(ID), 360 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 161 ms]
(14) BEST
    (15) proven lower bound
        (16) LowerBoundPropagationProof [FINISHED, 0 ms]
        (17) BOUNDS(n^1, INF)
    (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 35 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 94.1 s]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 36 ms]
        (24) 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(xs) -> sum2(xs, 0)
   sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y)
   ifsum(true, b, xs, y) -> y
   ifsum(false, b, xs, y) -> ifsum2(b, xs, y)
   ifsum2(true, xs, y) -> sum2(tail(xs), y)
   ifsum2(false, xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y))
   isNil(nil) -> true
   isNil(cons(x, xs)) -> false
   tail(nil) -> nil
   tail(cons(x, xs)) -> xs
   head(cons(x, xs)) -> x
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(x))) -> isZero(s(x))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(x))) -> s(p(s(x)))
   ge(x, 0) -> true
   ge(0, s(y)) -> false
   ge(s(x), s(y)) -> ge(x, y)
   a -> c
   a -> d

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(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d
Tuples:
   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30
S tuples:
   TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30
K tuples:none
Defined Rule Symbols:   times_2, generate_2, gen_3, if_4, sum_1, sum2_2, ifsum_4, ifsum2_3, isNil_1, tail_1, head_1, isZero_1, p_1, ge_2, a

Defined Pair Symbols:   TIMES_2, GENERATE_2, GEN_3, IF_4, SUM_1, SUM2_2, IFSUM_4, IFSUM2_3, ISNIL_1, TAIL_1, HEAD_1, ISZERO_1, P_1, GE_2, A

Compound Symbols:   c1_2, c2_1, c3_2, c4, c5_1, c6_1, c7_2, c8_3, c9, c10_1, c11_2, c12_3, c13_2, c14, c15, c16, c17, c18, c19, c20, c21, c22_1, c23, c24, c25_1, c26, c27, c28_1, c29, c30


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

(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) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0) -> c20
   ISZERO(s(0)) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0) -> c23
   P(s(0)) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0) -> c26
   GE(0, s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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(z0) -> sum2(z0, 0)
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0) -> true
   isZero(s(0)) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0) -> s(s(0))
   p(s(0)) -> 0
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0) -> true
   ge(0, s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

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) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
   GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
   GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
   IF(true, z0, z1, z2) -> c4
   IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
   SUM(z0) -> c6(SUM2(z0, 0'))
   SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
   SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
   IFSUM(true, z0, z1, z2) -> c9
   IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
   IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
   IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
   IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
   ISNIL(nil) -> c14
   ISNIL(cons(z0, z1)) -> c15
   TAIL(nil) -> c16
   TAIL(cons(z0, z1)) -> c17
   HEAD(cons(z0, z1)) -> c18
   HEAD(nil) -> c19
   ISZERO(0') -> c20
   ISZERO(s(0')) -> c21
   ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
   P(0') -> c23
   P(s(0')) -> c24
   P(s(s(z0))) -> c25(P(s(z0)))
   GE(z0, 0') -> c26
   GE(0', s(z0)) -> c27
   GE(s(z0), s(z1)) -> c28(GE(z0, z1))
   A -> c29
   A -> c30

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(z0) -> sum2(z0, 0')
   sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
   ifsum(true, z0, z1, z2) -> z2
   ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
   ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
   ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
   isNil(nil) -> true
   isNil(cons(z0, z1)) -> false
   tail(nil) -> nil
   tail(cons(z0, z1)) -> z1
   head(cons(z0, z1)) -> z0
   head(nil) -> error
   isZero(0') -> true
   isZero(s(0')) -> false
   isZero(s(s(z0))) -> isZero(s(z0))
   p(0') -> s(s(0'))
   p(s(0')) -> 0'
   p(s(s(z0))) -> s(p(s(z0)))
   ge(z0, 0') -> true
   ge(0', s(z0)) -> false
   ge(s(z0), s(z1)) -> ge(z0, z1)
   a -> c
   a -> d

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

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

(8)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
GEN, ge, GE, SUM2, isZero, ISZERO, p, P, gen, sum2

They will be analysed ascendingly in the following order:
ge < GEN
GE < GEN
ge < gen
isZero < SUM2
ISZERO < SUM2
p < SUM2
P < SUM2
isZero < sum2
p < sum2

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

(10)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
ge, GEN, GE, SUM2, isZero, ISZERO, p, P, gen, sum2

They will be analysed ascendingly in the following order:
ge < GEN
GE < GEN
ge < gen
isZero < SUM2
ISZERO < SUM2
p < SUM2
P < SUM2
isZero < sum2
p < sum2

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)

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

Induction Step:
ge(gen_0':s:error20_31(+(n26_31, 1)), gen_0':s:error20_31(+(n26_31, 1))) ->_R^Omega(0)
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) ->_IH
true

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

(12)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Lemmas:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
GE, GEN, SUM2, isZero, ISZERO, p, P, gen, sum2

They will be analysed ascendingly in the following order:
GE < GEN
isZero < SUM2
ISZERO < SUM2
p < SUM2
P < SUM2
isZero < sum2
p < sum2

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GE(gen_0':s:error20_31(n648_31), gen_0':s:error20_31(n648_31)) -> gen_c26:c27:c2822_31(n648_31), rt in Omega(1 + n648_31)

Induction Base:
GE(gen_0':s:error20_31(0), gen_0':s:error20_31(0)) ->_R^Omega(1)
c26

Induction Step:
GE(gen_0':s:error20_31(+(n648_31, 1)), gen_0':s:error20_31(+(n648_31, 1))) ->_R^Omega(1)
c28(GE(gen_0':s:error20_31(n648_31), gen_0':s:error20_31(n648_31))) ->_IH
c28(gen_c26:c27:c2822_31(c649_31))

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

(14)
Complex Obligation (BEST)

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

(15)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Lemmas:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
GE, GEN, SUM2, isZero, ISZERO, p, P, gen, sum2

They will be analysed ascendingly in the following order:
GE < GEN
isZero < SUM2
ISZERO < SUM2
p < SUM2
P < SUM2
isZero < sum2
p < sum2

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

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

(17)
BOUNDS(n^1, INF)

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

(18)
Obligation:
Innermost TRS:
Rules:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Lemmas:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)
GE(gen_0':s:error20_31(n648_31), gen_0':s:error20_31(n648_31)) -> gen_c26:c27:c2822_31(n648_31), rt in Omega(1 + n648_31)


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
GEN, SUM2, isZero, ISZERO, p, P, gen, sum2

They will be analysed ascendingly in the following order:
isZero < SUM2
ISZERO < SUM2
p < SUM2
P < SUM2
isZero < sum2
p < sum2

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
isZero(gen_0':s:error20_31(+(1, n2022_31))) -> false, rt in Omega(0)

Induction Base:
isZero(gen_0':s:error20_31(+(1, 0))) ->_R^Omega(0)
false

Induction Step:
isZero(gen_0':s:error20_31(+(1, +(n2022_31, 1)))) ->_R^Omega(0)
isZero(s(gen_0':s:error20_31(n2022_31))) ->_IH
false

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:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Lemmas:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)
GE(gen_0':s:error20_31(n648_31), gen_0':s:error20_31(n648_31)) -> gen_c26:c27:c2822_31(n648_31), rt in Omega(1 + n648_31)
isZero(gen_0':s:error20_31(+(1, n2022_31))) -> false, rt in Omega(0)


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
ISZERO, SUM2, p, P, gen, sum2

They will be analysed ascendingly in the following order:
ISZERO < SUM2
p < SUM2
P < SUM2
p < sum2

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
ISZERO(gen_0':s:error20_31(+(2, n2323_31))) -> *25_31, rt in Omega(n2323_31)

Induction Base:
ISZERO(gen_0':s:error20_31(+(2, 0)))

Induction Step:
ISZERO(gen_0':s:error20_31(+(2, +(n2323_31, 1)))) ->_R^Omega(1)
c22(ISZERO(s(gen_0':s:error20_31(+(1, n2323_31))))) ->_IH
c22(*25_31)

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:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Lemmas:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)
GE(gen_0':s:error20_31(n648_31), gen_0':s:error20_31(n648_31)) -> gen_c26:c27:c2822_31(n648_31), rt in Omega(1 + n648_31)
isZero(gen_0':s:error20_31(+(1, n2022_31))) -> false, rt in Omega(0)
ISZERO(gen_0':s:error20_31(+(2, n2323_31))) -> *25_31, rt in Omega(n2323_31)


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
p, SUM2, P, gen, sum2

They will be analysed ascendingly in the following order:
p < SUM2
P < SUM2
p < sum2

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

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
p(gen_0':s:error20_31(+(1, n75289_31))) -> gen_0':s:error20_31(n75289_31), rt in Omega(0)

Induction Base:
p(gen_0':s:error20_31(+(1, 0))) ->_R^Omega(0)
0'

Induction Step:
p(gen_0':s:error20_31(+(1, +(n75289_31, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s:error20_31(n75289_31)))) ->_IH
s(gen_0':s:error20_31(c75290_31))

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:
TIMES(z0, z1) -> c1(SUM(generate(z0, z1)), GENERATE(z0, z1))
GENERATE(z0, z1) -> c2(GEN(z0, z1, 0'))
GEN(z0, z1, z2) -> c3(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0))
IF(true, z0, z1, z2) -> c4
IF(false, z0, z1, z2) -> c5(GEN(z0, z1, s(z2)))
SUM(z0) -> c6(SUM2(z0, 0'))
SUM2(z0, z1) -> c7(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISNIL(z0))
SUM2(z0, z1) -> c8(IFSUM(isNil(z0), isZero(head(z0)), z0, z1), ISZERO(head(z0)), HEAD(z0))
IFSUM(true, z0, z1, z2) -> c9
IFSUM(false, z0, z1, z2) -> c10(IFSUM2(z0, z1, z2))
IFSUM2(true, z0, z1) -> c11(SUM2(tail(z0), z1), TAIL(z0))
IFSUM2(false, z0, z1) -> c12(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), P(head(z0)), HEAD(z0))
IFSUM2(false, z0, z1) -> c13(SUM2(cons(p(head(z0)), tail(z0)), s(z1)), TAIL(z0))
ISNIL(nil) -> c14
ISNIL(cons(z0, z1)) -> c15
TAIL(nil) -> c16
TAIL(cons(z0, z1)) -> c17
HEAD(cons(z0, z1)) -> c18
HEAD(nil) -> c19
ISZERO(0') -> c20
ISZERO(s(0')) -> c21
ISZERO(s(s(z0))) -> c22(ISZERO(s(z0)))
P(0') -> c23
P(s(0')) -> c24
P(s(s(z0))) -> c25(P(s(z0)))
GE(z0, 0') -> c26
GE(0', s(z0)) -> c27
GE(s(z0), s(z1)) -> c28(GE(z0, z1))
A -> c29
A -> c30
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(z0) -> sum2(z0, 0')
sum2(z0, z1) -> ifsum(isNil(z0), isZero(head(z0)), z0, z1)
ifsum(true, z0, z1, z2) -> z2
ifsum(false, z0, z1, z2) -> ifsum2(z0, z1, z2)
ifsum2(true, z0, z1) -> sum2(tail(z0), z1)
ifsum2(false, z0, z1) -> sum2(cons(p(head(z0)), tail(z0)), s(z1))
isNil(nil) -> true
isNil(cons(z0, z1)) -> false
tail(nil) -> nil
tail(cons(z0, z1)) -> z1
head(cons(z0, z1)) -> z0
head(nil) -> error
isZero(0') -> true
isZero(s(0')) -> false
isZero(s(s(z0))) -> isZero(s(z0))
p(0') -> s(s(0'))
p(s(0')) -> 0'
p(s(s(z0))) -> s(p(s(z0)))
ge(z0, 0') -> true
ge(0', s(z0)) -> false
ge(s(z0), s(z1)) -> ge(z0, z1)
a -> c
a -> d

Types:
TIMES :: 0':s:error -> 0':s:error -> c1
c1 :: c6 -> c2 -> c1
SUM :: cons:nil -> c6
generate :: 0':s:error -> 0':s:error -> cons:nil
GENERATE :: 0':s:error -> 0':s:error -> c2
c2 :: c3 -> c2
GEN :: 0':s:error -> 0':s:error -> 0':s:error -> c3
0' :: 0':s:error
c3 :: c4:c5 -> c26:c27:c28 -> c3
IF :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c4:c5
ge :: 0':s:error -> 0':s:error -> true:false
GE :: 0':s:error -> 0':s:error -> c26:c27:c28
true :: true:false
c4 :: c4:c5
false :: true:false
c5 :: c3 -> c4:c5
s :: 0':s:error -> 0':s:error
c6 :: c7:c8 -> c6
SUM2 :: cons:nil -> 0':s:error -> c7:c8
c7 :: c9:c10 -> c14:c15 -> c7:c8
IFSUM :: true:false -> true:false -> cons:nil -> 0':s:error -> c9:c10
isNil :: cons:nil -> true:false
isZero :: 0':s:error -> true:false
head :: cons:nil -> 0':s:error
ISNIL :: cons:nil -> c14:c15
c8 :: c9:c10 -> c20:c21:c22 -> c18:c19 -> c7:c8
ISZERO :: 0':s:error -> c20:c21:c22
HEAD :: cons:nil -> c18:c19
c9 :: c9:c10
c10 :: c11:c12:c13 -> c9:c10
IFSUM2 :: true:false -> cons:nil -> 0':s:error -> c11:c12:c13
c11 :: c7:c8 -> c16:c17 -> c11:c12:c13
tail :: cons:nil -> cons:nil
TAIL :: cons:nil -> c16:c17
c12 :: c7:c8 -> c23:c24:c25 -> c18:c19 -> c11:c12:c13
cons :: 0':s:error -> cons:nil -> cons:nil
p :: 0':s:error -> 0':s:error
P :: 0':s:error -> c23:c24:c25
c13 :: c7:c8 -> c16:c17 -> c11:c12:c13
nil :: cons:nil
c14 :: c14:c15
c15 :: c14:c15
c16 :: c16:c17
c17 :: c16:c17
c18 :: c18:c19
c19 :: c18:c19
c20 :: c20:c21:c22
c21 :: c20:c21:c22
c22 :: c20:c21:c22 -> c20:c21:c22
c23 :: c23:c24:c25
c24 :: c23:c24:c25
c25 :: c23:c24:c25 -> c23:c24:c25
c26 :: c26:c27:c28
c27 :: c26:c27:c28
c28 :: c26:c27:c28 -> c26:c27:c28
A :: c29:c30
c29 :: c29:c30
c30 :: c29:c30
times :: 0':s:error -> 0':s:error -> 0':s:error
sum :: cons:nil -> 0':s:error
gen :: 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
if :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> cons:nil
sum2 :: cons:nil -> 0':s:error -> 0':s:error
ifsum :: true:false -> true:false -> cons:nil -> 0':s:error -> 0':s:error
ifsum2 :: true:false -> cons:nil -> 0':s:error -> 0':s:error
error :: 0':s:error
a :: c:d
c :: c:d
d :: c:d
hole_c11_31 :: c1
hole_0':s:error2_31 :: 0':s:error
hole_c63_31 :: c6
hole_c24_31 :: c2
hole_cons:nil5_31 :: cons:nil
hole_c36_31 :: c3
hole_c4:c57_31 :: c4:c5
hole_c26:c27:c288_31 :: c26:c27:c28
hole_true:false9_31 :: true:false
hole_c7:c810_31 :: c7:c8
hole_c9:c1011_31 :: c9:c10
hole_c14:c1512_31 :: c14:c15
hole_c20:c21:c2213_31 :: c20:c21:c22
hole_c18:c1914_31 :: c18:c19
hole_c11:c12:c1315_31 :: c11:c12:c13
hole_c16:c1716_31 :: c16:c17
hole_c23:c24:c2517_31 :: c23:c24:c25
hole_c29:c3018_31 :: c29:c30
hole_c:d19_31 :: c:d
gen_0':s:error20_31 :: Nat -> 0':s:error
gen_cons:nil21_31 :: Nat -> cons:nil
gen_c26:c27:c2822_31 :: Nat -> c26:c27:c28
gen_c20:c21:c2223_31 :: Nat -> c20:c21:c22
gen_c23:c24:c2524_31 :: Nat -> c23:c24:c25


Lemmas:
ge(gen_0':s:error20_31(n26_31), gen_0':s:error20_31(n26_31)) -> true, rt in Omega(0)
GE(gen_0':s:error20_31(n648_31), gen_0':s:error20_31(n648_31)) -> gen_c26:c27:c2822_31(n648_31), rt in Omega(1 + n648_31)
isZero(gen_0':s:error20_31(+(1, n2022_31))) -> false, rt in Omega(0)
ISZERO(gen_0':s:error20_31(+(2, n2323_31))) -> *25_31, rt in Omega(n2323_31)
p(gen_0':s:error20_31(+(1, n75289_31))) -> gen_0':s:error20_31(n75289_31), rt in Omega(0)


Generator Equations:
gen_0':s:error20_31(0) <=> 0'
gen_0':s:error20_31(+(x, 1)) <=> s(gen_0':s:error20_31(x))
gen_cons:nil21_31(0) <=> nil
gen_cons:nil21_31(+(x, 1)) <=> cons(0', gen_cons:nil21_31(x))
gen_c26:c27:c2822_31(0) <=> c26
gen_c26:c27:c2822_31(+(x, 1)) <=> c28(gen_c26:c27:c2822_31(x))
gen_c20:c21:c2223_31(0) <=> c20
gen_c20:c21:c2223_31(+(x, 1)) <=> c22(gen_c20:c21:c2223_31(x))
gen_c23:c24:c2524_31(0) <=> c23
gen_c23:c24:c2524_31(+(x, 1)) <=> c25(gen_c23:c24:c2524_31(x))


The following defined symbols remain to be analysed:
P, SUM2, gen, sum2

They will be analysed ascendingly in the following order:
P < SUM2