Runtime Complexity TRS:
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)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
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')

Rewrite Strategy: INNERMOST

Infered types.

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')

Types:
isEmpty' :: cons':nil':differentLengthError' → false':true'
cons' :: 0':s' → cons':nil':differentLengthError' → cons':nil':differentLengthError'
false' :: false':true'
nil' :: cons':nil':differentLengthError'
true' :: false':true'
isZero' :: 0':s' → false':true'
0' :: 0':s'
s' :: 0':s' → 0':s'
head' :: cons':nil':differentLengthError' → 0':s'
tail' :: cons':nil':differentLengthError' → cons':nil':differentLengthError'
append' :: cons':nil':differentLengthError' → 0':s' → cons':nil':differentLengthError'
p' :: 0':s' → 0':s'
inc' :: 0':s' → 0':s'
addLists' :: cons':nil':differentLengthError' → cons':nil':differentLengthError' → cons':nil':differentLengthError' → cons':nil':differentLengthError'
if' :: false':true' → false':true' → false':true' → 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_false':true'1 :: false':true'
_hole_cons':nil':differentLengthError'2 :: cons':nil':differentLengthError'
_hole_0':s'3 :: 0':s'
_gen_cons':nil':differentLengthError'4 :: Nat → cons':nil':differentLengthError'
_gen_0':s'5 :: Nat → 0':s'

Heuristically decided to analyse the following defined symbols:
append', p', inc', addLists'

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

Generator Equations:
_gen_cons':nil':differentLengthError'4(0) ⇔ nil'
_gen_cons':nil':differentLengthError'4(+(x, 1)) ⇔ cons'(0', _gen_cons':nil':differentLengthError'4(x))
_gen_0':s'5(0) ⇔ 0'
_gen_0':s'5(+(x, 1)) ⇔ s'(_gen_0':s'5(x))

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

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

Proved the following rewrite lemma:
append'(_gen_cons':nil':differentLengthError'4(+(1, _n7)), _gen_0':s'5(b)) → _*6, rt ∈ Ω(_n7)

Induction Base:
append'(_gen_cons':nil':differentLengthError'4(+(1, 0)), _gen_0':s'5(b))

Induction Step:
append'(_gen_cons':nil':differentLengthError'4(+(1, +(_$n8, 1))), _gen_0':s'5(_b388678)) →_R^Ω(1)
cons'(0', append'(_gen_cons':nil':differentLengthError'4(+(1, _$n8)), _gen_0':s'5(_b388678))) →_IH
cons'(0', _*6)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
append'(_gen_cons':nil':differentLengthError'4(+(1, _n7)), _gen_0':s'5(b)) → _*6, rt ∈ Ω(_n7)

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

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

Proved the following rewrite lemma:
p'(_gen_0':s'5(+(1, _n390143))) → _gen_0':s'5(_n390143), rt ∈ Ω(1 + _n390143)

Induction Base:
p'(_gen_0':s'5(+(1, 0))) →_R^Ω(1)
0'

Induction Step:
p'(_gen_0':s'5(+(1, +(_$n390144, 1)))) →_R^Ω(1)
s'(p'(s'(_gen_0':s'5(_$n390144)))) →_IH
s'(_gen_0':s'5(_$n390144))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
append'(_gen_cons':nil':differentLengthError'4(+(1, _n7)), _gen_0':s'5(b)) → _*6, rt ∈ Ω(_n7)
p'(_gen_0':s'5(+(1, _n390143))) → _gen_0':s'5(_n390143), rt ∈ Ω(1 + _n390143)

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

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

Proved the following rewrite lemma:
inc'(_gen_0':s'5(_n391472)) → _gen_0':s'5(+(1, _n391472)), rt ∈ Ω(1 + _n391472)

Induction Base:
inc'(_gen_0':s'5(0)) →_R^Ω(1)
s'(0')

Induction Step:
inc'(_gen_0':s'5(+(_$n391473, 1))) →_R^Ω(1)
s'(inc'(_gen_0':s'5(_$n391473))) →_IH
s'(_gen_0':s'5(+(1, _$n391473)))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
append'(_gen_cons':nil':differentLengthError'4(+(1, _n7)), _gen_0':s'5(b)) → _*6, rt ∈ Ω(_n7)
p'(_gen_0':s'5(+(1, _n390143))) → _gen_0':s'5(_n390143), rt ∈ Ω(1 + _n390143)
inc'(_gen_0':s'5(_n391472)) → _gen_0':s'5(+(1, _n391472)), rt ∈ Ω(1 + _n391472)

The following defined symbols remain to be analysed:
addLists'

Could not prove a rewrite lemma for the defined symbol addLists'.

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
append'(_gen_cons':nil':differentLengthError'4(+(1, _n7)), _gen_0':s'5(b)) → _*6, rt ∈ Ω(_n7)