WORST_CASE(Omega(n^1),O(n^1))
proof of input_k6LTTJzeOo.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, n^1).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxWeightedTrs
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CpxTypedWeightedTrs
    (13) CompletionProof [UPPER BOUND(ID), 0 ms]
    (14) CpxTypedWeightedCompleteTrs
    (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (16) CpxRNTS
    (17) CompleteCoflocoProof [FINISHED, 912 ms]
    (18) BOUNDS(1, n^1)
(19) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CdtProblem
    (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CpxRelTRS
    (23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) typed CpxTrs
    (27) OrderProof [LOWER BOUND(ID), 4 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 259 ms]
    (30) typed CpxTrs
    (31) RewriteLemmaProof [LOWER BOUND(ID), 61 ms]
    (32) typed CpxTrs
    (33) RewriteLemmaProof [LOWER BOUND(ID), 72 ms]
    (34) typed CpxTrs
    (35) RewriteLemmaProof [LOWER BOUND(ID), 65 ms]
    (36) typed CpxTrs
    (37) RewriteLemmaProof [LOWER BOUND(ID), 522 ms]
    (38) BEST
        (39) proven lower bound
            (40) LowerBoundPropagationProof [FINISHED, 0 ms]
            (41) BOUNDS(n^1, INF)
        (42) typed CpxTrs
            (43) RewriteLemmaProof [LOWER BOUND(ID), 506 ms]
            (44) typed CpxTrs
            (45) RewriteLemmaProof [LOWER BOUND(ID), 371 ms]
            (46) typed CpxTrs
            (47) RewriteLemmaProof [LOWER BOUND(ID), 217 ms]
            (48) typed CpxTrs
            (49) RewriteLemmaProof [LOWER BOUND(ID), 150 ms]
            (50) typed CpxTrs
            (51) RewriteLemmaProof [LOWER BOUND(ID), 270 ms]
            (52) typed CpxTrs
            (53) RewriteLemmaProof [LOWER BOUND(ID), 1067 ms]
            (54) typed CpxTrs
            (55) RewriteLemmaProof [LOWER BOUND(ID), 75 ms]
            (56) typed CpxTrs


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

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


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: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL#1(nil) -> c5
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL2#1(nil) -> c9
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL3#1(nil) -> c13
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL#1(nil) -> c5
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL2#1(nil) -> c9
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL3#1(nil) -> c13
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1

Defined Pair Symbols:   APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1

Compound Symbols:   c_1, c1_1, c2, c3_1, c4_2, c5, c6_1, c7_2, c8_2, c9, c10_1, c11_2, c12_2, c13


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 4 trailing nodes:
   APPENDALL3#1(nil) -> c13
   APPENDALL2#1(nil) -> c9
   APPEND#1(nil, z0) -> c2
   APPENDALL#1(nil) -> c5

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1

Defined Pair Symbols:   APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1

Compound Symbols:   c_1, c1_1, c3_1, c4_2, c6_1, c7_2, c8_2, c10_1, c11_2, c12_2


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

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL2#1(::(z0, z1)) -> c2(APPEND(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1(::(z0, z1)) -> c2(APPENDALL(z0))
   APPENDALL3#1(::(z0, z1)) -> c2(APPEND(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1(::(z0, z1)) -> c2(APPENDALL2(z0))
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL2#1(::(z0, z1)) -> c2(APPEND(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1(::(z0, z1)) -> c2(APPENDALL(z0))
   APPENDALL3#1(::(z0, z1)) -> c2(APPEND(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1(::(z0, z1)) -> c2(APPENDALL2(z0))
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1

Defined Pair Symbols:   APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1

Compound Symbols:   c_1, c1_1, c3_1, c4_2, c6_1, c8_2, c10_1, c12_2, c2_1


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

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

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


The TRS R consists of the following rules:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL2#1(::(z0, z1)) -> c2(APPEND(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1(::(z0, z1)) -> c2(APPENDALL(z0))
   APPENDALL3#1(::(z0, z1)) -> c2(APPEND(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1(::(z0, z1)) -> c2(APPENDALL2(z0))

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

   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil

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

(9) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1)) [1]
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) [1]
   APPENDALL(z0) -> c3(APPENDALL#1(z0)) [1]
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) [1]
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) [1]
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1)) [1]
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0)) [1]
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1)) [1]
   APPENDALL2#1(::(z0, z1)) -> c2(APPEND(appendAll(z0), appendAll2(z1))) [1]
   APPENDALL2#1(::(z0, z1)) -> c2(APPENDALL(z0)) [1]
   APPENDALL3#1(::(z0, z1)) -> c2(APPEND(appendAll2(z0), appendAll3(z1))) [1]
   APPENDALL3#1(::(z0, z1)) -> c2(APPENDALL2(z0)) [1]
   append(z0, z1) -> append#1(z0, z1) [0]
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) [0]
   append#1(nil, z0) -> z0 [0]
   appendAll(z0) -> appendAll#1(z0) [0]
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) [0]
   appendAll#1(nil) -> nil [0]
   appendAll2(z0) -> appendAll2#1(z0) [0]
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) [0]
   appendAll2#1(nil) -> nil [0]
   appendAll3(z0) -> appendAll3#1(z0) [0]
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) [0]
   appendAll3#1(nil) -> nil [0]

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

(11) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(12)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1)) [1]
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) [1]
   APPENDALL(z0) -> c3(APPENDALL#1(z0)) [1]
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) [1]
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) [1]
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1)) [1]
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0)) [1]
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1)) [1]
   APPENDALL2#1(::(z0, z1)) -> c2(APPEND(appendAll(z0), appendAll2(z1))) [1]
   APPENDALL2#1(::(z0, z1)) -> c2(APPENDALL(z0)) [1]
   APPENDALL3#1(::(z0, z1)) -> c2(APPEND(appendAll2(z0), appendAll3(z1))) [1]
   APPENDALL3#1(::(z0, z1)) -> c2(APPENDALL2(z0)) [1]
   append(z0, z1) -> append#1(z0, z1) [0]
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) [0]
   append#1(nil, z0) -> z0 [0]
   appendAll(z0) -> appendAll#1(z0) [0]
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) [0]
   appendAll#1(nil) -> nil [0]
   appendAll2(z0) -> appendAll2#1(z0) [0]
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) [0]
   appendAll2#1(nil) -> nil [0]
   appendAll3(z0) -> appendAll3#1(z0) [0]
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) [0]
   appendAll3#1(nil) -> nil [0]

The TRS has the following type information:
APPEND :: :::nil -> :::nil -> c:c3:c6
c :: c1 -> c:c3:c6
APPEND#1 :: :::nil -> :::nil -> c1
:: :: :::nil -> :::nil -> :::nil
c1 :: c:c3:c6 -> c1
APPENDALL :: :::nil -> c:c3:c6
c3 :: c4 -> c:c3:c6
APPENDALL#1 :: :::nil -> c4
c4 :: c:c3:c6 -> c:c3:c6 -> c4
appendAll :: :::nil -> :::nil
APPENDALL2 :: :::nil -> c:c3:c6
c6 :: c8:c12:c2 -> c:c3:c6
APPENDALL2#1 :: :::nil -> c8:c12:c2
c8 :: c:c3:c6 -> c:c3:c6 -> c8:c12:c2
appendAll2 :: :::nil -> :::nil
APPENDALL3 :: :::nil -> c10
c10 :: c8:c12:c2 -> c10
APPENDALL3#1 :: :::nil -> c8:c12:c2
c12 :: c:c3:c6 -> c10 -> c8:c12:c2
appendAll3 :: :::nil -> :::nil
c2 :: c:c3:c6 -> c8:c12:c2
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
nil :: :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil

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

(13) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   append(v0, v1) -> null_append [0]
   append#1(v0, v1) -> null_append#1 [0]
   appendAll(v0) -> null_appendAll [0]
   appendAll#1(v0) -> null_appendAll#1 [0]
   appendAll2(v0) -> null_appendAll2 [0]
   appendAll2#1(v0) -> null_appendAll2#1 [0]
   appendAll3(v0) -> null_appendAll3 [0]
   appendAll3#1(v0) -> null_appendAll3#1 [0]
   APPEND#1(v0, v1) -> null_APPEND#1 [0]
   APPENDALL#1(v0) -> null_APPENDALL#1 [0]
   APPENDALL2#1(v0) -> null_APPENDALL2#1 [0]
   APPENDALL3#1(v0) -> null_APPENDALL3#1 [0]

And the following fresh constants:    null_append, null_append#1, null_appendAll, null_appendAll#1, null_appendAll2, null_appendAll2#1, null_appendAll3, null_appendAll3#1, null_APPEND#1, null_APPENDALL#1, null_APPENDALL2#1, null_APPENDALL3#1, const, const1

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

(14)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1)) [1]
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2)) [1]
   APPENDALL(z0) -> c3(APPENDALL#1(z0)) [1]
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) [1]
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0)) [1]
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1)) [1]
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0)) [1]
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1)) [1]
   APPENDALL2#1(::(z0, z1)) -> c2(APPEND(appendAll(z0), appendAll2(z1))) [1]
   APPENDALL2#1(::(z0, z1)) -> c2(APPENDALL(z0)) [1]
   APPENDALL3#1(::(z0, z1)) -> c2(APPEND(appendAll2(z0), appendAll3(z1))) [1]
   APPENDALL3#1(::(z0, z1)) -> c2(APPENDALL2(z0)) [1]
   append(z0, z1) -> append#1(z0, z1) [0]
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) [0]
   append#1(nil, z0) -> z0 [0]
   appendAll(z0) -> appendAll#1(z0) [0]
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1)) [0]
   appendAll#1(nil) -> nil [0]
   appendAll2(z0) -> appendAll2#1(z0) [0]
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1)) [0]
   appendAll2#1(nil) -> nil [0]
   appendAll3(z0) -> appendAll3#1(z0) [0]
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1)) [0]
   appendAll3#1(nil) -> nil [0]
   append(v0, v1) -> null_append [0]
   append#1(v0, v1) -> null_append#1 [0]
   appendAll(v0) -> null_appendAll [0]
   appendAll#1(v0) -> null_appendAll#1 [0]
   appendAll2(v0) -> null_appendAll2 [0]
   appendAll2#1(v0) -> null_appendAll2#1 [0]
   appendAll3(v0) -> null_appendAll3 [0]
   appendAll3#1(v0) -> null_appendAll3#1 [0]
   APPEND#1(v0, v1) -> null_APPEND#1 [0]
   APPENDALL#1(v0) -> null_APPENDALL#1 [0]
   APPENDALL2#1(v0) -> null_APPENDALL2#1 [0]
   APPENDALL3#1(v0) -> null_APPENDALL3#1 [0]

The TRS has the following type information:
APPEND :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c:c3:c6
c :: c1:null_APPEND#1 -> c:c3:c6
APPEND#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c1:null_APPEND#1
:: :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
c1 :: c:c3:c6 -> c1:null_APPEND#1
APPENDALL :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c:c3:c6
c3 :: c4:null_APPENDALL#1 -> c:c3:c6
APPENDALL#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c4:null_APPENDALL#1
c4 :: c:c3:c6 -> c:c3:c6 -> c4:null_APPENDALL#1
appendAll :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
APPENDALL2 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c:c3:c6
c6 :: c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1 -> c:c3:c6
APPENDALL2#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
c8 :: c:c3:c6 -> c:c3:c6 -> c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
appendAll2 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
APPENDALL3 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c10
c10 :: c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1 -> c10
APPENDALL3#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
c12 :: c:c3:c6 -> c10 -> c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
appendAll3 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
c2 :: c:c3:c6 -> c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
append :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
append#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
nil :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
appendAll#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
appendAll2#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
appendAll3#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1 -> :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_append :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_append#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_appendAll :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_appendAll#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_appendAll2 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_appendAll2#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_appendAll3 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_appendAll3#1 :: :::nil:null_append:null_append#1:null_appendAll:null_appendAll#1:null_appendAll2:null_appendAll2#1:null_appendAll3:null_appendAll3#1
null_APPEND#1 :: c1:null_APPEND#1
null_APPENDALL#1 :: c4:null_APPENDALL#1
null_APPENDALL2#1 :: c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
null_APPENDALL3#1 :: c8:c12:c2:null_APPENDALL2#1:null_APPENDALL3#1
const :: c:c3:c6
const1 :: c10

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

(15) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   nil => 0
   null_append => 0
   null_append#1 => 0
   null_appendAll => 0
   null_appendAll#1 => 0
   null_appendAll2 => 0
   null_appendAll2#1 => 0
   null_appendAll3 => 0
   null_appendAll3#1 => 0
   null_APPEND#1 => 0
   null_APPENDALL#1 => 0
   null_APPENDALL2#1 => 0
   null_APPENDALL3#1 => 0
   const => 0
   const1 => 0

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

(16)
Obligation:
Complexity RNTS consisting of the following rules:

   APPEND(z, z') -{ 1 }-> 1 + APPEND#1(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   APPEND#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   APPEND#1(z, z') -{ 1 }-> 1 + APPEND(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   APPENDALL(z) -{ 1 }-> 1 + APPENDALL#1(z0) :|: z = z0, z0 >= 0
   APPENDALL#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   APPENDALL#1(z) -{ 1 }-> 1 + APPEND(z0, appendAll(z1)) + APPENDALL(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   APPENDALL2(z) -{ 1 }-> 1 + APPENDALL2#1(z0) :|: z = z0, z0 >= 0
   APPENDALL2#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   APPENDALL2#1(z) -{ 1 }-> 1 + APPENDALL(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   APPENDALL2#1(z) -{ 1 }-> 1 + APPEND(appendAll(z0), appendAll2(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   APPENDALL2#1(z) -{ 1 }-> 1 + APPEND(appendAll(z0), appendAll2(z1)) + APPENDALL2(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   APPENDALL3(z) -{ 1 }-> 1 + APPENDALL3#1(z0) :|: z = z0, z0 >= 0
   APPENDALL3#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   APPENDALL3#1(z) -{ 1 }-> 1 + APPENDALL2(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   APPENDALL3#1(z) -{ 1 }-> 1 + APPEND(appendAll2(z0), appendAll3(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   APPENDALL3#1(z) -{ 1 }-> 1 + APPEND(appendAll2(z0), appendAll3(z1)) + APPENDALL3(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   append(z, z') -{ 0 }-> append#1(z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   append(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   append#1(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0
   append#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   append#1(z, z') -{ 0 }-> 1 + z0 + append(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0
   appendAll(z) -{ 0 }-> appendAll#1(z0) :|: z = z0, z0 >= 0
   appendAll(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   appendAll#1(z) -{ 0 }-> append(z0, appendAll(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   appendAll#1(z) -{ 0 }-> 0 :|: z = 0
   appendAll#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   appendAll2(z) -{ 0 }-> appendAll2#1(z0) :|: z = z0, z0 >= 0
   appendAll2(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   appendAll2#1(z) -{ 0 }-> append(appendAll(z0), appendAll2(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   appendAll2#1(z) -{ 0 }-> 0 :|: z = 0
   appendAll2#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   appendAll3(z) -{ 0 }-> appendAll3#1(z0) :|: z = z0, z0 >= 0
   appendAll3(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   appendAll3#1(z) -{ 0 }-> append(appendAll2(z0), appendAll3(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   appendAll3#1(z) -{ 0 }-> 0 :|: z = 0
   appendAll3#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

(17) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun2(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun3(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun4(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun5(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun6(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun7(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[append(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun8(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[appendAll(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun9(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[appendAll2(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun10(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[appendAll3(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun11(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun1(V3, V2, Ret1)],[Out = 1 + Ret1,V1 = V3,V2 >= 0,V = V2,V3 >= 0]).
eq(fun1(V1, V, Out),1,[fun(V4, V6, Ret11)],[Out = 1 + Ret11,V4 >= 0,V = V6,V5 >= 0,V1 = 1 + V4 + V5,V6 >= 0]).
eq(fun2(V1, Out),1,[fun3(V7, Ret12)],[Out = 1 + Ret12,V1 = V7,V7 >= 0]).
eq(fun3(V1, Out),1,[appendAll(V9, Ret011),fun(V8, Ret011, Ret01),fun2(V9, Ret13)],[Out = 1 + Ret01 + Ret13,V9 >= 0,V8 >= 0,V1 = 1 + V8 + V9]).
eq(fun4(V1, Out),1,[fun5(V10, Ret14)],[Out = 1 + Ret14,V1 = V10,V10 >= 0]).
eq(fun5(V1, Out),1,[appendAll(V11, Ret010),appendAll2(V12, Ret0111),fun(Ret010, Ret0111, Ret012),fun4(V12, Ret15)],[Out = 1 + Ret012 + Ret15,V12 >= 0,V11 >= 0,V1 = 1 + V11 + V12]).
eq(fun6(V1, Out),1,[fun7(V13, Ret16)],[Out = 1 + Ret16,V1 = V13,V13 >= 0]).
eq(fun7(V1, Out),1,[appendAll2(V15, Ret0101),appendAll3(V14, Ret0112),fun(Ret0101, Ret0112, Ret013),fun6(V14, Ret17)],[Out = 1 + Ret013 + Ret17,V14 >= 0,V15 >= 0,V1 = 1 + V14 + V15]).
eq(fun5(V1, Out),1,[appendAll(V17, Ret10),appendAll2(V16, Ret111),fun(Ret10, Ret111, Ret18)],[Out = 1 + Ret18,V16 >= 0,V17 >= 0,V1 = 1 + V16 + V17]).
eq(fun5(V1, Out),1,[fun2(V18, Ret19)],[Out = 1 + Ret19,V19 >= 0,V18 >= 0,V1 = 1 + V18 + V19]).
eq(fun7(V1, Out),1,[appendAll2(V21, Ret101),appendAll3(V20, Ret112),fun(Ret101, Ret112, Ret110)],[Out = 1 + Ret110,V20 >= 0,V21 >= 0,V1 = 1 + V20 + V21]).
eq(fun7(V1, Out),1,[fun4(V22, Ret113)],[Out = 1 + Ret113,V23 >= 0,V22 >= 0,V1 = 1 + V22 + V23]).
eq(append(V1, V, Out),0,[fun8(V24, V25, Ret)],[Out = Ret,V1 = V24,V25 >= 0,V = V25,V24 >= 0]).
eq(fun8(V1, V, Out),0,[append(V28, V26, Ret114)],[Out = 1 + Ret114 + V27,V28 >= 0,V = V26,V27 >= 0,V1 = 1 + V27 + V28,V26 >= 0]).
eq(fun8(V1, V, Out),0,[],[Out = V29,V29 >= 0,V1 = 0,V = V29]).
eq(appendAll(V1, Out),0,[fun9(V30, Ret2)],[Out = Ret2,V1 = V30,V30 >= 0]).
eq(fun9(V1, Out),0,[appendAll(V31, Ret115),append(V32, Ret115, Ret3)],[Out = Ret3,V31 >= 0,V32 >= 0,V1 = 1 + V31 + V32]).
eq(fun9(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(appendAll2(V1, Out),0,[fun10(V33, Ret4)],[Out = Ret4,V1 = V33,V33 >= 0]).
eq(fun10(V1, Out),0,[appendAll(V35, Ret0),appendAll2(V34, Ret116),append(Ret0, Ret116, Ret5)],[Out = Ret5,V34 >= 0,V35 >= 0,V1 = 1 + V34 + V35]).
eq(fun10(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(appendAll3(V1, Out),0,[fun11(V36, Ret6)],[Out = Ret6,V1 = V36,V36 >= 0]).
eq(fun11(V1, Out),0,[appendAll2(V37, Ret02),appendAll3(V38, Ret117),append(Ret02, Ret117, Ret7)],[Out = Ret7,V38 >= 0,V37 >= 0,V1 = 1 + V37 + V38]).
eq(fun11(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(append(V1, V, Out),0,[],[Out = 0,V40 >= 0,V39 >= 0,V1 = V40,V = V39]).
eq(fun8(V1, V, Out),0,[],[Out = 0,V42 >= 0,V41 >= 0,V1 = V42,V = V41]).
eq(appendAll(V1, Out),0,[],[Out = 0,V43 >= 0,V1 = V43]).
eq(fun9(V1, Out),0,[],[Out = 0,V44 >= 0,V1 = V44]).
eq(appendAll2(V1, Out),0,[],[Out = 0,V45 >= 0,V1 = V45]).
eq(fun10(V1, Out),0,[],[Out = 0,V46 >= 0,V1 = V46]).
eq(appendAll3(V1, Out),0,[],[Out = 0,V47 >= 0,V1 = V47]).
eq(fun11(V1, Out),0,[],[Out = 0,V48 >= 0,V1 = V48]).
eq(fun1(V1, V, Out),0,[],[Out = 0,V49 >= 0,V50 >= 0,V1 = V49,V = V50]).
eq(fun3(V1, Out),0,[],[Out = 0,V51 >= 0,V1 = V51]).
eq(fun5(V1, Out),0,[],[Out = 0,V52 >= 0,V1 = V52]).
eq(fun7(V1, Out),0,[],[Out = 0,V53 >= 0,V1 = V53]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun2(V1,Out),[V1],[Out]).
input_output_vars(fun3(V1,Out),[V1],[Out]).
input_output_vars(fun4(V1,Out),[V1],[Out]).
input_output_vars(fun5(V1,Out),[V1],[Out]).
input_output_vars(fun6(V1,Out),[V1],[Out]).
input_output_vars(fun7(V1,Out),[V1],[Out]).
input_output_vars(append(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun8(V1,V,Out),[V1,V],[Out]).
input_output_vars(appendAll(V1,Out),[V1],[Out]).
input_output_vars(fun9(V1,Out),[V1],[Out]).
input_output_vars(appendAll2(V1,Out),[V1],[Out]).
input_output_vars(fun10(V1,Out),[V1],[Out]).
input_output_vars(appendAll3(V1,Out),[V1],[Out]).
input_output_vars(fun11(V1,Out),[V1],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [append/3,fun8/3]
1. recursive [non_tail] : [appendAll/2,fun9/2]
2. recursive [non_tail] : [appendAll2/2,fun10/2]
3. recursive [non_tail] : [appendAll3/2,fun11/2]
4. recursive  : [fun/3,fun1/3]
5. recursive  : [fun2/2,fun3/2]
6. recursive  : [fun4/2,fun5/2]
7. recursive  : [fun6/2,fun7/2]
8. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into append/3
1. SCC is partially evaluated into appendAll/2
2. SCC is partially evaluated into appendAll2/2
3. SCC is partially evaluated into appendAll3/2
4. SCC is partially evaluated into fun/3
5. SCC is partially evaluated into fun2/2
6. SCC is partially evaluated into fun4/2
7. SCC is partially evaluated into fun7/2
8. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations append/3 
* CE 40 is refined into CE [41] 
* CE 38 is refined into CE [42] 
* CE 39 is refined into CE [43] 


### Cost equations --> "Loop" of append/3 
* CEs [42] --> Loop 21 
* CEs [43] --> Loop 22 
* CEs [41] --> Loop 23 

### Ranking functions of CR append(V1,V,Out) 
* RF of phase [23]: [V1]

#### Partial ranking functions of CR append(V1,V,Out) 
* Partial RF of phase [23]:
  - RF of loop [23:1]:
    V1


### Specialization of cost equations appendAll/2 
* CE 27 is refined into CE [44,45,46,47] 
* CE 26 is refined into CE [48] 


### Cost equations --> "Loop" of appendAll/2 
* CEs [48] --> Loop 24 
* CEs [47] --> Loop 25 
* CEs [46] --> Loop 26 
* CEs [44] --> Loop 27 
* CEs [45] --> Loop 28 

### Ranking functions of CR appendAll(V1,Out) 
* RF of phase [25,26,27,28]: [V1]

#### Partial ranking functions of CR appendAll(V1,Out) 
* Partial RF of phase [25,26,27,28]:
  - RF of loop [25:1,26:1]:
    V1-1
  - RF of loop [27:1,28:1]:
    V1


### Specialization of cost equations appendAll2/2 
* CE 29 is refined into CE [49,50,51,52,53,54] 
* CE 28 is refined into CE [55] 


### Cost equations --> "Loop" of appendAll2/2 
* CEs [55] --> Loop 29 
* CEs [53] --> Loop 30 
* CEs [54] --> Loop 31 
* CEs [49,51] --> Loop 32 
* CEs [50,52] --> Loop 33 

### Ranking functions of CR appendAll2(V1,Out) 
* RF of phase [30,31,32,33]: [V1]

#### Partial ranking functions of CR appendAll2(V1,Out) 
* Partial RF of phase [30,31,32,33]:
  - RF of loop [30:1,31:1]:
    V1-2
  - RF of loop [32:1,33:1]:
    V1


### Specialization of cost equations appendAll3/2 
* CE 37 is refined into CE [56,57,58,59,60,61] 
* CE 36 is refined into CE [62] 


### Cost equations --> "Loop" of appendAll3/2 
* CEs [62] --> Loop 34 
* CEs [60] --> Loop 35 
* CEs [61] --> Loop 36 
* CEs [56,58] --> Loop 37 
* CEs [57,59] --> Loop 38 

### Ranking functions of CR appendAll3(V1,Out) 
* RF of phase [35,36,37,38]: [V1]

#### Partial ranking functions of CR appendAll3(V1,Out) 
* Partial RF of phase [35,36,37,38]:
  - RF of loop [35:1,36:1]:
    V1-2
  - RF of loop [37:1,38:1]:
    V1


### Specialization of cost equations fun/3 
* CE 31 is refined into CE [63] 
* CE 30 is refined into CE [64] 


### Cost equations --> "Loop" of fun/3 
* CEs [64] --> Loop 39 
* CEs [63] --> Loop 40 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [40]: [V1]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [40]:
  - RF of loop [40:1]:
    V1


### Specialization of cost equations fun2/2 
* CE 25 is refined into CE [65,66,67,68] 
* CE 24 is refined into CE [69] 


### Cost equations --> "Loop" of fun2/2 
* CEs [69] --> Loop 41 
* CEs [66,68] --> Loop 42 
* CEs [65,67] --> Loop 43 

### Ranking functions of CR fun2(V1,Out) 
* RF of phase [42,43]: [V1]

#### Partial ranking functions of CR fun2(V1,Out) 
* Partial RF of phase [42,43]:
  - RF of loop [42:1]:
    V1-1
  - RF of loop [43:1]:
    V1


### Specialization of cost equations fun4/2 
* CE 35 is refined into CE [70,71,72,73,74,75] 
* CE 33 is refined into CE [76,77] 
* CE 34 is refined into CE [78,79,80,81,82,83] 
* CE 32 is refined into CE [84] 


### Cost equations --> "Loop" of fun4/2 
* CEs [77] --> Loop 44 
* CEs [81,83] --> Loop 45 
* CEs [76,78,79,80,82] --> Loop 46 
* CEs [84] --> Loop 47 
* CEs [73,75] --> Loop 48 
* CEs [70,71,72,74] --> Loop 49 

### Ranking functions of CR fun4(V1,Out) 
* RF of phase [48,49]: [V1]

#### Partial ranking functions of CR fun4(V1,Out) 
* Partial RF of phase [48,49]:
  - RF of loop [48:1]:
    V1-2
  - RF of loop [49:1]:
    V1


### Specialization of cost equations fun7/2 
* CE 21 is refined into CE [85,86,87,88,89,90] 
* CE 22 is refined into CE [91,92,93] 
* CE 23 is refined into CE [94] 
* CE 20 is refined into CE [95,96,97,98,99,100] 


### Cost equations --> "Loop" of fun7/2 
* CEs [98,100] --> Loop 50 
* CEs [95,96,97,99] --> Loop 51 
* CEs [93] --> Loop 52 
* CEs [88,90] --> Loop 53 
* CEs [92] --> Loop 54 
* CEs [85,86,87,89,91] --> Loop 55 
* CEs [94] --> Loop 56 

### Ranking functions of CR fun7(V1,Out) 
* RF of phase [50,51]: [V1]

#### Partial ranking functions of CR fun7(V1,Out) 
* Partial RF of phase [50,51]:
  - RF of loop [50:1]:
    V1-2
  - RF of loop [51:1]:
    V1


### Specialization of cost equations start/2 
* CE 1 is refined into CE [101,102,103] 
* CE 2 is refined into CE [104] 
* CE 3 is refined into CE [105,106] 
* CE 4 is refined into CE [107,108,109,110,111,112] 
* CE 5 is refined into CE [113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130] 
* CE 6 is refined into CE [131,132,133,134,135,136,137,138] 
* CE 7 is refined into CE [139,140] 
* CE 8 is refined into CE [141,142,143,144,145,146,147,148,149,150,151,152] 
* CE 9 is refined into CE [153,154,155,156,157,158,159,160,161,162,163,164] 
* CE 10 is refined into CE [165,166,167,168,169,170,171,172] 
* CE 11 is refined into CE [173,174,175,176] 
* CE 12 is refined into CE [177,178] 
* CE 13 is refined into CE [179,180] 
* CE 14 is refined into CE [181,182,183] 
* CE 15 is refined into CE [184,185,186] 
* CE 16 is refined into CE [187,188,189,190] 
* CE 17 is refined into CE [191,192] 
* CE 18 is refined into CE [193,194] 
* CE 19 is refined into CE [195,196] 


### Cost equations --> "Loop" of start/2 
* CEs [101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196] --> Loop 57 

### Ranking functions of CR start(V1,V) 

#### Partial ranking functions of CR start(V1,V) 


Computing Bounds
=====================================

#### Cost of chains of append(V1,V,Out):
* Chain [[23],22]: 0
  with precondition: [V+V1=Out,V1>=1,V>=0] 

* Chain [[23],21]: 0
  with precondition: [V>=0,Out>=1,V1>=Out] 

* Chain [22]: 0
  with precondition: [V1=0,V=Out,V>=0] 

* Chain [21]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of appendAll(V1,Out):
* Chain [[25,26,27,28],24]: 0
  with precondition: [Out>=0,V1>=Out+1] 

* Chain [24]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of appendAll2(V1,Out):
* Chain [[30,31,32,33],29]: 0
  with precondition: [Out>=0,V1>=Out+1] 

* Chain [29]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of appendAll3(V1,Out):
* Chain [[35,36,37,38],34]: 0
  with precondition: [Out>=0,V1>=Out+1] 

* Chain [34]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[40],39]: 2*it(40)+1
  Such that:it(40) =< V1

  with precondition: [V>=0,Out>=3,2*V1+1>=Out] 

* Chain [39]: 1
  with precondition: [Out=1,V1>=0,V>=0] 


#### Cost of chains of fun2(V1,Out):
* Chain [[42,43],41]: 10*it(42)+1
  Such that:aux(10) =< V1
it(42) =< aux(10)

  with precondition: [Out>=4,3*V1+1>=Out] 

* Chain [41]: 1
  with precondition: [Out=1,V1>=0] 


#### Cost of chains of fun4(V1,Out):
* Chain [[48,49],47]: 10*it(48)+1
  Such that:aux(14) =< V1
it(48) =< aux(14)

  with precondition: [Out>=4,3*V1+1>=Out] 

* Chain [[48,49],46]: 10*it(48)+3
  Such that:aux(15) =< V1
it(48) =< aux(15)

  with precondition: [Out>=6,3*V1>=Out] 

* Chain [[48,49],45]: 14*it(48)+3
  Such that:aux(17) =< V1
it(48) =< aux(17)

  with precondition: [Out>=8,3*V1>=Out+4] 

* Chain [[48,49],44]: 20*it(48)+3
  Such that:aux(18) =< V1
it(48) =< aux(18)

  with precondition: [Out>=9,3*V1>=Out] 

* Chain [47]: 1
  with precondition: [Out=1,V1>=0] 

* Chain [46]: 3
  with precondition: [Out=3,V1>=1] 

* Chain [45]: 4*s(13)+3
  Such that:aux(16) =< V1
s(13) =< aux(16)

  with precondition: [Out>=5,2*V1>=Out+1] 

* Chain [44]: 10*s(16)+3
  Such that:s(15) =< V1
s(16) =< s(15)

  with precondition: [Out>=6,3*V1>=Out] 


#### Cost of chains of fun7(V1,Out):
* Chain [[50,51],56]: 10*it(50)+0
  Such that:aux(23) =< V1
it(50) =< aux(23)

  with precondition: [Out>=3,3*V1>=Out] 

* Chain [[50,51],55]: 10*it(50)+2
  Such that:aux(24) =< V1
it(50) =< aux(24)

  with precondition: [Out>=5,3*V1>=Out+1] 

* Chain [[50,51],54]: 10*it(50)+4
  Such that:aux(25) =< V1
it(50) =< aux(25)

  with precondition: [Out>=7,3*V1>=Out+2] 

* Chain [[50,51],53]: 14*it(50)+2
  Such that:aux(27) =< V1
it(50) =< aux(27)

  with precondition: [Out>=7,3*V1>=Out+5] 

* Chain [[50,51],52]: 78*it(50)+4
  Such that:aux(28) =< V1
it(50) =< aux(28)

  with precondition: [Out>=8,3*V1>=Out+1] 

* Chain [56]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [55]: 2
  with precondition: [Out=2,V1>=1] 

* Chain [54]: 4
  with precondition: [Out=4,V1>=2] 

* Chain [53]: 4*s(35)+2
  Such that:aux(26) =< V1
s(35) =< aux(26)

  with precondition: [Out>=4,2*V1>=Out+2] 

* Chain [52]: 68*s(38)+4
  Such that:s(37) =< V1
s(38) =< s(37)

  with precondition: [Out>=5,3*V1>=Out+1] 


#### Cost of chains of start(V1,V):
* Chain [57]: 952*s(54)+5
  Such that:aux(34) =< V1
s(54) =< aux(34)

  with precondition: [V1>=0] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [57] with precondition: [V1>=0] 
    - Upper bound: 952*V1+5 
    - Complexity: n 

### Maximum cost of start(V1,V): 952*V1+5 
Asymptotic class: n 
* Total analysis performed in 848 ms.


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

(18)
BOUNDS(1, n^1)

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

(19) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil
Tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL#1(nil) -> c5
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL2#1(nil) -> c9
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL3#1(nil) -> c13
S tuples:
   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL#1(nil) -> c5
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL2#1(nil) -> c9
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL3#1(nil) -> c13
K tuples:none
Defined Rule Symbols:   append_2, append#1_2, appendAll_1, appendAll#1_1, appendAll2_1, appendAll2#1_1, appendAll3_1, appendAll3#1_1

Defined Pair Symbols:   APPEND_2, APPEND#1_2, APPENDALL_1, APPENDALL#1_1, APPENDALL2_1, APPENDALL2#1_1, APPENDALL3_1, APPENDALL3#1_1

Compound Symbols:   c_1, c1_1, c2, c3_1, c4_2, c5, c6_1, c7_2, c8_2, c9, c10_1, c11_2, c12_2, c13


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

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

(22)
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:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL#1(nil) -> c5
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL2#1(nil) -> c9
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL3#1(nil) -> c13

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

   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil

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

(23) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(24)
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:

   APPEND(z0, z1) -> c(APPEND#1(z0, z1))
   APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
   APPEND#1(nil, z0) -> c2
   APPENDALL(z0) -> c3(APPENDALL#1(z0))
   APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
   APPENDALL#1(nil) -> c5
   APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
   APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
   APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
   APPENDALL2#1(nil) -> c9
   APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
   APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
   APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
   APPENDALL3#1(nil) -> c13

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

   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll3(z0) -> appendAll3#1(z0)
   appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
   appendAll3#1(nil) -> nil

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

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

(26)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil

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

(27) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
APPEND, APPEND#1, APPENDALL, APPENDALL#1, appendAll, APPENDALL2, APPENDALL2#1, appendAll2, APPENDALL3, APPENDALL3#1, appendAll3, append, append#1, appendAll#1, appendAll2#1, 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
appendAll < APPENDALL#1
appendAll < APPENDALL2#1
appendAll = appendAll#1
appendAll < appendAll2#1
APPENDALL2 = APPENDALL2#1
APPENDALL2 < APPENDALL3#1
appendAll2 < APPENDALL2#1
appendAll2 < APPENDALL3#1
appendAll2 = appendAll2#1
appendAll2 < appendAll3#1
APPENDALL3 = APPENDALL3#1
appendAll3 < APPENDALL3#1
appendAll3 = appendAll3#1
append = append#1
append < appendAll#1
append < appendAll2#1
append < appendAll3#1

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

(28)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
append#1, APPEND, APPEND#1, APPENDALL, APPENDALL#1, appendAll, APPENDALL2, APPENDALL2#1, appendAll2, APPENDALL3, APPENDALL3#1, appendAll3, append, appendAll#1, appendAll2#1, 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
appendAll < APPENDALL#1
appendAll < APPENDALL2#1
appendAll = appendAll#1
appendAll < appendAll2#1
APPENDALL2 = APPENDALL2#1
APPENDALL2 < APPENDALL3#1
appendAll2 < APPENDALL2#1
appendAll2 < APPENDALL3#1
appendAll2 = appendAll2#1
appendAll2 < appendAll3#1
APPENDALL3 = APPENDALL3#1
appendAll3 < APPENDALL3#1
appendAll3 = appendAll3#1
append = append#1
append < appendAll#1
append < appendAll2#1
append < appendAll3#1

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)

Induction Base:
append#1(gen_:::nil10_14(0), gen_:::nil10_14(b)) ->_R^Omega(0)
gen_:::nil10_14(b)

Induction Step:
append#1(gen_:::nil10_14(+(n12_14, 1)), gen_:::nil10_14(b)) ->_R^Omega(0)
::(nil, append(gen_:::nil10_14(n12_14), gen_:::nil10_14(b))) ->_R^Omega(0)
::(nil, append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b))) ->_IH
::(nil, gen_:::nil10_14(+(b, c13_14)))

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

(30)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
append, APPEND, APPEND#1, APPENDALL, APPENDALL#1, appendAll, APPENDALL2, APPENDALL2#1, appendAll2, APPENDALL3, APPENDALL3#1, appendAll3, appendAll#1, appendAll2#1, 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
appendAll < APPENDALL#1
appendAll < APPENDALL2#1
appendAll = appendAll#1
appendAll < appendAll2#1
APPENDALL2 = APPENDALL2#1
APPENDALL2 < APPENDALL3#1
appendAll2 < APPENDALL2#1
appendAll2 < APPENDALL3#1
appendAll2 = appendAll2#1
appendAll2 < appendAll3#1
APPENDALL3 = APPENDALL3#1
appendAll3 < APPENDALL3#1
appendAll3 = appendAll3#1
append = append#1
append < appendAll#1
append < appendAll2#1
append < appendAll3#1

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

(31) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)

Induction Base:
appendAll#1(gen_:::nil10_14(0)) ->_R^Omega(0)
nil

Induction Step:
appendAll#1(gen_:::nil10_14(+(n949_14, 1))) ->_R^Omega(0)
append(nil, appendAll(gen_:::nil10_14(n949_14))) ->_R^Omega(0)
append(nil, appendAll#1(gen_:::nil10_14(n949_14))) ->_IH
append(nil, gen_:::nil10_14(0)) ->_R^Omega(0)
append#1(nil, gen_:::nil10_14(0)) ->_L^Omega(0)
gen_:::nil10_14(+(0, 0))

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

(32)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
appendAll, APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, appendAll2, APPENDALL3, APPENDALL3#1, appendAll3, appendAll2#1, 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
appendAll < APPENDALL#1
appendAll < APPENDALL2#1
appendAll = appendAll#1
appendAll < appendAll2#1
APPENDALL2 = APPENDALL2#1
APPENDALL2 < APPENDALL3#1
appendAll2 < APPENDALL2#1
appendAll2 < APPENDALL3#1
appendAll2 = appendAll2#1
appendAll2 < appendAll3#1
APPENDALL3 = APPENDALL3#1
appendAll3 < APPENDALL3#1
appendAll3 = appendAll3#1

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

(33) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)

Induction Base:
appendAll2#1(gen_:::nil10_14(0)) ->_R^Omega(0)
nil

Induction Step:
appendAll2#1(gen_:::nil10_14(+(n1459_14, 1))) ->_R^Omega(0)
append(appendAll(nil), appendAll2(gen_:::nil10_14(n1459_14))) ->_R^Omega(0)
append(appendAll#1(nil), appendAll2(gen_:::nil10_14(n1459_14))) ->_L^Omega(0)
append(gen_:::nil10_14(0), appendAll2(gen_:::nil10_14(n1459_14))) ->_R^Omega(0)
append(gen_:::nil10_14(0), appendAll2#1(gen_:::nil10_14(n1459_14))) ->_IH
append(gen_:::nil10_14(0), gen_:::nil10_14(0)) ->_R^Omega(0)
append#1(gen_:::nil10_14(0), gen_:::nil10_14(0)) ->_L^Omega(0)
gen_:::nil10_14(+(0, 0))

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

(34)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
appendAll2, APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#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
appendAll2 < APPENDALL2#1
appendAll2 < APPENDALL3#1
appendAll2 = appendAll2#1
appendAll2 < appendAll3#1
APPENDALL3 = APPENDALL3#1
appendAll3 < APPENDALL3#1
appendAll3 = appendAll3#1

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)

Induction Base:
appendAll3#1(gen_:::nil10_14(0)) ->_R^Omega(0)
nil

Induction Step:
appendAll3#1(gen_:::nil10_14(+(n2503_14, 1))) ->_R^Omega(0)
append(appendAll2(nil), appendAll3(gen_:::nil10_14(n2503_14))) ->_R^Omega(0)
append(appendAll2#1(nil), appendAll3(gen_:::nil10_14(n2503_14))) ->_L^Omega(0)
append(gen_:::nil10_14(0), appendAll3(gen_:::nil10_14(n2503_14))) ->_R^Omega(0)
append(gen_:::nil10_14(0), appendAll3#1(gen_:::nil10_14(n2503_14))) ->_IH
append(gen_:::nil10_14(0), gen_:::nil10_14(0)) ->_R^Omega(0)
append#1(gen_:::nil10_14(0), gen_:::nil10_14(0)) ->_L^Omega(0)
gen_:::nil10_14(+(0, 0))

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

(36)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
appendAll3, 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
appendAll3 < APPENDALL3#1
appendAll3 = appendAll3#1

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND#1(gen_:::nil10_14(+(1, n3568_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n3568_14)

Induction Base:
APPEND#1(gen_:::nil10_14(+(1, 0)), gen_:::nil10_14(b))

Induction Step:
APPEND#1(gen_:::nil10_14(+(1, +(n3568_14, 1))), gen_:::nil10_14(b)) ->_R^Omega(1)
c1(APPEND(gen_:::nil10_14(+(1, n3568_14)), gen_:::nil10_14(b))) ->_R^Omega(1)
c1(c(APPEND#1(gen_:::nil10_14(+(1, n3568_14)), gen_:::nil10_14(b)))) ->_IH
c1(c(*11_14))

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

(38)
Complex Obligation (BEST)

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

(39)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)


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

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

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

(41)
BOUNDS(n^1, INF)

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

(42)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n3568_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n3568_14)


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

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

(43) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)

Induction Base:
APPEND(gen_:::nil10_14(0), gen_:::nil10_14(b))

Induction Step:
APPEND(gen_:::nil10_14(+(n4713_14, 1)), gen_:::nil10_14(b)) ->_R^Omega(1)
c(APPEND#1(gen_:::nil10_14(+(n4713_14, 1)), gen_:::nil10_14(b))) ->_R^Omega(1)
c(c1(APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)))) ->_IH
c(c1(*11_14))

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

(44)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n3568_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n3568_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
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

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

(45) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)

Induction Base:
APPEND#1(gen_:::nil10_14(+(1, 0)), gen_:::nil10_14(b))

Induction Step:
APPEND#1(gen_:::nil10_14(+(1, +(n7182_14, 1))), gen_:::nil10_14(b)) ->_R^Omega(1)
c1(APPEND(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b))) ->_R^Omega(1)
c1(c(APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)))) ->_IH
c1(c(*11_14))

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

(46)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)


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

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

(47) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPENDALL#1(gen_:::nil10_14(+(1, n11259_14))) -> *11_14, rt in Omega(n11259_14)

Induction Base:
APPENDALL#1(gen_:::nil10_14(+(1, 0)))

Induction Step:
APPENDALL#1(gen_:::nil10_14(+(1, +(n11259_14, 1)))) ->_R^Omega(1)
c4(APPEND(nil, appendAll(gen_:::nil10_14(+(1, n11259_14)))), APPENDALL(gen_:::nil10_14(+(1, n11259_14)))) ->_R^Omega(0)
c4(APPEND(nil, appendAll#1(gen_:::nil10_14(+(1, n11259_14)))), APPENDALL(gen_:::nil10_14(+(1, n11259_14)))) ->_L^Omega(0)
c4(APPEND(nil, gen_:::nil10_14(0)), APPENDALL(gen_:::nil10_14(+(1, n11259_14)))) ->_R^Omega(1)
c4(c(APPEND#1(nil, gen_:::nil10_14(0))), APPENDALL(gen_:::nil10_14(+(1, n11259_14)))) ->_R^Omega(1)
c4(c(c2), APPENDALL(gen_:::nil10_14(+(1, n11259_14)))) ->_R^Omega(1)
c4(c(c2), c3(APPENDALL#1(gen_:::nil10_14(+(1, n11259_14))))) ->_IH
c4(c(c2), c3(*11_14))

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

(48)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)
APPENDALL#1(gen_:::nil10_14(+(1, n11259_14))) -> *11_14, rt in Omega(n11259_14)


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

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

(49) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPENDALL(gen_:::nil10_14(n15603_14)) -> *11_14, rt in Omega(n15603_14)

Induction Base:
APPENDALL(gen_:::nil10_14(0))

Induction Step:
APPENDALL(gen_:::nil10_14(+(n15603_14, 1))) ->_R^Omega(1)
c3(APPENDALL#1(gen_:::nil10_14(+(n15603_14, 1)))) ->_R^Omega(1)
c3(c4(APPEND(nil, appendAll(gen_:::nil10_14(n15603_14))), APPENDALL(gen_:::nil10_14(n15603_14)))) ->_R^Omega(0)
c3(c4(APPEND(nil, appendAll#1(gen_:::nil10_14(n15603_14))), APPENDALL(gen_:::nil10_14(n15603_14)))) ->_L^Omega(0)
c3(c4(APPEND(nil, gen_:::nil10_14(0)), APPENDALL(gen_:::nil10_14(n15603_14)))) ->_R^Omega(1)
c3(c4(c(APPEND#1(nil, gen_:::nil10_14(0))), APPENDALL(gen_:::nil10_14(n15603_14)))) ->_R^Omega(1)
c3(c4(c(c2), APPENDALL(gen_:::nil10_14(n15603_14)))) ->_IH
c3(c4(c(c2), *11_14))

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

(50)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)
APPENDALL#1(gen_:::nil10_14(+(1, n11259_14))) -> *11_14, rt in Omega(n11259_14)
APPENDALL(gen_:::nil10_14(n15603_14)) -> *11_14, rt in Omega(n15603_14)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


The following defined symbols remain to be analysed:
APPENDALL#1, 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

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

(51) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPENDALL#1(gen_:::nil10_14(+(1, n19150_14))) -> *11_14, rt in Omega(n19150_14)

Induction Base:
APPENDALL#1(gen_:::nil10_14(+(1, 0)))

Induction Step:
APPENDALL#1(gen_:::nil10_14(+(1, +(n19150_14, 1)))) ->_R^Omega(1)
c4(APPEND(nil, appendAll(gen_:::nil10_14(+(1, n19150_14)))), APPENDALL(gen_:::nil10_14(+(1, n19150_14)))) ->_R^Omega(0)
c4(APPEND(nil, appendAll#1(gen_:::nil10_14(+(1, n19150_14)))), APPENDALL(gen_:::nil10_14(+(1, n19150_14)))) ->_L^Omega(0)
c4(APPEND(nil, gen_:::nil10_14(0)), APPENDALL(gen_:::nil10_14(+(1, n19150_14)))) ->_R^Omega(1)
c4(c(APPEND#1(nil, gen_:::nil10_14(0))), APPENDALL(gen_:::nil10_14(+(1, n19150_14)))) ->_R^Omega(1)
c4(c(c2), APPENDALL(gen_:::nil10_14(+(1, n19150_14)))) ->_R^Omega(1)
c4(c(c2), c3(APPENDALL#1(gen_:::nil10_14(+(1, n19150_14))))) ->_IH
c4(c(c2), c3(*11_14))

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

(52)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)
APPENDALL#1(gen_:::nil10_14(+(1, n19150_14))) -> *11_14, rt in Omega(n19150_14)
APPENDALL(gen_:::nil10_14(n15603_14)) -> *11_14, rt in Omega(n15603_14)


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

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

(53) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPENDALL2#1(gen_:::nil10_14(+(1, n24836_14))) -> *11_14, rt in Omega(n24836_14)

Induction Base:
APPENDALL2#1(gen_:::nil10_14(+(1, 0)))

Induction Step:
APPENDALL2#1(gen_:::nil10_14(+(1, +(n24836_14, 1)))) ->_R^Omega(1)
c8(APPEND(appendAll(nil), appendAll2(gen_:::nil10_14(+(1, n24836_14)))), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_R^Omega(0)
c8(APPEND(appendAll#1(nil), appendAll2(gen_:::nil10_14(+(1, n24836_14)))), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_L^Omega(0)
c8(APPEND(gen_:::nil10_14(0), appendAll2(gen_:::nil10_14(+(1, n24836_14)))), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_R^Omega(0)
c8(APPEND(gen_:::nil10_14(0), appendAll2#1(gen_:::nil10_14(+(1, n24836_14)))), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_L^Omega(0)
c8(APPEND(gen_:::nil10_14(0), gen_:::nil10_14(0)), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_R^Omega(1)
c8(c(APPEND#1(gen_:::nil10_14(0), gen_:::nil10_14(0))), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_R^Omega(1)
c8(c(c2), APPENDALL2(gen_:::nil10_14(+(1, n24836_14)))) ->_R^Omega(1)
c8(c(c2), c6(APPENDALL2#1(gen_:::nil10_14(+(1, n24836_14))))) ->_IH
c8(c(c2), c6(*11_14))

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

(54)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)
APPENDALL#1(gen_:::nil10_14(+(1, n19150_14))) -> *11_14, rt in Omega(n19150_14)
APPENDALL(gen_:::nil10_14(n15603_14)) -> *11_14, rt in Omega(n15603_14)
APPENDALL2#1(gen_:::nil10_14(+(1, n24836_14))) -> *11_14, rt in Omega(n24836_14)


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

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

(55) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
APPENDALL2(gen_:::nil10_14(n49022_14)) -> *11_14, rt in Omega(n49022_14)

Induction Base:
APPENDALL2(gen_:::nil10_14(0))

Induction Step:
APPENDALL2(gen_:::nil10_14(+(n49022_14, 1))) ->_R^Omega(1)
c6(APPENDALL2#1(gen_:::nil10_14(+(n49022_14, 1)))) ->_R^Omega(1)
c6(c8(APPEND(appendAll(nil), appendAll2(gen_:::nil10_14(n49022_14))), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_R^Omega(0)
c6(c8(APPEND(appendAll#1(nil), appendAll2(gen_:::nil10_14(n49022_14))), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_L^Omega(0)
c6(c8(APPEND(gen_:::nil10_14(0), appendAll2(gen_:::nil10_14(n49022_14))), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_R^Omega(0)
c6(c8(APPEND(gen_:::nil10_14(0), appendAll2#1(gen_:::nil10_14(n49022_14))), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_L^Omega(0)
c6(c8(APPEND(gen_:::nil10_14(0), gen_:::nil10_14(0)), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_R^Omega(1)
c6(c8(c(APPEND#1(gen_:::nil10_14(0), gen_:::nil10_14(0))), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_R^Omega(1)
c6(c8(c(c2), APPENDALL2(gen_:::nil10_14(n49022_14)))) ->_IH
c6(c8(c(c2), *11_14))

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

(56)
Obligation:
Innermost TRS:
Rules:
APPEND(z0, z1) -> c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) -> c1(APPEND(z1, z2))
APPEND#1(nil, z0) -> c2
APPENDALL(z0) -> c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) -> c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPENDALL#1(nil) -> c5
APPENDALL2(z0) -> c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) -> c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0))
APPENDALL2#1(::(z0, z1)) -> c8(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL2(z1))
APPENDALL2#1(nil) -> c9
APPENDALL3(z0) -> c10(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) -> c11(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0))
APPENDALL3#1(::(z0, z1)) -> c12(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL3(z1))
APPENDALL3#1(nil) -> c13
append(z0, z1) -> append#1(z0, z1)
append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
append#1(nil, z0) -> z0
appendAll(z0) -> appendAll#1(z0)
appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
appendAll#1(nil) -> nil
appendAll2(z0) -> appendAll2#1(z0)
appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
appendAll2#1(nil) -> nil
appendAll3(z0) -> appendAll3#1(z0)
appendAll3#1(::(z0, z1)) -> append(appendAll2(z0), appendAll3(z1))
appendAll3#1(nil) -> nil

Types:
APPEND :: :::nil -> :::nil -> c
c :: c1:c2 -> c
APPEND#1 :: :::nil -> :::nil -> c1:c2
:: :: :::nil -> :::nil -> :::nil
c1 :: c -> c1:c2
nil :: :::nil
c2 :: c1:c2
APPENDALL :: :::nil -> c3
c3 :: c4:c5 -> c3
APPENDALL#1 :: :::nil -> c4:c5
c4 :: c -> c3 -> c4:c5
appendAll :: :::nil -> :::nil
c5 :: c4:c5
APPENDALL2 :: :::nil -> c6
c6 :: c7:c8:c9 -> c6
APPENDALL2#1 :: :::nil -> c7:c8:c9
c7 :: c -> c3 -> c7:c8:c9
appendAll2 :: :::nil -> :::nil
c8 :: c -> c6 -> c7:c8:c9
c9 :: c7:c8:c9
APPENDALL3 :: :::nil -> c10
c10 :: c11:c12:c13 -> c10
APPENDALL3#1 :: :::nil -> c11:c12:c13
c11 :: c -> c6 -> c11:c12:c13
appendAll3 :: :::nil -> :::nil
c12 :: c -> c10 -> c11:c12:c13
c13 :: c11:c12:c13
append :: :::nil -> :::nil -> :::nil
append#1 :: :::nil -> :::nil -> :::nil
appendAll#1 :: :::nil -> :::nil
appendAll2#1 :: :::nil -> :::nil
appendAll3#1 :: :::nil -> :::nil
hole_c1_14 :: c
hole_:::nil2_14 :: :::nil
hole_c1:c23_14 :: c1:c2
hole_c34_14 :: c3
hole_c4:c55_14 :: c4:c5
hole_c66_14 :: c6
hole_c7:c8:c97_14 :: c7:c8:c9
hole_c108_14 :: c10
hole_c11:c12:c139_14 :: c11:c12:c13
gen_:::nil10_14 :: Nat -> :::nil


Lemmas:
append#1(gen_:::nil10_14(n12_14), gen_:::nil10_14(b)) -> gen_:::nil10_14(+(n12_14, b)), rt in Omega(0)
appendAll#1(gen_:::nil10_14(n949_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll2#1(gen_:::nil10_14(n1459_14)) -> gen_:::nil10_14(0), rt in Omega(0)
appendAll3#1(gen_:::nil10_14(n2503_14)) -> gen_:::nil10_14(0), rt in Omega(0)
APPEND#1(gen_:::nil10_14(+(1, n7182_14)), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n7182_14)
APPEND(gen_:::nil10_14(n4713_14), gen_:::nil10_14(b)) -> *11_14, rt in Omega(n4713_14)
APPENDALL#1(gen_:::nil10_14(+(1, n19150_14))) -> *11_14, rt in Omega(n19150_14)
APPENDALL(gen_:::nil10_14(n15603_14)) -> *11_14, rt in Omega(n15603_14)
APPENDALL2#1(gen_:::nil10_14(+(1, n24836_14))) -> *11_14, rt in Omega(n24836_14)
APPENDALL2(gen_:::nil10_14(n49022_14)) -> *11_14, rt in Omega(n49022_14)


Generator Equations:
gen_:::nil10_14(0) <=> nil
gen_:::nil10_14(+(x, 1)) <=> ::(nil, gen_:::nil10_14(x))


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

They will be analysed ascendingly in the following order:
APPENDALL2 = APPENDALL2#1
APPENDALL2 < APPENDALL3#1
APPENDALL3 = APPENDALL3#1