Runtime Complexity TRS:
The TRS R consists of the following rules:

append(@l1, @l2) → append#1(@l1, @l2)
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2))
append#1(nil, @l2) → @l2
appendAll(@l) → appendAll#1(@l)
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls))
appendAll#1(nil) → nil
appendAll2(@l) → appendAll2#1(@l)
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls))
appendAll2#1(nil) → nil
appendAll3(@l) → appendAll3#1(@l)
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls))
appendAll3#1(nil) → nil

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Heuristically decided to analyse the following defined symbols:
append', append#1', appendAll', appendAll#1', appendAll2', appendAll2#1', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
append' = append#1'
append' < appendAll#1'
append' < appendAll2#1'
append' < appendAll3#1'
appendAll' = appendAll#1'
appendAll' < appendAll2#1'
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
append#1', append', appendAll', appendAll#1', appendAll2', appendAll2#1', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
append' = append#1'
append' < appendAll#1'
append' < appendAll2#1'
append' < appendAll3#1'
appendAll' = appendAll#1'
appendAll' < appendAll2#1'
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

Proved the following rewrite lemma:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Induction Base:
append#1'(_gen_::':nil'2(0), _gen_::':nil'2(b)) →RΩ(1)
_gen_::':nil'2(b)

Induction Step:
append#1'(_gen_::':nil'2(+(_$n5, 1)), _gen_::':nil'2(_b145)) →RΩ(1)
::'(nil', append'(_gen_::':nil'2(_$n5), _gen_::':nil'2(_b145))) →RΩ(1)
::'(nil', append#1'(_gen_::':nil'2(_$n5), _gen_::':nil'2(_b145))) →IH
::'(nil', _gen_::':nil'2(+(_$n5, _b145)))

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
append', appendAll', appendAll#1', appendAll2', appendAll2#1', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
append' = append#1'
append' < appendAll#1'
append' < appendAll2#1'
append' < appendAll3#1'
appendAll' = appendAll#1'
appendAll' < appendAll2#1'
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
appendAll#1', appendAll', appendAll2', appendAll2#1', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
appendAll' = appendAll#1'
appendAll' < appendAll2#1'
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

Proved the following rewrite lemma:
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)

Induction Base:
appendAll#1'(_gen_::':nil'2(0)) →RΩ(1)
nil'

Induction Step:
appendAll#1'(_gen_::':nil'2(+(_$n948, 1))) →RΩ(1)
append'(nil', appendAll'(_gen_::':nil'2(_$n948))) →RΩ(1)
append'(nil', appendAll#1'(_gen_::':nil'2(_$n948))) →IH
append'(nil', _gen_::':nil'2(0)) →RΩ(1)
append#1'(nil', _gen_::':nil'2(0)) →LΩ(1)
_gen_::':nil'2(+(0, 0))

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
appendAll', appendAll2', appendAll2#1', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
appendAll' = appendAll#1'
appendAll' < appendAll2#1'
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
appendAll2#1', appendAll2', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

Proved the following rewrite lemma:
appendAll2#1'(_gen_::':nil'2(_n1908)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n1908)

Induction Base:
appendAll2#1'(_gen_::':nil'2(0)) →RΩ(1)
nil'

Induction Step:
appendAll2#1'(_gen_::':nil'2(+(_$n1909, 1))) →RΩ(1)
append'(appendAll'(nil'), appendAll2'(_gen_::':nil'2(_$n1909))) →RΩ(1)
append'(appendAll#1'(nil'), appendAll2'(_gen_::':nil'2(_$n1909))) →LΩ(1)
append'(_gen_::':nil'2(0), appendAll2'(_gen_::':nil'2(_$n1909))) →RΩ(1)
append'(_gen_::':nil'2(0), appendAll2#1'(_gen_::':nil'2(_$n1909))) →IH
append'(_gen_::':nil'2(0), _gen_::':nil'2(0)) →RΩ(1)
append#1'(_gen_::':nil'2(0), _gen_::':nil'2(0)) →LΩ(1)
_gen_::':nil'2(+(0, 0))

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)
appendAll2#1'(_gen_::':nil'2(_n1908)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n1908)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
appendAll2', appendAll3', appendAll3#1'

They will be analysed ascendingly in the following order:
appendAll2' = appendAll2#1'
appendAll2' < appendAll3#1'
appendAll3' = appendAll3#1'

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)
appendAll2#1'(_gen_::':nil'2(_n1908)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n1908)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
appendAll3#1', appendAll3'

They will be analysed ascendingly in the following order:
appendAll3' = appendAll3#1'

Proved the following rewrite lemma:
appendAll3#1'(_gen_::':nil'2(_n3884)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n3884)

Induction Base:
appendAll3#1'(_gen_::':nil'2(0)) →RΩ(1)
nil'

Induction Step:
appendAll3#1'(_gen_::':nil'2(+(_$n3885, 1))) →RΩ(1)
append'(appendAll2'(nil'), appendAll3'(_gen_::':nil'2(_$n3885))) →RΩ(1)
append'(appendAll2#1'(nil'), appendAll3'(_gen_::':nil'2(_$n3885))) →LΩ(1)
append'(_gen_::':nil'2(0), appendAll3'(_gen_::':nil'2(_$n3885))) →RΩ(1)
append'(_gen_::':nil'2(0), appendAll3#1'(_gen_::':nil'2(_$n3885))) →IH
append'(_gen_::':nil'2(0), _gen_::':nil'2(0)) →RΩ(1)
append#1'(_gen_::':nil'2(0), _gen_::':nil'2(0)) →LΩ(1)
_gen_::':nil'2(+(0, 0))

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)
appendAll2#1'(_gen_::':nil'2(_n1908)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n1908)
appendAll3#1'(_gen_::':nil'2(_n3884)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n3884)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

The following defined symbols remain to be analysed:
appendAll3'

They will be analysed ascendingly in the following order:
appendAll3' = appendAll3#1'

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

Rules:
append'(@l1, @l2) → append#1'(@l1, @l2)
append#1'(::'(@x, @xs), @l2) → ::'(@x, append'(@xs, @l2))
append#1'(nil', @l2) → @l2
appendAll'(@l) → appendAll#1'(@l)
appendAll#1'(::'(@l1, @ls)) → append'(@l1, appendAll'(@ls))
appendAll#1'(nil') → nil'
appendAll2'(@l) → appendAll2#1'(@l)
appendAll2#1'(::'(@l1, @ls)) → append'(appendAll'(@l1), appendAll2'(@ls))
appendAll2#1'(nil') → nil'
appendAll3'(@l) → appendAll3#1'(@l)
appendAll3#1'(::'(@l1, @ls)) → append'(appendAll2'(@l1), appendAll3'(@ls))
appendAll3#1'(nil') → nil'

Types:
append' :: ::':nil' → ::':nil' → ::':nil'
append#1' :: ::':nil' → ::':nil' → ::':nil'
::' :: ::':nil' → ::':nil' → ::':nil'
nil' :: ::':nil'
appendAll' :: ::':nil' → ::':nil'
appendAll#1' :: ::':nil' → ::':nil'
appendAll2' :: ::':nil' → ::':nil'
appendAll2#1' :: ::':nil' → ::':nil'
appendAll3' :: ::':nil' → ::':nil'
appendAll3#1' :: ::':nil' → ::':nil'
_hole_::':nil'1 :: ::':nil'
_gen_::':nil'2 :: Nat → ::':nil'

Lemmas:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
appendAll#1'(_gen_::':nil'2(_n947)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n947)
appendAll2#1'(_gen_::':nil'2(_n1908)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n1908)
appendAll3#1'(_gen_::':nil'2(_n3884)) → _gen_::':nil'2(0), rt ∈ Ω(1 + n3884)

Generator Equations:
_gen_::':nil'2(0) ⇔ nil'
_gen_::':nil'2(+(x, 1)) ⇔ ::'(nil', _gen_::':nil'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
append#1'(_gen_::':nil'2(_n4), _gen_::':nil'2(b)) → _gen_::':nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)