WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 204 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 6 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 141 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 74 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 51 ms]
    (16) CdtProblem
    (17) CdtKnowledgeProof [FINISHED, 0 ms]
    (18) BOUNDS(1, 1)
(19) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(20) TRS for Loop Detection
    (21) DecreasingLoopProof [LOWER BOUND(ID), 77 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) TRS for Loop Detection


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

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^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))
   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
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^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))
   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
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(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
   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
Tuples:
   APPEND'(z0, z1) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPEND#1'(nil, z0) -> c16
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL#1'(nil) -> c19
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL2#1'(nil) -> c22
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPENDALL3#1'(nil) -> c25
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPEND#1''(nil, z0) -> c28
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL#1''(nil) -> c31
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c33(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL2#1''(nil) -> c35
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c37(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL2''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL3#1''(nil) -> c39
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPEND#1''(nil, z0) -> c28
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL#1''(nil) -> c31
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c33(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL2#1''(nil) -> c35
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c37(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL2''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL3#1''(nil) -> c39
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, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c16, c17_1, c18_2, c19, c20_1, c21_3, c22, c23_1, c24_3, c25, c26_1, c27_1, c28, c29_1, c30_3, c31, c32_1, c33_4, c34_4, c35, c36_1, c37_4, c38_4, c39


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 8 trailing nodes:
   APPENDALL#1'(nil) -> c19
   APPEND#1'(nil, z0) -> c16
   APPENDALL2#1''(nil) -> c35
   APPEND#1''(nil, z0) -> c28
   APPENDALL3#1'(nil) -> c25
   APPENDALL3#1''(nil) -> c39
   APPENDALL2#1'(nil) -> c22
   APPENDALL#1''(nil) -> c31

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

(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
   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
Tuples:
   APPEND'(z0, z1) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c33(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c37(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL2''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c33(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c37(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL2''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), 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, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c17_1, c18_2, c20_1, c21_3, c23_1, c24_3, c26_1, c27_1, c29_1, c30_3, c32_1, c33_4, c34_4, c36_1, c37_4, c38_4


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

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

(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
   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
Tuples:
   APPEND'(z0, z1) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(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, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c17_1, c18_2, c20_1, c21_3, c23_1, c24_3, c26_1, c27_1, c29_1, c30_3, c32_1, c34_4, c36_1, c38_4, c16_1


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

(9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   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

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   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) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
K tuples:none
Defined Rule Symbols:   appendAll_1, appendAll#1_1, append_2, append#1_2, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c17_1, c18_2, c20_1, c21_3, c23_1, c24_3, c26_1, c27_1, c29_1, c30_3, c32_1, c34_4, c36_1, c38_4, c16_1


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

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   APPEND'(z0, z1) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(::(x_1, x_2)) = x_1 + x_2
   POL(APPEND#1'(x_1, x_2)) = 0
   POL(APPEND#1''(x_1, x_2)) = 0
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = 0
   POL(APPENDALL#1'(x_1)) = 0
   POL(APPENDALL#1''(x_1)) = 0
   POL(APPENDALL'(x_1)) = 0
   POL(APPENDALL''(x_1)) = 0
   POL(APPENDALL2#1'(x_1)) = 0
   POL(APPENDALL2#1''(x_1)) = 0
   POL(APPENDALL2'(x_1)) = 0
   POL(APPENDALL2''(x_1)) = 0
   POL(APPENDALL3#1'(x_1)) = 0
   POL(APPENDALL3#1''(x_1)) = [1] + x_1
   POL(APPENDALL3'(x_1)) = 0
   POL(APPENDALL3''(x_1)) = [1] + x_1
   POL(append(x_1, x_2)) = 0
   POL(append#1(x_1, x_2)) = [1] + x_1 + x_2
   POL(appendAll(x_1)) = x_1
   POL(appendAll#1(x_1)) = [1] + x_1
   POL(appendAll2(x_1)) = x_1
   POL(appendAll2#1(x_1)) = [1] + x_1
   POL(appendAll3(x_1)) = [1] + x_1
   POL(appendAll3#1(x_1)) = [1] + x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c17(x_1)) = x_1
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c20(x_1)) = x_1
   POL(c21(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c29(x_1)) = x_1
   POL(c30(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c32(x_1)) = x_1
   POL(c34(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c36(x_1)) = x_1
   POL(c38(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(nil) = [1]

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   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) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
K tuples:
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
Defined Rule Symbols:   appendAll_1, appendAll#1_1, append_2, append#1_2, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c17_1, c18_2, c20_1, c21_3, c23_1, c24_3, c26_1, c27_1, c29_1, c30_3, c32_1, c34_4, c36_1, c38_4, c16_1


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

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
We considered the (Usable) Rules:none
And the Tuples:
   APPEND'(z0, z1) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(::(x_1, x_2)) = x_1 + x_2
   POL(APPEND#1'(x_1, x_2)) = 0
   POL(APPEND#1''(x_1, x_2)) = 0
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = 0
   POL(APPENDALL#1'(x_1)) = 0
   POL(APPENDALL#1''(x_1)) = 0
   POL(APPENDALL'(x_1)) = 0
   POL(APPENDALL''(x_1)) = 0
   POL(APPENDALL2#1'(x_1)) = 0
   POL(APPENDALL2#1''(x_1)) = [1]
   POL(APPENDALL2'(x_1)) = 0
   POL(APPENDALL2''(x_1)) = [1]
   POL(APPENDALL3#1'(x_1)) = 0
   POL(APPENDALL3#1''(x_1)) = [1] + x_1
   POL(APPENDALL3'(x_1)) = 0
   POL(APPENDALL3''(x_1)) = [1] + x_1
   POL(append(x_1, x_2)) = 0
   POL(append#1(x_1, x_2)) = [1] + x_1 + x_2
   POL(appendAll(x_1)) = x_1
   POL(appendAll#1(x_1)) = [1] + x_1
   POL(appendAll2(x_1)) = x_1
   POL(appendAll2#1(x_1)) = [1] + x_1
   POL(appendAll3(x_1)) = [1] + x_1
   POL(appendAll3#1(x_1)) = [1] + x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c17(x_1)) = x_1
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c20(x_1)) = x_1
   POL(c21(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c29(x_1)) = x_1
   POL(c30(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c32(x_1)) = x_1
   POL(c34(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c36(x_1)) = x_1
   POL(c38(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(nil) = [1]

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   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) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
K tuples:
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
Defined Rule Symbols:   appendAll_1, appendAll#1_1, append_2, append#1_2, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c17_1, c18_2, c20_1, c21_3, c23_1, c24_3, c26_1, c27_1, c29_1, c30_3, c32_1, c34_4, c36_1, c38_4, c16_1


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
We considered the (Usable) Rules:
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   append(z0, z1) -> append#1(z0, z1)
   append#1(nil, z0) -> z0
   appendAll(z0) -> appendAll#1(z0)
   appendAll2(z0) -> appendAll2#1(z0)
   appendAll2#1(::(z0, z1)) -> append(appendAll(z0), appendAll2(z1))
   appendAll2#1(nil) -> nil
   appendAll#1(nil) -> nil
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
And the Tuples:
   APPEND'(z0, z1) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(::(x_1, x_2)) = [1] + x_1 + x_2
   POL(APPEND#1'(x_1, x_2)) = 0
   POL(APPEND#1''(x_1, x_2)) = x_1
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = x_1
   POL(APPENDALL#1'(x_1)) = 0
   POL(APPENDALL#1''(x_1)) = x_1
   POL(APPENDALL'(x_1)) = 0
   POL(APPENDALL''(x_1)) = x_1
   POL(APPENDALL2#1'(x_1)) = 0
   POL(APPENDALL2#1''(x_1)) = [1] + x_1
   POL(APPENDALL2'(x_1)) = 0
   POL(APPENDALL2''(x_1)) = [1] + x_1
   POL(APPENDALL3#1'(x_1)) = 0
   POL(APPENDALL3#1''(x_1)) = x_1
   POL(APPENDALL3'(x_1)) = 0
   POL(APPENDALL3''(x_1)) = x_1
   POL(append(x_1, x_2)) = x_1 + x_2
   POL(append#1(x_1, x_2)) = x_1 + x_2
   POL(appendAll(x_1)) = x_1
   POL(appendAll#1(x_1)) = x_1
   POL(appendAll2(x_1)) = x_1
   POL(appendAll2#1(x_1)) = x_1
   POL(appendAll3(x_1)) = [1] + x_1
   POL(appendAll3#1(x_1)) = [1] + x_1
   POL(c14(x_1)) = x_1
   POL(c15(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c17(x_1)) = x_1
   POL(c18(x_1, x_2)) = x_1 + x_2
   POL(c20(x_1)) = x_1
   POL(c21(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c23(x_1)) = x_1
   POL(c24(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c29(x_1)) = x_1
   POL(c30(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c32(x_1)) = x_1
   POL(c34(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c36(x_1)) = x_1
   POL(c38(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(nil) = [1]

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   appendAll(z0) -> appendAll#1(z0)
   appendAll#1(::(z0, z1)) -> append(z0, appendAll(z1))
   appendAll#1(nil) -> nil
   append(z0, z1) -> append#1(z0, z1)
   append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2))
   append#1(nil, z0) -> z0
   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) -> c14(APPEND#1'(z0, z1))
   APPEND#1'(::(z0, z1), z2) -> c15(APPEND'(z1, z2))
   APPENDALL'(z0) -> c17(APPENDALL#1'(z0))
   APPENDALL#1'(::(z0, z1)) -> c18(APPEND'(z0, appendAll(z1)), APPENDALL'(z1))
   APPENDALL2'(z0) -> c20(APPENDALL2#1'(z0))
   APPENDALL2#1'(::(z0, z1)) -> c21(APPEND'(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1))
   APPENDALL3'(z0) -> c23(APPENDALL3#1'(z0))
   APPENDALL3#1'(::(z0, z1)) -> c24(APPEND'(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1))
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
S tuples:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
K tuples:
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
Defined Rule Symbols:   appendAll_1, appendAll#1_1, append_2, append#1_2, 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, APPEND''_2, APPEND#1''_2, APPENDALL''_1, APPENDALL#1''_1, APPENDALL2''_1, APPENDALL2#1''_1, APPENDALL3''_1, APPENDALL3#1''_1

Compound Symbols:   c14_1, c15_1, c17_1, c18_2, c20_1, c21_3, c23_1, c24_3, c26_1, c27_1, c29_1, c30_3, c32_1, c34_4, c36_1, c38_4, c16_1


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

(17) CdtKnowledgeProof (FINISHED)
The following tuples could be moved from S to K by knowledge propagation:
   APPEND''(z0, z1) -> c26(APPEND#1''(z0, z1))
   APPENDALL''(z0) -> c29(APPENDALL#1''(z0))
   APPENDALL2''(z0) -> c32(APPENDALL2#1''(z0))
   APPENDALL3''(z0) -> c36(APPENDALL3#1''(z0))
   APPEND#1''(::(z0, z1), z2) -> c27(APPEND''(z1, z2))
   APPENDALL#1''(::(z0, z1)) -> c30(APPEND''(z0, appendAll(z1)), APPENDALL'(z1), APPENDALL''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c34(APPEND''(appendAll(z0), appendAll2(z1)), APPENDALL'(z0), APPENDALL2'(z1), APPENDALL2''(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPEND''(appendAll(z0), appendAll2(z1)))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL'(z0))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL2'(z1))
   APPENDALL2#1''(::(z0, z1)) -> c16(APPENDALL''(z0))
   APPENDALL3#1''(::(z0, z1)) -> c38(APPEND''(appendAll2(z0), appendAll3(z1)), APPENDALL2'(z0), APPENDALL3'(z1), APPENDALL3''(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPEND''(appendAll2(z0), appendAll3(z1)))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2'(z0))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL3'(z1))
   APPENDALL3#1''(::(z0, z1)) -> c16(APPENDALL2''(z0))
Now S is empty
----------------------------------------

(18)
BOUNDS(1, 1)

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

(19) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(20)
Obligation:
Analyzing the following TRS for decreasing loops:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^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))
   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
----------------------------------------

(21) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

APPENDALL2(::(z01_1, z12_1)) ->^+ c6(c8(APPEND(appendAll(z01_1), appendAll2(z12_1)), APPENDALL2(z12_1)))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1].

The pumping substitution is [z12_1 / ::(z01_1, z12_1)].

The result substitution is [ ].




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

(22)
Complex Obligation (BEST)

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

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

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^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))
   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
----------------------------------------

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

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Analyzing the following TRS for decreasing loops:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^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))
   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