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


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, 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), 2 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), 322 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), 47 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 34 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 15 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 3360 ms]
        (24) BEST
            (25) proven lower bound
                (26) LowerBoundPropagationProof [FINISHED, 0 ms]
                (27) BOUNDS(n^2, INF)
            (28) typed CpxTrs
                (29) RewriteLemmaProof [LOWER BOUND(ID), 225 ms]
                (30) BOUNDS(1, INF)


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

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


The TRS R consists of the following rules:

   isEmpty(cons(x, xs)) -> false
   isEmpty(nil) -> true
   isZero(0) -> true
   isZero(s(x)) -> false
   head(cons(x, xs)) -> x
   tail(cons(x, xs)) -> xs
   tail(nil) -> nil
   p(s(s(x))) -> s(p(s(x)))
   p(s(0)) -> 0
   p(0) -> 0
   inc(s(x)) -> s(inc(x))
   inc(0) -> s(0)
   sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))
   if(true, b, y, xs, ys, x) -> y
   if(false, true, y, xs, ys, x) -> sumList(xs, y)
   if(false, false, y, xs, ys, x) -> sumList(ys, x)
   sum(xs) -> sumList(xs, 0)

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:
   isEmpty(cons(z0, z1)) -> false
   isEmpty(nil) -> true
   isZero(0) -> true
   isZero(s(z0)) -> false
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
   tail(nil) -> nil
   p(s(s(z0))) -> s(p(s(z0)))
   p(s(0)) -> 0
   p(0) -> 0
   inc(s(z0)) -> s(inc(z0))
   inc(0) -> s(0)
   sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
   if(true, z0, z1, z2, z3, z4) -> z1
   if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
   if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
   sum(z0) -> sumList(z0, 0)
Tuples:
   ISEMPTY(cons(z0, z1)) -> c
   ISEMPTY(nil) -> c1
   ISZERO(0) -> c2
   ISZERO(s(z0)) -> c3
   HEAD(cons(z0, z1)) -> c4
   TAIL(cons(z0, z1)) -> c5
   TAIL(nil) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   P(s(0)) -> c8
   P(0) -> c9
   INC(s(z0)) -> c10(INC(z0))
   INC(0) -> c11
   SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
   SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
   IF(true, z0, z1, z2, z3, z4) -> c18
   IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
   IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
   SUM(z0) -> c21(SUMLIST(z0, 0))
S tuples:
   ISEMPTY(cons(z0, z1)) -> c
   ISEMPTY(nil) -> c1
   ISZERO(0) -> c2
   ISZERO(s(z0)) -> c3
   HEAD(cons(z0, z1)) -> c4
   TAIL(cons(z0, z1)) -> c5
   TAIL(nil) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   P(s(0)) -> c8
   P(0) -> c9
   INC(s(z0)) -> c10(INC(z0))
   INC(0) -> c11
   SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
   SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
   IF(true, z0, z1, z2, z3, z4) -> c18
   IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
   IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
   SUM(z0) -> c21(SUMLIST(z0, 0))
K tuples:none
Defined Rule Symbols:   isEmpty_1, isZero_1, head_1, tail_1, p_1, inc_1, sumList_2, if_6, sum_1

Defined Pair Symbols:   ISEMPTY_1, ISZERO_1, HEAD_1, TAIL_1, P_1, INC_1, SUMLIST_2, IF_6, SUM_1

Compound Symbols:   c, c1, c2, c3, c4, c5, c6, c7_1, c8, c9, c10_1, c11, c12_2, c13_3, c14_2, c15_3, c16_2, c17_2, c18, c19_1, c20_1, c21_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^2, INF).


The TRS R consists of the following rules:

   ISEMPTY(cons(z0, z1)) -> c
   ISEMPTY(nil) -> c1
   ISZERO(0) -> c2
   ISZERO(s(z0)) -> c3
   HEAD(cons(z0, z1)) -> c4
   TAIL(cons(z0, z1)) -> c5
   TAIL(nil) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   P(s(0)) -> c8
   P(0) -> c9
   INC(s(z0)) -> c10(INC(z0))
   INC(0) -> c11
   SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
   SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
   IF(true, z0, z1, z2, z3, z4) -> c18
   IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
   IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
   SUM(z0) -> c21(SUMLIST(z0, 0))

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

   isEmpty(cons(z0, z1)) -> false
   isEmpty(nil) -> true
   isZero(0) -> true
   isZero(s(z0)) -> false
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
   tail(nil) -> nil
   p(s(s(z0))) -> s(p(s(z0)))
   p(s(0)) -> 0
   p(0) -> 0
   inc(s(z0)) -> s(inc(z0))
   inc(0) -> s(0)
   sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
   if(true, z0, z1, z2, z3, z4) -> z1
   if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
   if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
   sum(z0) -> sumList(z0, 0)

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


The TRS R consists of the following rules:

   ISEMPTY(cons(z0, z1)) -> c
   ISEMPTY(nil) -> c1
   ISZERO(0') -> c2
   ISZERO(s(z0)) -> c3
   HEAD(cons(z0, z1)) -> c4
   TAIL(cons(z0, z1)) -> c5
   TAIL(nil) -> c6
   P(s(s(z0))) -> c7(P(s(z0)))
   P(s(0')) -> c8
   P(0') -> c9
   INC(s(z0)) -> c10(INC(z0))
   INC(0') -> c11
   SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
   SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
   SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
   SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
   IF(true, z0, z1, z2, z3, z4) -> c18
   IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
   IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
   SUM(z0) -> c21(SUMLIST(z0, 0'))

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

   isEmpty(cons(z0, z1)) -> false
   isEmpty(nil) -> true
   isZero(0') -> true
   isZero(s(z0)) -> false
   head(cons(z0, z1)) -> z0
   tail(cons(z0, z1)) -> z1
   tail(nil) -> nil
   p(s(s(z0))) -> s(p(s(z0)))
   p(s(0')) -> 0'
   p(0') -> 0'
   inc(s(z0)) -> s(inc(z0))
   inc(0') -> s(0')
   sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
   if(true, z0, z1, z2, z3, z4) -> z1
   if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
   if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
   sum(z0) -> sumList(z0, 0')

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

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

(8)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
P, INC, SUMLIST, p, inc, sumList

They will be analysed ascendingly in the following order:
P < SUMLIST
INC < SUMLIST
p < SUMLIST
inc < SUMLIST
p < sumList
inc < sumList

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

(10)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
P, INC, SUMLIST, p, inc, sumList

They will be analysed ascendingly in the following order:
P < SUMLIST
INC < SUMLIST
p < SUMLIST
inc < SUMLIST
p < sumList
inc < sumList

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)

Induction Base:
P(gen_0':s14_22(+(1, 0))) ->_R^Omega(1)
c8

Induction Step:
P(gen_0':s14_22(+(1, +(n18_22, 1)))) ->_R^Omega(1)
c7(P(s(gen_0':s14_22(n18_22)))) ->_IH
c7(gen_c7:c8:c915_22(c19_22))

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:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
P, INC, SUMLIST, p, inc, sumList

They will be analysed ascendingly in the following order:
P < SUMLIST
INC < SUMLIST
p < SUMLIST
inc < SUMLIST
p < sumList
inc < sumList

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

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

(15)
BOUNDS(n^1, INF)

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

(16)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Lemmas:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
INC, SUMLIST, p, inc, sumList

They will be analysed ascendingly in the following order:
INC < SUMLIST
p < SUMLIST
inc < SUMLIST
p < sumList
inc < sumList

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INC(gen_0':s14_22(n445_22)) -> gen_c10:c1116_22(n445_22), rt in Omega(1 + n445_22)

Induction Base:
INC(gen_0':s14_22(0)) ->_R^Omega(1)
c11

Induction Step:
INC(gen_0':s14_22(+(n445_22, 1))) ->_R^Omega(1)
c10(INC(gen_0':s14_22(n445_22))) ->_IH
c10(gen_c10:c1116_22(c446_22))

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

(18)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Lemmas:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)
INC(gen_0':s14_22(n445_22)) -> gen_c10:c1116_22(n445_22), rt in Omega(1 + n445_22)


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
p, SUMLIST, inc, sumList

They will be analysed ascendingly in the following order:
p < SUMLIST
inc < SUMLIST
p < sumList
inc < sumList

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
p(gen_0':s14_22(+(1, n903_22))) -> gen_0':s14_22(n903_22), rt in Omega(0)

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

Induction Step:
p(gen_0':s14_22(+(1, +(n903_22, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s14_22(n903_22)))) ->_IH
s(gen_0':s14_22(c904_22))

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:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Lemmas:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)
INC(gen_0':s14_22(n445_22)) -> gen_c10:c1116_22(n445_22), rt in Omega(1 + n445_22)
p(gen_0':s14_22(+(1, n903_22))) -> gen_0':s14_22(n903_22), rt in Omega(0)


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
inc, SUMLIST, sumList

They will be analysed ascendingly in the following order:
inc < SUMLIST
inc < sumList

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
inc(gen_0':s14_22(n1312_22)) -> gen_0':s14_22(+(1, n1312_22)), rt in Omega(0)

Induction Base:
inc(gen_0':s14_22(0)) ->_R^Omega(0)
s(0')

Induction Step:
inc(gen_0':s14_22(+(n1312_22, 1))) ->_R^Omega(0)
s(inc(gen_0':s14_22(n1312_22))) ->_IH
s(gen_0':s14_22(+(1, c1313_22)))

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:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Lemmas:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)
INC(gen_0':s14_22(n445_22)) -> gen_c10:c1116_22(n445_22), rt in Omega(1 + n445_22)
p(gen_0':s14_22(+(1, n903_22))) -> gen_0':s14_22(n903_22), rt in Omega(0)
inc(gen_0':s14_22(n1312_22)) -> gen_0':s14_22(+(1, n1312_22)), rt in Omega(0)


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
SUMLIST, sumList
----------------------------------------

(23) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
SUMLIST(gen_cons:nil13_22(n1723_22), gen_0':s14_22(b)) -> *17_22, rt in Omega(b*n1723_22 + n1723_22)

Induction Base:
SUMLIST(gen_cons:nil13_22(0), gen_0':s14_22(b))

Induction Step:
SUMLIST(gen_cons:nil13_22(+(n1723_22, 1)), gen_0':s14_22(b)) ->_R^Omega(1)
c17(IF(isEmpty(gen_cons:nil13_22(+(n1723_22, 1))), isZero(head(gen_cons:nil13_22(+(n1723_22, 1)))), gen_0':s14_22(b), tail(gen_cons:nil13_22(+(n1723_22, 1))), cons(p(head(gen_cons:nil13_22(+(n1723_22, 1)))), tail(gen_cons:nil13_22(+(n1723_22, 1)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, isZero(head(gen_cons:nil13_22(+(1, n1723_22)))), gen_0':s14_22(b), tail(gen_cons:nil13_22(+(1, n1723_22))), cons(p(head(gen_cons:nil13_22(+(1, n1723_22)))), tail(gen_cons:nil13_22(+(1, n1723_22)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, isZero(0'), gen_0':s14_22(b), tail(gen_cons:nil13_22(+(1, n1723_22))), cons(p(head(gen_cons:nil13_22(+(1, n1723_22)))), tail(gen_cons:nil13_22(+(1, n1723_22)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, true, gen_0':s14_22(b), tail(gen_cons:nil13_22(+(1, n1723_22))), cons(p(head(gen_cons:nil13_22(+(1, n1723_22)))), tail(gen_cons:nil13_22(+(1, n1723_22)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n1723_22), cons(p(head(gen_cons:nil13_22(+(1, n1723_22)))), tail(gen_cons:nil13_22(+(1, n1723_22)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n1723_22), cons(p(0'), tail(gen_cons:nil13_22(+(1, n1723_22)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n1723_22), cons(0', tail(gen_cons:nil13_22(+(1, n1723_22)))), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_R^Omega(0)
c17(IF(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n1723_22), cons(0', gen_cons:nil13_22(n1723_22)), inc(gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_L^Omega(0)
c17(IF(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n1723_22), cons(0', gen_cons:nil13_22(n1723_22)), gen_0':s14_22(+(1, b))), INC(gen_0':s14_22(b))) ->_R^Omega(1)
c17(c19(SUMLIST(gen_cons:nil13_22(n1723_22), gen_0':s14_22(b))), INC(gen_0':s14_22(b))) ->_IH
c17(c19(*17_22), INC(gen_0':s14_22(b))) ->_L^Omega(1 + b)
c17(c19(*17_22), gen_c10:c1116_22(b))

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

(24)
Complex Obligation (BEST)

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

(25)
Obligation:
Proved the lower bound n^2 for the following obligation:

Innermost TRS:
Rules:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Lemmas:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)
INC(gen_0':s14_22(n445_22)) -> gen_c10:c1116_22(n445_22), rt in Omega(1 + n445_22)
p(gen_0':s14_22(+(1, n903_22))) -> gen_0':s14_22(n903_22), rt in Omega(0)
inc(gen_0':s14_22(n1312_22)) -> gen_0':s14_22(+(1, n1312_22)), rt in Omega(0)


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


The following defined symbols remain to be analysed:
SUMLIST, sumList
----------------------------------------

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

(27)
BOUNDS(n^2, INF)

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

(28)
Obligation:
Innermost TRS:
Rules:
ISEMPTY(cons(z0, z1)) -> c
ISEMPTY(nil) -> c1
ISZERO(0') -> c2
ISZERO(s(z0)) -> c3
HEAD(cons(z0, z1)) -> c4
TAIL(cons(z0, z1)) -> c5
TAIL(nil) -> c6
P(s(s(z0))) -> c7(P(s(z0)))
P(s(0')) -> c8
P(0') -> c9
INC(s(z0)) -> c10(INC(z0))
INC(0') -> c11
SUMLIST(z0, z1) -> c12(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISEMPTY(z0))
SUMLIST(z0, z1) -> c13(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), ISZERO(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c14(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c15(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), P(head(z0)), HEAD(z0))
SUMLIST(z0, z1) -> c16(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), TAIL(z0))
SUMLIST(z0, z1) -> c17(IF(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1)), INC(z1))
IF(true, z0, z1, z2, z3, z4) -> c18
IF(false, true, z0, z1, z2, z3) -> c19(SUMLIST(z1, z0))
IF(false, false, z0, z1, z2, z3) -> c20(SUMLIST(z2, z3))
SUM(z0) -> c21(SUMLIST(z0, 0'))
isEmpty(cons(z0, z1)) -> false
isEmpty(nil) -> true
isZero(0') -> true
isZero(s(z0)) -> false
head(cons(z0, z1)) -> z0
tail(cons(z0, z1)) -> z1
tail(nil) -> nil
p(s(s(z0))) -> s(p(s(z0)))
p(s(0')) -> 0'
p(0') -> 0'
inc(s(z0)) -> s(inc(z0))
inc(0') -> s(0')
sumList(z0, z1) -> if(isEmpty(z0), isZero(head(z0)), z1, tail(z0), cons(p(head(z0)), tail(z0)), inc(z1))
if(true, z0, z1, z2, z3, z4) -> z1
if(false, true, z0, z1, z2, z3) -> sumList(z1, z0)
if(false, false, z0, z1, z2, z3) -> sumList(z2, z3)
sum(z0) -> sumList(z0, 0')

Types:
ISEMPTY :: cons:nil -> c:c1
cons :: 0':s -> cons:nil -> cons:nil
c :: c:c1
nil :: cons:nil
c1 :: c:c1
ISZERO :: 0':s -> c2:c3
0' :: 0':s
c2 :: c2:c3
s :: 0':s -> 0':s
c3 :: c2:c3
HEAD :: cons:nil -> c4
c4 :: c4
TAIL :: cons:nil -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
P :: 0':s -> c7:c8:c9
c7 :: c7:c8:c9 -> c7:c8:c9
c8 :: c7:c8:c9
c9 :: c7:c8:c9
INC :: 0':s -> c10:c11
c10 :: c10:c11 -> c10:c11
c11 :: c10:c11
SUMLIST :: cons:nil -> 0':s -> c12:c13:c14:c15:c16:c17
c12 :: c18:c19:c20 -> c:c1 -> c12:c13:c14:c15:c16:c17
IF :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> c18:c19:c20
isEmpty :: cons:nil -> true:false
isZero :: 0':s -> true:false
head :: cons:nil -> 0':s
tail :: cons:nil -> cons:nil
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
c13 :: c18:c19:c20 -> c2:c3 -> c4 -> c12:c13:c14:c15:c16:c17
c14 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c15 :: c18:c19:c20 -> c7:c8:c9 -> c4 -> c12:c13:c14:c15:c16:c17
c16 :: c18:c19:c20 -> c5:c6 -> c12:c13:c14:c15:c16:c17
c17 :: c18:c19:c20 -> c10:c11 -> c12:c13:c14:c15:c16:c17
true :: true:false
c18 :: c18:c19:c20
false :: true:false
c19 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
c20 :: c12:c13:c14:c15:c16:c17 -> c18:c19:c20
SUM :: cons:nil -> c21
c21 :: c12:c13:c14:c15:c16:c17 -> c21
sumList :: cons:nil -> 0':s -> 0':s
if :: true:false -> true:false -> 0':s -> cons:nil -> cons:nil -> 0':s -> 0':s
sum :: cons:nil -> 0':s
hole_c:c11_22 :: c:c1
hole_cons:nil2_22 :: cons:nil
hole_0':s3_22 :: 0':s
hole_c2:c34_22 :: c2:c3
hole_c45_22 :: c4
hole_c5:c66_22 :: c5:c6
hole_c7:c8:c97_22 :: c7:c8:c9
hole_c10:c118_22 :: c10:c11
hole_c12:c13:c14:c15:c16:c179_22 :: c12:c13:c14:c15:c16:c17
hole_c18:c19:c2010_22 :: c18:c19:c20
hole_true:false11_22 :: true:false
hole_c2112_22 :: c21
gen_cons:nil13_22 :: Nat -> cons:nil
gen_0':s14_22 :: Nat -> 0':s
gen_c7:c8:c915_22 :: Nat -> c7:c8:c9
gen_c10:c1116_22 :: Nat -> c10:c11


Lemmas:
P(gen_0':s14_22(+(1, n18_22))) -> gen_c7:c8:c915_22(n18_22), rt in Omega(1 + n18_22)
INC(gen_0':s14_22(n445_22)) -> gen_c10:c1116_22(n445_22), rt in Omega(1 + n445_22)
p(gen_0':s14_22(+(1, n903_22))) -> gen_0':s14_22(n903_22), rt in Omega(0)
inc(gen_0':s14_22(n1312_22)) -> gen_0':s14_22(+(1, n1312_22)), rt in Omega(0)
SUMLIST(gen_cons:nil13_22(n1723_22), gen_0':s14_22(b)) -> *17_22, rt in Omega(b*n1723_22 + n1723_22)


Generator Equations:
gen_cons:nil13_22(0) <=> nil
gen_cons:nil13_22(+(x, 1)) <=> cons(0', gen_cons:nil13_22(x))
gen_0':s14_22(0) <=> 0'
gen_0':s14_22(+(x, 1)) <=> s(gen_0':s14_22(x))
gen_c7:c8:c915_22(0) <=> c8
gen_c7:c8:c915_22(+(x, 1)) <=> c7(gen_c7:c8:c915_22(x))
gen_c10:c1116_22(0) <=> c11
gen_c10:c1116_22(+(x, 1)) <=> c10(gen_c10:c1116_22(x))


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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
sumList(gen_cons:nil13_22(n107350_22), gen_0':s14_22(b)) -> gen_0':s14_22(b), rt in Omega(0)

Induction Base:
sumList(gen_cons:nil13_22(0), gen_0':s14_22(b)) ->_R^Omega(0)
if(isEmpty(gen_cons:nil13_22(0)), isZero(head(gen_cons:nil13_22(0))), gen_0':s14_22(b), tail(gen_cons:nil13_22(0)), cons(p(head(gen_cons:nil13_22(0))), tail(gen_cons:nil13_22(0))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(true, isZero(head(gen_cons:nil13_22(0))), gen_0':s14_22(b), tail(gen_cons:nil13_22(0)), cons(p(head(gen_cons:nil13_22(0))), tail(gen_cons:nil13_22(0))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(true, isZero(head(gen_cons:nil13_22(0))), gen_0':s14_22(b), nil, cons(p(head(gen_cons:nil13_22(0))), tail(gen_cons:nil13_22(0))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(true, isZero(head(gen_cons:nil13_22(0))), gen_0':s14_22(b), nil, cons(p(head(gen_cons:nil13_22(0))), nil), inc(gen_0':s14_22(b))) ->_L^Omega(0)
if(true, isZero(head(gen_cons:nil13_22(0))), gen_0':s14_22(b), nil, cons(p(head(gen_cons:nil13_22(0))), nil), gen_0':s14_22(+(1, b))) ->_R^Omega(0)
gen_0':s14_22(b)

Induction Step:
sumList(gen_cons:nil13_22(+(n107350_22, 1)), gen_0':s14_22(b)) ->_R^Omega(0)
if(isEmpty(gen_cons:nil13_22(+(n107350_22, 1))), isZero(head(gen_cons:nil13_22(+(n107350_22, 1)))), gen_0':s14_22(b), tail(gen_cons:nil13_22(+(n107350_22, 1))), cons(p(head(gen_cons:nil13_22(+(n107350_22, 1)))), tail(gen_cons:nil13_22(+(n107350_22, 1)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, isZero(head(gen_cons:nil13_22(+(1, n107350_22)))), gen_0':s14_22(b), tail(gen_cons:nil13_22(+(1, n107350_22))), cons(p(head(gen_cons:nil13_22(+(1, n107350_22)))), tail(gen_cons:nil13_22(+(1, n107350_22)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, isZero(0'), gen_0':s14_22(b), tail(gen_cons:nil13_22(+(1, n107350_22))), cons(p(head(gen_cons:nil13_22(+(1, n107350_22)))), tail(gen_cons:nil13_22(+(1, n107350_22)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, true, gen_0':s14_22(b), tail(gen_cons:nil13_22(+(1, n107350_22))), cons(p(head(gen_cons:nil13_22(+(1, n107350_22)))), tail(gen_cons:nil13_22(+(1, n107350_22)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n107350_22), cons(p(head(gen_cons:nil13_22(+(1, n107350_22)))), tail(gen_cons:nil13_22(+(1, n107350_22)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n107350_22), cons(p(0'), tail(gen_cons:nil13_22(+(1, n107350_22)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n107350_22), cons(0', tail(gen_cons:nil13_22(+(1, n107350_22)))), inc(gen_0':s14_22(b))) ->_R^Omega(0)
if(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n107350_22), cons(0', gen_cons:nil13_22(n107350_22)), inc(gen_0':s14_22(b))) ->_L^Omega(0)
if(false, true, gen_0':s14_22(b), gen_cons:nil13_22(n107350_22), cons(0', gen_cons:nil13_22(n107350_22)), gen_0':s14_22(+(1, b))) ->_R^Omega(0)
sumList(gen_cons:nil13_22(n107350_22), gen_0':s14_22(b)) ->_IH
gen_0':s14_22(b)

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

(30)
BOUNDS(1, INF)