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

0 CpxTRS
↳1 RenamingProof (⇔, 0 ms)
↳2 CpxRelTRS
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 typed CpxTrs
↳5 OrderProof (LOWER BOUND(ID), 0 ms)
↳6 typed CpxTrs
↳7 RewriteLemmaProof (LOWER BOUND(ID), 496 ms)
↳8 BEST
    ↳9 typed CpxTrs
        ↳10 NoRewriteLemmaProof (LOWER BOUND(ID), 3 ms)
        ↳11 typed CpxTrs
        ↳12 RewriteLemmaProof (LOWER BOUND(ID), 0 ms)
        ↳13 BEST
            ↳14 typed CpxTrs
                ↳15 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                ↳16 typed CpxTrs
                ↳17 RewriteLemmaProof (LOWER BOUND(ID), 27 ms)
                ↳18 BEST
                    ↳19 typed CpxTrs
                        ↳20 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                        ↳21 typed CpxTrs
                        ↳22 RewriteLemmaProof (LOWER BOUND(ID), 45 ms)
                        ↳23 BEST
                            ↳24 typed CpxTrs
                                ↳25 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                                ↳26 typed CpxTrs
                                ↳27 LowerBoundsProof (⇔, 0 ms)
                                ↳28 BOUNDS(n^1, INF)
                            ↳29 typed CpxTrs
                                ↳30 LowerBoundsProof (⇔, 0 ms)
                                ↳31 BOUNDS(n^1, INF)
                    ↳32 typed CpxTrs
                        ↳33 LowerBoundsProof (⇔, 0 ms)
                        ↳34 BOUNDS(n^1, INF)
            ↳35 typed CpxTrs
                ↳36 LowerBoundsProof (⇔, 0 ms)
                ↳37 BOUNDS(n^1, INF)
    ↳38 typed CpxTrs
        ↳39 LowerBoundsProof (⇔, 0 ms)
        ↳40 BOUNDS(n^1, INF)

(0) Obligation:

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

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative 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

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

(5) OrderProof (LOWER BOUND(ID) transformation)

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

(6) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(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

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

Induction Base:
append#1(gen_:::nil2_0(0), gen_:::nil2_0(b)) →RΩ(1)
gen_:::nil2_0(b)

Induction Step:
append#1(gen_:::nil2_0(+(n4_0, 1)), gen_:::nil2_0(b)) →RΩ(1)
::(nil, append(gen_:::nil2_0(n4_0), gen_:::nil2_0(b))) →RΩ(1)
::(nil, append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b))) →IH
::(nil, gen_:::nil2_0(+(b, c5_0)))

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

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(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

(10) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(11) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(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

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)

Induction Base:
appendAll#1(gen_:::nil2_0(0)) →RΩ(1)
nil

Induction Step:
appendAll#1(gen_:::nil2_0(+(n657_0, 1))) →RΩ(1)
append(nil, appendAll(gen_:::nil2_0(n657_0))) →RΩ(1)
append(nil, appendAll#1(gen_:::nil2_0(n657_0))) →IH
append(nil, gen_:::nil2_0(0)) →RΩ(1)
append#1(nil, gen_:::nil2_0(0)) →LΩ(1)
gen_:::nil2_0(+(0, 0))

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

(13) Complex Obligation (BEST)

(14) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(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

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(16) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(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

(17) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)

Induction Base:
appendAll2#1(gen_:::nil2_0(0)) →RΩ(1)
nil

Induction Step:
appendAll2#1(gen_:::nil2_0(+(n1046_0, 1))) →RΩ(1)
append(appendAll(nil), appendAll2(gen_:::nil2_0(n1046_0))) →RΩ(1)
append(appendAll#1(nil), appendAll2(gen_:::nil2_0(n1046_0))) →LΩ(1)
append(gen_:::nil2_0(0), appendAll2(gen_:::nil2_0(n1046_0))) →RΩ(1)
append(gen_:::nil2_0(0), appendAll2#1(gen_:::nil2_0(n1046_0))) →IH
append(gen_:::nil2_0(0), gen_:::nil2_0(0)) →RΩ(1)
append#1(gen_:::nil2_0(0), gen_:::nil2_0(0)) →LΩ(1)
gen_:::nil2_0(+(0, 0))

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

(18) Complex Obligation (BEST)

(19) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(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

(20) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(21) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

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

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

(22) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
appendAll3#1(gen_:::nil2_0(n1796_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n17960)

Induction Base:
appendAll3#1(gen_:::nil2_0(0)) →RΩ(1)
nil

Induction Step:
appendAll3#1(gen_:::nil2_0(+(n1796_0, 1))) →RΩ(1)
append(appendAll2(nil), appendAll3(gen_:::nil2_0(n1796_0))) →RΩ(1)
append(appendAll2#1(nil), appendAll3(gen_:::nil2_0(n1796_0))) →LΩ(1)
append(gen_:::nil2_0(0), appendAll3(gen_:::nil2_0(n1796_0))) →RΩ(1)
append(gen_:::nil2_0(0), appendAll3#1(gen_:::nil2_0(n1796_0))) →IH
append(gen_:::nil2_0(0), gen_:::nil2_0(0)) →RΩ(1)
append#1(gen_:::nil2_0(0), gen_:::nil2_0(0)) →LΩ(1)
gen_:::nil2_0(+(0, 0))

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

(23) Complex Obligation (BEST)

(24) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)
appendAll3#1(gen_:::nil2_0(n1796_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n17960)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
appendAll3

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

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(26) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)
appendAll3#1(gen_:::nil2_0(n1796_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n17960)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

(28) BOUNDS(n^1, INF)

(29) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)
appendAll3#1(gen_:::nil2_0(n1796_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n17960)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

(31) BOUNDS(n^1, INF)

(32) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)
appendAll2#1(gen_:::nil2_0(n1046_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n10460)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

(34) BOUNDS(n^1, INF)

(35) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)
appendAll#1(gen_:::nil2_0(n657_0)) → gen_:::nil2_0(0), rt ∈ Ω(1 + n6570)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

(37) BOUNDS(n^1, INF)

(38) Obligation:

Innermost TRS:
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_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(nil, gen_:::nil2_0(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) was proven with the following lemma:
append#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(b)) → gen_:::nil2_0(+(n4_0, b)), rt ∈ Ω(1 + n40)

(40) BOUNDS(n^1, INF)