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

(0) Obligation:

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

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

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS 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(z1))
APPENDALL2#1(nil) → c8
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL3#1(nil) → c11

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(z1))
APPENDALL2#1(nil) → c8
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL3#1(nil) → c11

K tuples:none
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11

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

Removed 4 trailing nodes:

APPENDALL3#1(nil) → c11
APPENDALL#1(nil) → c5
APPEND#1(nil, z0) → c2
APPENDALL2#1(nil) → c8

(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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

K tuples:none
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(5) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

We considered the (Usable) Rules:none
And the 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [1] + x₂   
POL(APPEND(x₁, x₂)) = 0   
POL(APPEND#1(x₁, x₂)) = 0   
POL(APPENDALL(x₁)) = 0   
POL(APPENDALL#1(x₁)) = 0   
POL(APPENDALL2(x₁)) = 0   
POL(APPENDALL2#1(x₁)) = 0   
POL(APPENDALL3(x₁)) = [4] + [4]x₁   
POL(APPENDALL3#1(x₁)) = [3] + [4]x₁   
POL(append(x₁, x₂)) = [2]   
POL(append#1(x₁, x₂)) = [3]   
POL(appendAll(x₁)) = [4]   
POL(appendAll#1(x₁)) = [2] + [3]x₁   
POL(appendAll2(x₁)) = [1]   
POL(appendAll2#1(x₁)) = [2] + [3]x₁   
POL(appendAll3(x₁)) = [1] + [3]x₁   
POL(appendAll3#1(x₁)) = [4]x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = 0   

(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)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), 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(z1))

K tuples:

APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(7) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))

We considered the (Usable) Rules:none
And the 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [5] + x₁ + x₂   
POL(APPEND(x₁, x₂)) = 0   
POL(APPEND#1(x₁, x₂)) = 0   
POL(APPENDALL(x₁)) = [4]   
POL(APPENDALL#1(x₁)) = [4]   
POL(APPENDALL2(x₁)) = [2] + [3]x₁   
POL(APPENDALL2#1(x₁)) = [1] + [3]x₁   
POL(APPENDALL3(x₁)) = [1] + [3]x₁   
POL(APPENDALL3#1(x₁)) = [1] + [3]x₁   
POL(append(x₁, x₂)) = [5] + x₁   
POL(append#1(x₁, x₂)) = [2] + [3]x₁ + [5]x₂   
POL(appendAll(x₁)) = [1]   
POL(appendAll#1(x₁)) = [3] + [2]x₁   
POL(appendAll2(x₁)) = [2] + [4]x₁   
POL(appendAll2#1(x₁)) = [2] + [3]x₁   
POL(appendAll3(x₁)) = [2] + [3]x₁   
POL(appendAll3#1(x₁)) = [3] + [3]x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = [5]   

(8) 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), 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))

K tuples:

APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(9) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))

We considered the (Usable) Rules:none
And the 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [2] + x₁ + x₂   
POL(APPEND(x₁, x₂)) = 0   
POL(APPEND#1(x₁, x₂)) = 0   
POL(APPENDALL(x₁)) = [4] + [4]x₁   
POL(APPENDALL#1(x₁)) = [4]x₁   
POL(APPENDALL2(x₁)) = [4] + [4]x₁   
POL(APPENDALL2#1(x₁)) = [4] + [4]x₁   
POL(APPENDALL3(x₁)) = [5] + [4]x₁   
POL(APPENDALL3#1(x₁)) = [1] + [4]x₁   
POL(append(x₁, x₂)) = [2]   
POL(append#1(x₁, x₂)) = [4] + [3]x₁ + [3]x₂   
POL(appendAll(x₁)) = [1] + [3]x₁   
POL(appendAll#1(x₁)) = [5]x₁   
POL(appendAll2(x₁)) = [5] + x₁   
POL(appendAll2#1(x₁)) = [5] + x₁   
POL(appendAll3(x₁)) = [2] + [5]x₁   
POL(appendAll3#1(x₁)) = [2] + [3]x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = 0   

(10) 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

K tuples:

APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(11) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

We considered the (Usable) Rules:

append#1(nil, z0) → z0
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1))
appendAll(z0) → appendAll#1(z0)
appendAll2#1(nil) → nil
append(z0, z1) → append#1(z0, z1)
appendAll2(z0) → appendAll2#1(z0)
appendAll#1(nil) → nil
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2))
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1))

And the 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(::(x₁, x₂)) = [4] + x₁ + x₂   
POL(APPEND(x₁, x₂)) = [4] + x₁   
POL(APPEND#1(x₁, x₂)) = [2] + x₁   
POL(APPENDALL(x₁)) = x₁   
POL(APPENDALL#1(x₁)) = x₁   
POL(APPENDALL2(x₁)) = [3]x₁   
POL(APPENDALL2#1(x₁)) = [3]x₁   
POL(APPENDALL3(x₁)) = [2] + [5]x₁   
POL(APPENDALL3#1(x₁)) = [1] + [5]x₁   
POL(append(x₁, x₂)) = [1] + x₁ + x₂   
POL(append#1(x₁, x₂)) = [1] + x₁ + x₂   
POL(appendAll(x₁)) = [1] + [2]x₁   
POL(appendAll#1(x₁)) = [2]x₁   
POL(appendAll2(x₁)) = [2]x₁   
POL(appendAll2#1(x₁)) = [2]x₁   
POL(appendAll3(x₁)) = [3] + [3]x₁   
POL(appendAll3#1(x₁)) = [2] + [2]x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c9(x₁)) = x₁   
POL(nil) = 0   

(12) 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(z1))
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))

S tuples:none
K tuples:

APPENDALL3(z0) → c9(APPENDALL3#1(z0))
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
APPENDALL2(z0) → c6(APPENDALL2#1(z0))
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1))
APPENDALL(z0) → c3(APPENDALL#1(z0))
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
APPEND(z0, z1) → c(APPEND#1(z0, z1))
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))

Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

(13) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(14) BOUNDS(O(1), O(1))