WORST_CASE(Omega(n^1),?)
proof of input_Ta7FKu5q7l.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), 67 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), 312 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), 41 ms]
        (18) typed CpxTrs
        (19) RewriteLemmaProof [LOWER BOUND(ID), 71 ms]
        (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 39 ms]
        (22) typed CpxTrs
        (23) RewriteLemmaProof [LOWER BOUND(ID), 66 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:

   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
   append(nil, x) -> cons(x, nil)
   append(cons(y, ys), x) -> cons(y, append(ys, x))
   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)
   addLists(xs, ys, zs) -> if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
   if(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
   if(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
   if(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
   if(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists(xs2, ys2, zs)
   if(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists(xs, ys, zs2)
   addList(xs, ys) -> addLists(xs, ys, nil)

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
   append(nil, z0) -> cons(z0, nil)
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   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)
   addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
   if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
   if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
   if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
   if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
   if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
   addList(z0, z1) -> addLists(z0, z1, nil)
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
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   P(s(s(z0))) -> c9(P(s(z0)))
   P(s(0)) -> c10
   P(0) -> c11
   INC(s(z0)) -> c12(INC(z0))
   INC(0) -> c13
   ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
   ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
   ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
   ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
   IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
   IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
   IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
   IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
   IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
   ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   P(s(s(z0))) -> c9(P(s(z0)))
   P(s(0)) -> c10
   P(0) -> c11
   INC(s(z0)) -> c12(INC(z0))
   INC(0) -> c13
   ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
   ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
   ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
   ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
   IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
   IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
   IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
   IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
   IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
   ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
K tuples:none
Defined Rule Symbols:   isEmpty_1, isZero_1, head_1, tail_1, append_2, p_1, inc_1, addLists_3, if_9, addList_2

Defined Pair Symbols:   ISEMPTY_1, ISZERO_1, HEAD_1, TAIL_1, APPEND_2, P_1, INC_1, ADDLISTS_3, IF_9, ADDLIST_2

Compound Symbols:   c, c1, c2, c3, c4, c5, c6, c7, c8_1, c9_1, c10, c11, c12_1, c13, c14_2, c15_2, c16_3, c17_2, c18_2, c19_3, c20_2, c21_3, c22_2, c23_3, c24, c25, c26, c27_1, c28_1, c29_1


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

(3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   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
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   P(s(s(z0))) -> c9(P(s(z0)))
   P(s(0)) -> c10
   P(0) -> c11
   INC(s(z0)) -> c12(INC(z0))
   INC(0) -> c13
   ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
   ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
   ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
   ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
   IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
   IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
   IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
   IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
   IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
   ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))

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
   append(nil, z0) -> cons(z0, nil)
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   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)
   addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
   if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
   if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
   if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
   if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
   if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
   addList(z0, z1) -> addLists(z0, z1, nil)

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:

   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
   APPEND(nil, z0) -> c7
   APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
   P(s(s(z0))) -> c9(P(s(z0)))
   P(s(0')) -> c10
   P(0') -> c11
   INC(s(z0)) -> c12(INC(z0))
   INC(0') -> c13
   ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
   ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
   ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
   ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
   ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
   ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
   ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
   IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
   IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
   IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
   IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
   IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
   ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))

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
   append(nil, z0) -> cons(z0, nil)
   append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
   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')
   addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
   if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
   if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
   if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
   if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
   if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
   addList(z0, z1) -> addLists(z0, z1, nil)

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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13

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

(9) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
APPEND, P, INC, ADDLISTS, p, inc, append, addLists

They will be analysed ascendingly in the following order:
APPEND < ADDLISTS
P < ADDLISTS
INC < ADDLISTS
p < ADDLISTS
inc < ADDLISTS
append < ADDLISTS
p < addLists
inc < addLists
append < addLists

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

(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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
APPEND, P, INC, ADDLISTS, p, inc, append, addLists

They will be analysed ascendingly in the following order:
APPEND < ADDLISTS
P < ADDLISTS
INC < ADDLISTS
p < ADDLISTS
inc < ADDLISTS
append < ADDLISTS
p < addLists
inc < addLists
append < addLists

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

(11) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b)) -> gen_c7:c816_30(n20_30), rt in Omega(1 + n20_30)

Induction Base:
APPEND(gen_cons:nil:differentLengthError14_30(0), gen_0':s15_30(b)) ->_R^Omega(1)
c7

Induction Step:
APPEND(gen_cons:nil:differentLengthError14_30(+(n20_30, 1)), gen_0':s15_30(b)) ->_R^Omega(1)
c8(APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b))) ->_IH
c8(gen_c7:c816_30(c21_30))

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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
APPEND, P, INC, ADDLISTS, p, inc, append, addLists

They will be analysed ascendingly in the following order:
APPEND < ADDLISTS
P < ADDLISTS
INC < ADDLISTS
p < ADDLISTS
inc < ADDLISTS
append < ADDLISTS
p < addLists
inc < addLists
append < addLists

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

(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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Lemmas:
APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b)) -> gen_c7:c816_30(n20_30), rt in Omega(1 + n20_30)


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
P, INC, ADDLISTS, p, inc, append, addLists

They will be analysed ascendingly in the following order:
P < ADDLISTS
INC < ADDLISTS
p < ADDLISTS
inc < ADDLISTS
append < ADDLISTS
p < addLists
inc < addLists
append < addLists

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
P(gen_0':s15_30(+(1, n1073_30))) -> gen_c9:c10:c1117_30(n1073_30), rt in Omega(1 + n1073_30)

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

Induction Step:
P(gen_0':s15_30(+(1, +(n1073_30, 1)))) ->_R^Omega(1)
c9(P(s(gen_0':s15_30(n1073_30)))) ->_IH
c9(gen_c9:c10:c1117_30(c1074_30))

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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Lemmas:
APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b)) -> gen_c7:c816_30(n20_30), rt in Omega(1 + n20_30)
P(gen_0':s15_30(+(1, n1073_30))) -> gen_c9:c10:c1117_30(n1073_30), rt in Omega(1 + n1073_30)


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
INC, ADDLISTS, p, inc, append, addLists

They will be analysed ascendingly in the following order:
INC < ADDLISTS
p < ADDLISTS
inc < ADDLISTS
append < ADDLISTS
p < addLists
inc < addLists
append < addLists

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
INC(gen_0':s15_30(n1577_30)) -> gen_c12:c1318_30(n1577_30), rt in Omega(1 + n1577_30)

Induction Base:
INC(gen_0':s15_30(0)) ->_R^Omega(1)
c13

Induction Step:
INC(gen_0':s15_30(+(n1577_30, 1))) ->_R^Omega(1)
c12(INC(gen_0':s15_30(n1577_30))) ->_IH
c12(gen_c12:c1318_30(c1578_30))

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

(20)
Obligation:
Innermost TRS:
Rules:
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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Lemmas:
APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b)) -> gen_c7:c816_30(n20_30), rt in Omega(1 + n20_30)
P(gen_0':s15_30(+(1, n1073_30))) -> gen_c9:c10:c1117_30(n1073_30), rt in Omega(1 + n1073_30)
INC(gen_0':s15_30(n1577_30)) -> gen_c12:c1318_30(n1577_30), rt in Omega(1 + n1577_30)


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
p, ADDLISTS, inc, append, addLists

They will be analysed ascendingly in the following order:
p < ADDLISTS
inc < ADDLISTS
append < ADDLISTS
p < addLists
inc < addLists
append < addLists

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

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

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

Induction Step:
p(gen_0':s15_30(+(1, +(n2114_30, 1)))) ->_R^Omega(0)
s(p(s(gen_0':s15_30(n2114_30)))) ->_IH
s(gen_0':s15_30(c2115_30))

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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Lemmas:
APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b)) -> gen_c7:c816_30(n20_30), rt in Omega(1 + n20_30)
P(gen_0':s15_30(+(1, n1073_30))) -> gen_c9:c10:c1117_30(n1073_30), rt in Omega(1 + n1073_30)
INC(gen_0':s15_30(n1577_30)) -> gen_c12:c1318_30(n1577_30), rt in Omega(1 + n1577_30)
p(gen_0':s15_30(+(1, n2114_30))) -> gen_0':s15_30(n2114_30), rt in Omega(0)


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
inc, ADDLISTS, append, addLists

They will be analysed ascendingly in the following order:
inc < ADDLISTS
append < ADDLISTS
inc < addLists
append < addLists

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

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

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

Induction Step:
inc(gen_0':s15_30(+(n2561_30, 1))) ->_R^Omega(0)
s(inc(gen_0':s15_30(n2561_30))) ->_IH
s(gen_0':s15_30(+(1, c2562_30)))

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:
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
APPEND(nil, z0) -> c7
APPEND(cons(z0, z1), z2) -> c8(APPEND(z1, z2))
P(s(s(z0))) -> c9(P(s(z0)))
P(s(0')) -> c10
P(0') -> c11
INC(s(z0)) -> c12(INC(z0))
INC(0') -> c13
ADDLISTS(z0, z1, z2) -> c14(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z0))
ADDLISTS(z0, z1, z2) -> c15(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISEMPTY(z1))
ADDLISTS(z0, z1, z2) -> c16(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), ISZERO(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c17(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c18(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c19(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), P(head(z0)), HEAD(z0))
ADDLISTS(z0, z1, z2) -> c20(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z0))
ADDLISTS(z0, z1, z2) -> c21(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), INC(head(z1)), HEAD(z1))
ADDLISTS(z0, z1, z2) -> c22(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), TAIL(z1))
ADDLISTS(z0, z1, z2) -> c23(IF(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1))), APPEND(z2, head(z1)), HEAD(z1))
IF(true, true, z0, z1, z2, z3, z4, z5, z6) -> c24
IF(true, false, z0, z1, z2, z3, z4, z5, z6) -> c25
IF(false, true, z0, z1, z2, z3, z4, z5, z6) -> c26
IF(false, false, false, z0, z1, z2, z3, z4, z5) -> c27(ADDLISTS(z2, z3, z4))
IF(false, false, true, z0, z1, z2, z3, z4, z5) -> c28(ADDLISTS(z0, z1, z5))
ADDLIST(z0, z1) -> c29(ADDLISTS(z0, z1, nil))
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
append(nil, z0) -> cons(z0, nil)
append(cons(z0, z1), z2) -> cons(z0, append(z1, z2))
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')
addLists(z0, z1, z2) -> if(isEmpty(z0), isEmpty(z1), isZero(head(z0)), tail(z0), tail(z1), cons(p(head(z0)), tail(z0)), cons(inc(head(z1)), tail(z1)), z2, append(z2, head(z1)))
if(true, true, z0, z1, z2, z3, z4, z5, z6) -> z5
if(true, false, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, true, z0, z1, z2, z3, z4, z5, z6) -> differentLengthError
if(false, false, false, z0, z1, z2, z3, z4, z5) -> addLists(z2, z3, z4)
if(false, false, true, z0, z1, z2, z3, z4, z5) -> addLists(z0, z1, z5)
addList(z0, z1) -> addLists(z0, z1, nil)

Types:
ISEMPTY :: cons:nil:differentLengthError -> c:c1
cons :: 0':s -> cons:nil:differentLengthError -> cons:nil:differentLengthError
c :: c:c1
nil :: cons:nil:differentLengthError
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:differentLengthError -> c4
c4 :: c4
TAIL :: cons:nil:differentLengthError -> c5:c6
c5 :: c5:c6
c6 :: c5:c6
APPEND :: cons:nil:differentLengthError -> 0':s -> c7:c8
c7 :: c7:c8
c8 :: c7:c8 -> c7:c8
P :: 0':s -> c9:c10:c11
c9 :: c9:c10:c11 -> c9:c10:c11
c10 :: c9:c10:c11
c11 :: c9:c10:c11
INC :: 0':s -> c12:c13
c12 :: c12:c13 -> c12:c13
c13 :: c12:c13
ADDLISTS :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c14 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
IF :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> c24:c25:c26:c27:c28
isEmpty :: cons:nil:differentLengthError -> true:false
isZero :: 0':s -> true:false
head :: cons:nil:differentLengthError -> 0':s
tail :: cons:nil:differentLengthError -> cons:nil:differentLengthError
p :: 0':s -> 0':s
inc :: 0':s -> 0':s
append :: cons:nil:differentLengthError -> 0':s -> cons:nil:differentLengthError
c15 :: c24:c25:c26:c27:c28 -> c:c1 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c16 :: c24:c25:c26:c27:c28 -> c2:c3 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c17 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c18 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c19 :: c24:c25:c26:c27:c28 -> c9:c10:c11 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c20 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c21 :: c24:c25:c26:c27:c28 -> c12:c13 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c22 :: c24:c25:c26:c27:c28 -> c5:c6 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
c23 :: c24:c25:c26:c27:c28 -> c7:c8 -> c4 -> c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
true :: true:false
c24 :: c24:c25:c26:c27:c28
false :: true:false
c25 :: c24:c25:c26:c27:c28
c26 :: c24:c25:c26:c27:c28
c27 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
c28 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c24:c25:c26:c27:c28
ADDLIST :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> c29
c29 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23 -> c29
addLists :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
if :: true:false -> true:false -> true:false -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
differentLengthError :: cons:nil:differentLengthError
addList :: cons:nil:differentLengthError -> cons:nil:differentLengthError -> cons:nil:differentLengthError
hole_c:c11_30 :: c:c1
hole_cons:nil:differentLengthError2_30 :: cons:nil:differentLengthError
hole_0':s3_30 :: 0':s
hole_c2:c34_30 :: c2:c3
hole_c45_30 :: c4
hole_c5:c66_30 :: c5:c6
hole_c7:c87_30 :: c7:c8
hole_c9:c10:c118_30 :: c9:c10:c11
hole_c12:c139_30 :: c12:c13
hole_c14:c15:c16:c17:c18:c19:c20:c21:c22:c2310_30 :: c14:c15:c16:c17:c18:c19:c20:c21:c22:c23
hole_c24:c25:c26:c27:c2811_30 :: c24:c25:c26:c27:c28
hole_true:false12_30 :: true:false
hole_c2913_30 :: c29
gen_cons:nil:differentLengthError14_30 :: Nat -> cons:nil:differentLengthError
gen_0':s15_30 :: Nat -> 0':s
gen_c7:c816_30 :: Nat -> c7:c8
gen_c9:c10:c1117_30 :: Nat -> c9:c10:c11
gen_c12:c1318_30 :: Nat -> c12:c13


Lemmas:
APPEND(gen_cons:nil:differentLengthError14_30(n20_30), gen_0':s15_30(b)) -> gen_c7:c816_30(n20_30), rt in Omega(1 + n20_30)
P(gen_0':s15_30(+(1, n1073_30))) -> gen_c9:c10:c1117_30(n1073_30), rt in Omega(1 + n1073_30)
INC(gen_0':s15_30(n1577_30)) -> gen_c12:c1318_30(n1577_30), rt in Omega(1 + n1577_30)
p(gen_0':s15_30(+(1, n2114_30))) -> gen_0':s15_30(n2114_30), rt in Omega(0)
inc(gen_0':s15_30(n2561_30)) -> gen_0':s15_30(+(1, n2561_30)), rt in Omega(0)


Generator Equations:
gen_cons:nil:differentLengthError14_30(0) <=> nil
gen_cons:nil:differentLengthError14_30(+(x, 1)) <=> cons(0', gen_cons:nil:differentLengthError14_30(x))
gen_0':s15_30(0) <=> 0'
gen_0':s15_30(+(x, 1)) <=> s(gen_0':s15_30(x))
gen_c7:c816_30(0) <=> c7
gen_c7:c816_30(+(x, 1)) <=> c8(gen_c7:c816_30(x))
gen_c9:c10:c1117_30(0) <=> c10
gen_c9:c10:c1117_30(+(x, 1)) <=> c9(gen_c9:c10:c1117_30(x))
gen_c12:c1318_30(0) <=> c13
gen_c12:c1318_30(+(x, 1)) <=> c12(gen_c12:c1318_30(x))


The following defined symbols remain to be analysed:
append, ADDLISTS, addLists

They will be analysed ascendingly in the following order:
append < ADDLISTS
append < addLists