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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 785 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 151 ms]
    (14) CdtProblem
    (15) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (16) CdtProblem
    (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 2807 ms]
    (18) CdtProblem
    (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 1829 ms]
    (20) CdtProblem
    (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 1555 ms]
    (22) CdtProblem
    (23) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 1307 ms]
    (24) CdtProblem
    (25) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) BOUNDS(1, 1)
(27) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(28) CpxRelTRS
    (29) SlicingProof [LOWER BOUND(ID), 0 ms]
    (30) CpxRelTRS
    (31) TypeInferenceProof [BOTH BOUNDS(ID, ID), 4 ms]
    (32) typed CpxTrs
    (33) OrderProof [LOWER BOUND(ID), 0 ms]
    (34) typed CpxTrs
    (35) RewriteLemmaProof [LOWER BOUND(ID), 344 ms]
    (36) BEST
        (37) proven lower bound
            (38) LowerBoundPropagationProof [FINISHED, 0 ms]
            (39) BOUNDS(n^1, INF)
        (40) typed CpxTrs
            (41) RewriteLemmaProof [LOWER BOUND(ID), 66 ms]
            (42) typed CpxTrs


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

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


The TRS R consists of the following rules:

   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))

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

   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))

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^2).


The TRS R consists of the following rules:

   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))

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

   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))

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

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

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
Tuples:
   LT'(0, s(z0)) -> c14
   LT'(s(z0), 0) -> c15
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(nil, z0) -> c17
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, nil) -> c19
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(F_2'(lt(z2, z3), z2, z3, z4, z0, z1), LT'(z2, z3))
   F_2'(true, z0, z1, z2, z3, z4) -> c22
   F_2'(false, z0, z1, z2, z3, z4) -> c23
   QSORT'(nil) -> c24
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(0, s(z0)) -> c27
   LT''(s(z0), 0) -> c28
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(nil, z0) -> c30
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, nil) -> c32
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   F_1''(pair(z0, z1), z2, z3, z4) -> c34(F_2''(lt(z2, z3), z2, z3, z4, z0, z1), LT'(z2, z3), LT''(z2, z3))
   F_2''(true, z0, z1, z2, z3, z4) -> c35
   F_2''(false, z0, z1, z2, z3, z4) -> c36
   QSORT''(nil) -> c37
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
S tuples:
   LT''(0, s(z0)) -> c27
   LT''(s(z0), 0) -> c28
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(nil, z0) -> c30
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, nil) -> c32
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   F_1''(pair(z0, z1), z2, z3, z4) -> c34(F_2''(lt(z2, z3), z2, z3, z4, z0, z1), LT'(z2, z3), LT''(z2, z3))
   F_2''(true, z0, z1, z2, z3, z4) -> c35
   F_2''(false, z0, z1, z2, z3, z4) -> c36
   QSORT''(nil) -> c37
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
K tuples:none
Defined Rule Symbols:   LT_2, APPEND_2, SPLIT_2, F_1_4, F_2_6, QSORT_1, F_3_3, lt_2, append_2, split_2, f_1_4, f_2_6, qsort_1, f_3_3

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, F_1'_4, F_2'_6, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, F_1''_4, F_2''_6, QSORT''_1, F_3''_3

Compound Symbols:   c14, c15, c16_1, c17, c18_1, c19, c20_2, c21_2, c22, c23, c24, c25_2, c26_3, c27, c28, c29_1, c30, c31_1, c32, c33_3, c34_3, c35, c36, c37, c38_3, c39_4, c40_4


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

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 14 trailing nodes:
   SPLIT''(z0, nil) -> c32
   F_2''(true, z0, z1, z2, z3, z4) -> c35
   F_2'(false, z0, z1, z2, z3, z4) -> c23
   APPEND''(nil, z0) -> c30
   LT'(s(z0), 0) -> c15
   LT''(0, s(z0)) -> c27
   LT'(0, s(z0)) -> c14
   QSORT'(nil) -> c24
   APPEND'(nil, z0) -> c17
   QSORT''(nil) -> c37
   F_2''(false, z0, z1, z2, z3, z4) -> c36
   SPLIT'(z0, nil) -> c19
   F_2'(true, z0, z1, z2, z3, z4) -> c22
   LT''(s(z0), 0) -> c28

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(F_2'(lt(z2, z3), z2, z3, z4, z0, z1), LT'(z2, z3))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   F_1''(pair(z0, z1), z2, z3, z4) -> c34(F_2''(lt(z2, z3), z2, z3, z4, z0, z1), LT'(z2, z3), LT''(z2, z3))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
S tuples:
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   F_1''(pair(z0, z1), z2, z3, z4) -> c34(F_2''(lt(z2, z3), z2, z3, z4, z0, z1), LT'(z2, z3), LT''(z2, z3))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
K tuples:none
Defined Rule Symbols:   LT_2, APPEND_2, SPLIT_2, F_1_4, F_2_6, QSORT_1, F_3_3, lt_2, append_2, split_2, f_1_4, f_2_6, qsort_1, f_3_3

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, F_1'_4, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, F_1''_4, QSORT''_1, F_3''_3

Compound Symbols:   c16_1, c18_1, c20_2, c21_2, c25_2, c26_3, c29_1, c31_1, c33_3, c34_3, c38_3, c39_4, c40_4


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

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 2 trailing tuple parts
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c34(LT'(z2, z3), LT''(z2, z3))
S tuples:
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c34(LT'(z2, z3), LT''(z2, z3))
K tuples:none
Defined Rule Symbols:   LT_2, APPEND_2, SPLIT_2, F_1_4, F_2_6, QSORT_1, F_3_3, lt_2, append_2, split_2, f_1_4, f_2_6, qsort_1, f_3_3

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c34_2


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

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

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
K tuples:none
Defined Rule Symbols:   LT_2, APPEND_2, SPLIT_2, F_1_4, F_2_6, QSORT_1, F_3_3, lt_2, append_2, split_2, f_1_4, f_2_6, qsort_1, f_3_3

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   LT(0, s(z0)) -> c
   LT(s(z0), 0) -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
K tuples:none
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_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.
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
We considered the (Usable) Rules:
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   split(z0, nil) -> pair(nil, nil)
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
And the Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [1]
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = 0
   POL(F_1'(x_1, x_2, x_3, x_4)) = 0
   POL(F_1''(x_1, x_2, x_3, x_4)) = 0
   POL(F_3'(x_1, x_2, x_3)) = 0
   POL(F_3''(x_1, x_2, x_3)) = [1] + x_1
   POL(LT'(x_1, x_2)) = 0
   POL(LT''(x_1, x_2)) = 0
   POL(QSORT'(x_1)) = 0
   POL(QSORT''(x_1)) = x_1
   POL(SPLIT'(x_1, x_2)) = 0
   POL(SPLIT''(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_2
   POL(append(x_1, x_2)) = [1] + x_1 + x_2
   POL(c14(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c25(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c29(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c33(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c39(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c40(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(f_1(x_1, x_2, x_3, x_4)) = [1] + x_1
   POL(f_2(x_1, x_2, x_3, x_4, x_5, x_6)) = [1] + x_5 + x_6
   POL(f_3(x_1, x_2, x_3)) = [1] + x_2 + x_3
   POL(false) = [1]
   POL(lt(x_1, x_2)) = [1]
   POL(nil) = 0
   POL(pair(x_1, x_2)) = x_1 + x_2
   POL(qsort(x_1)) = x_1
   POL(s(x_1)) = [1] + x_1
   POL(split(x_1, x_2)) = x_2
   POL(true) = [1]

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

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
K tuples:
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))

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

(16)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
K tuples:
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
We considered the (Usable) Rules:
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   split(z0, nil) -> pair(nil, nil)
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
And the Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [2]
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = 0
   POL(F_1'(x_1, x_2, x_3, x_4)) = 0
   POL(F_1''(x_1, x_2, x_3, x_4)) = x_2*x_3
   POL(F_3'(x_1, x_2, x_3)) = 0
   POL(F_3''(x_1, x_2, x_3)) = x_2*x_3 + x_1^2
   POL(LT'(x_1, x_2)) = 0
   POL(LT''(x_1, x_2)) = x_1*x_2
   POL(QSORT'(x_1)) = 0
   POL(QSORT''(x_1)) = x_1^2
   POL(SPLIT'(x_1, x_2)) = 0
   POL(SPLIT''(x_1, x_2)) = x_1*x_2 + x_1^2
   POL(add(x_1, x_2)) = x_1 + x_2
   POL(append(x_1, x_2)) = [2]
   POL(c14(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c25(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c29(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c33(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c39(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c40(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(f_1(x_1, x_2, x_3, x_4)) = x_1 + x_3
   POL(f_2(x_1, x_2, x_3, x_4, x_5, x_6)) = x_3 + x_5 + x_6
   POL(f_3(x_1, x_2, x_3)) = [1] + x_2 + x_3 + x_3^2 + x_2*x_3 + x_2^2
   POL(false) = 0
   POL(lt(x_1, x_2)) = 0
   POL(nil) = 0
   POL(pair(x_1, x_2)) = x_1 + x_2
   POL(qsort(x_1)) = 0
   POL(s(x_1)) = [2] + x_1
   POL(split(x_1, x_2)) = x_2
   POL(true) = 0

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

(18)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
K tuples:
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
We considered the (Usable) Rules:
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   split(z0, nil) -> pair(nil, nil)
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
And the Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [2]
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = 0
   POL(F_1'(x_1, x_2, x_3, x_4)) = 0
   POL(F_1''(x_1, x_2, x_3, x_4)) = [2]
   POL(F_3'(x_1, x_2, x_3)) = 0
   POL(F_3''(x_1, x_2, x_3)) = x_1^2
   POL(LT'(x_1, x_2)) = 0
   POL(LT''(x_1, x_2)) = [1]
   POL(QSORT'(x_1)) = 0
   POL(QSORT''(x_1)) = x_1^2
   POL(SPLIT'(x_1, x_2)) = 0
   POL(SPLIT''(x_1, x_2)) = [2]x_2
   POL(add(x_1, x_2)) = [1] + x_2
   POL(append(x_1, x_2)) = [2]
   POL(c14(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c25(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c29(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c33(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c39(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c40(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(f_1(x_1, x_2, x_3, x_4)) = [1] + x_1
   POL(f_2(x_1, x_2, x_3, x_4, x_5, x_6)) = [1] + x_5 + x_6
   POL(f_3(x_1, x_2, x_3)) = [1] + x_2 + x_3 + x_3^2 + x_2*x_3 + x_2^2
   POL(false) = 0
   POL(lt(x_1, x_2)) = 0
   POL(nil) = 0
   POL(pair(x_1, x_2)) = x_1 + x_2
   POL(qsort(x_1)) = 0
   POL(s(x_1)) = 0
   POL(split(x_1, x_2)) = x_2
   POL(true) = 0

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
K tuples:
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
We considered the (Usable) Rules:
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   split(z0, nil) -> pair(nil, nil)
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
And the Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [2]
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = 0
   POL(F_1'(x_1, x_2, x_3, x_4)) = 0
   POL(F_1''(x_1, x_2, x_3, x_4)) = 0
   POL(F_3'(x_1, x_2, x_3)) = 0
   POL(F_3''(x_1, x_2, x_3)) = x_1^2
   POL(LT'(x_1, x_2)) = 0
   POL(LT''(x_1, x_2)) = 0
   POL(QSORT'(x_1)) = 0
   POL(QSORT''(x_1)) = x_1^2
   POL(SPLIT'(x_1, x_2)) = 0
   POL(SPLIT''(x_1, x_2)) = x_2
   POL(add(x_1, x_2)) = [1] + x_2
   POL(append(x_1, x_2)) = [2]
   POL(c14(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c25(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c29(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c33(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c39(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c40(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(f_1(x_1, x_2, x_3, x_4)) = [1] + x_1
   POL(f_2(x_1, x_2, x_3, x_4, x_5, x_6)) = [1] + x_5 + x_6
   POL(f_3(x_1, x_2, x_3)) = [1] + x_2 + x_3 + x_3^2 + x_2*x_3 + x_2^2
   POL(false) = 0
   POL(lt(x_1, x_2)) = 0
   POL(nil) = 0
   POL(pair(x_1, x_2)) = x_1 + x_2
   POL(qsort(x_1)) = 0
   POL(s(x_1)) = 0
   POL(split(x_1, x_2)) = x_2
   POL(true) = 0

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

(22)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
K tuples:
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
We considered the (Usable) Rules:
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   split(z0, nil) -> pair(nil, nil)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   qsort(nil) -> nil
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   append(nil, z0) -> z0
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
And the Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [2]
   POL(APPEND'(x_1, x_2)) = 0
   POL(APPEND''(x_1, x_2)) = x_1
   POL(F_1'(x_1, x_2, x_3, x_4)) = 0
   POL(F_1''(x_1, x_2, x_3, x_4)) = 0
   POL(F_3'(x_1, x_2, x_3)) = 0
   POL(F_3''(x_1, x_2, x_3)) = [2]x_1 + x_1^2
   POL(LT'(x_1, x_2)) = 0
   POL(LT''(x_1, x_2)) = 0
   POL(QSORT'(x_1)) = 0
   POL(QSORT''(x_1)) = x_1^2
   POL(SPLIT'(x_1, x_2)) = 0
   POL(SPLIT''(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_2
   POL(append(x_1, x_2)) = x_1 + x_2
   POL(c14(x_1)) = x_1
   POL(c16(x_1)) = x_1
   POL(c18(x_1)) = x_1
   POL(c20(x_1, x_2)) = x_1 + x_2
   POL(c21(x_1)) = x_1
   POL(c25(x_1, x_2)) = x_1 + x_2
   POL(c26(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c29(x_1)) = x_1
   POL(c31(x_1)) = x_1
   POL(c33(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c39(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(c40(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4
   POL(f_1(x_1, x_2, x_3, x_4)) = [1] + x_1
   POL(f_2(x_1, x_2, x_3, x_4, x_5, x_6)) = [1] + x_5 + x_6
   POL(f_3(x_1, x_2, x_3)) = [1] + x_1
   POL(false) = 0
   POL(lt(x_1, x_2)) = 0
   POL(nil) = 0
   POL(pair(x_1, x_2)) = x_1 + x_2
   POL(qsort(x_1)) = x_1
   POL(s(x_1)) = 0
   POL(split(x_1, x_2)) = x_2
   POL(true) = 0

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

(24)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   lt(0, s(z0)) -> true
   lt(s(z0), 0) -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
Tuples:
   LT'(s(z0), s(z1)) -> c16(LT'(z0, z1))
   APPEND'(add(z0, z1), z2) -> c18(APPEND'(z1, z2))
   SPLIT'(z0, add(z1, z2)) -> c20(F_1'(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2))
   QSORT'(add(z0, z1)) -> c25(F_3'(split(z0, z1), z0, z1), SPLIT'(z0, z1))
   F_3'(pair(z0, z1), z2, z3) -> c26(APPEND'(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   F_1'(pair(z0, z1), z2, z3, z4) -> c21(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
S tuples:none
K tuples:
   F_3''(pair(z0, z1), z2, z3) -> c39(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z0))
   F_3''(pair(z0, z1), z2, z3) -> c40(APPEND''(qsort(z0), add(z3, qsort(z1))), QSORT'(z0), QSORT'(z1), QSORT''(z1))
   QSORT''(add(z0, z1)) -> c38(F_3''(split(z0, z1), z0, z1), SPLIT'(z0, z1), SPLIT''(z0, z1))
   LT''(s(z0), s(z1)) -> c29(LT''(z0, z1))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT'(z2, z3))
   F_1''(pair(z0, z1), z2, z3, z4) -> c14(LT''(z2, z3))
   SPLIT''(z0, add(z1, z2)) -> c33(F_1''(split(z0, z2), z0, z1, z2), SPLIT'(z0, z2), SPLIT''(z0, z2))
   APPEND''(add(z0, z1), z2) -> c31(APPEND''(z1, z2))
Defined Rule Symbols:   split_2, f_1_4, f_2_6, lt_2, qsort_1, f_3_3, append_2

Defined Pair Symbols:   LT'_2, APPEND'_2, SPLIT'_2, QSORT'_1, F_3'_3, LT''_2, APPEND''_2, SPLIT''_2, QSORT''_1, F_3''_3, F_1'_4, F_1''_4

Compound Symbols:   c16_1, c18_1, c20_2, c25_2, c26_3, c29_1, c31_1, c33_3, c38_3, c39_4, c40_4, c21_1, c14_1


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

(25) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(26)
BOUNDS(1, 1)

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

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

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

   LT(0', s(z0)) -> c
   LT(s(z0), 0') -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(F_2(lt(z2, z3), z2, z3, z4, z0, z1), LT(z2, z3))
   F_2(true, z0, z1, z2, z3, z4) -> c8
   F_2(false, z0, z1, z2, z3, z4) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z2, z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z2, z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))

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

   lt(0', s(z0)) -> true
   lt(s(z0), 0') -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1, z2)
   f_1(pair(z0, z1), z2, z3, z4) -> f_2(lt(z2, z3), z2, z3, z4, z0, z1)
   f_2(true, z0, z1, z2, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z0, z1, z2, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z0, z1)
   f_3(pair(z0, z1), z2, z3) -> append(qsort(z0), add(z3, qsort(z1)))

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

(29) SlicingProof (LOWER BOUND(ID))
Sliced the following arguments:
F_1/3
F_2/1
F_2/2
F_2/3
F_2/4
F_2/5
F_3/1
f_1/3
f_2/1
f_2/3
f_3/1

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

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

   LT(0', s(z0)) -> c
   LT(s(z0), 0') -> c1
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(nil, z0) -> c3
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, nil) -> c5
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3) -> c7(F_2(lt(z2, z3)), LT(z2, z3))
   F_2(true) -> c8
   F_2(false) -> c9
   QSORT(nil) -> c10
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z1), SPLIT(z0, z1))
   F_3(pair(z0, z1), z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
   F_3(pair(z0, z1), z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))

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

   lt(0', s(z0)) -> true
   lt(s(z0), 0') -> false
   lt(s(z0), s(z1)) -> lt(z0, z1)
   append(nil, z0) -> z0
   append(add(z0, z1), z2) -> add(z0, append(z1, z2))
   split(z0, nil) -> pair(nil, nil)
   split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1)
   f_1(pair(z0, z1), z2, z3) -> f_2(lt(z2, z3), z3, z0, z1)
   f_2(true, z1, z3, z4) -> pair(z3, add(z1, z4))
   f_2(false, z1, z3, z4) -> pair(add(z1, z3), z4)
   qsort(nil) -> nil
   qsort(add(z0, z1)) -> f_3(split(z0, z1), z1)
   f_3(pair(z0, z1), z3) -> append(qsort(z0), add(z3, qsort(z1)))

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

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

(32)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(s(z0), 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
APPEND(nil, z0) -> c3
APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
SPLIT(z0, nil) -> c5
SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1), SPLIT(z0, z2))
F_1(pair(z0, z1), z2, z3) -> c7(F_2(lt(z2, z3)), LT(z2, z3))
F_2(true) -> c8
F_2(false) -> c9
QSORT(nil) -> c10
QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z1), SPLIT(z0, z1))
F_3(pair(z0, z1), z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
F_3(pair(z0, z1), z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
lt(0', s(z0)) -> true
lt(s(z0), 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
append(nil, z0) -> z0
append(add(z0, z1), z2) -> add(z0, append(z1, z2))
split(z0, nil) -> pair(nil, nil)
split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1)
f_1(pair(z0, z1), z2, z3) -> f_2(lt(z2, z3), z3, z0, z1)
f_2(true, z1, z3, z4) -> pair(z3, add(z1, z4))
f_2(false, z1, z3, z4) -> pair(add(z1, z3), z4)
qsort(nil) -> nil
qsort(add(z0, z1)) -> f_3(split(z0, z1), z1)
f_3(pair(z0, z1), z3) -> append(qsort(z0), add(z3, qsort(z1)))

Types:
LT :: 0':s:nil:add -> 0':s:nil:add -> c:c1:c2
0' :: 0':s:nil:add
s :: 0':s:nil:add -> 0':s:nil:add
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APPEND :: 0':s:nil:add -> 0':s:nil:add -> c3:c4
nil :: 0':s:nil:add
c3 :: c3:c4
add :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
c4 :: c3:c4 -> c3:c4
SPLIT :: 0':s:nil:add -> 0':s:nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7 -> c5:c6 -> c5:c6
F_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> c7
split :: 0':s:nil:add -> 0':s:nil:add -> pair
pair :: 0':s:nil:add -> 0':s:nil:add -> pair
c7 :: c8:c9 -> c:c1:c2 -> c7
F_2 :: true:false -> c8:c9
lt :: 0':s:nil:add -> 0':s:nil:add -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c8:c9
QSORT :: 0':s:nil:add -> c10:c11
c10 :: c10:c11
c11 :: c12:c13 -> c5:c6 -> c10:c11
F_3 :: pair -> 0':s:nil:add -> c12:c13
c12 :: c3:c4 -> c10:c11 -> c12:c13
qsort :: 0':s:nil:add -> 0':s:nil:add
c13 :: c3:c4 -> c10:c11 -> c12:c13
append :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
f_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 0':s:nil:add
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s:nil:add2_14 :: 0':s:nil:add
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c75_14 :: c7
hole_pair6_14 :: pair
hole_c8:c97_14 :: c8:c9
hole_true:false8_14 :: true:false
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_0':s:nil:add12_14 :: Nat -> 0':s:nil:add
gen_c3:c413_14 :: Nat -> c3:c4
gen_c5:c614_14 :: Nat -> c5:c6

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

(33) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
LT, APPEND, SPLIT, split, lt, QSORT, qsort, append

They will be analysed ascendingly in the following order:
APPEND < QSORT
split < SPLIT
SPLIT < QSORT
split < QSORT
split < qsort
qsort < QSORT
append < qsort

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

(34)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(s(z0), 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
APPEND(nil, z0) -> c3
APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
SPLIT(z0, nil) -> c5
SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1), SPLIT(z0, z2))
F_1(pair(z0, z1), z2, z3) -> c7(F_2(lt(z2, z3)), LT(z2, z3))
F_2(true) -> c8
F_2(false) -> c9
QSORT(nil) -> c10
QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z1), SPLIT(z0, z1))
F_3(pair(z0, z1), z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
F_3(pair(z0, z1), z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
lt(0', s(z0)) -> true
lt(s(z0), 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
append(nil, z0) -> z0
append(add(z0, z1), z2) -> add(z0, append(z1, z2))
split(z0, nil) -> pair(nil, nil)
split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1)
f_1(pair(z0, z1), z2, z3) -> f_2(lt(z2, z3), z3, z0, z1)
f_2(true, z1, z3, z4) -> pair(z3, add(z1, z4))
f_2(false, z1, z3, z4) -> pair(add(z1, z3), z4)
qsort(nil) -> nil
qsort(add(z0, z1)) -> f_3(split(z0, z1), z1)
f_3(pair(z0, z1), z3) -> append(qsort(z0), add(z3, qsort(z1)))

Types:
LT :: 0':s:nil:add -> 0':s:nil:add -> c:c1:c2
0' :: 0':s:nil:add
s :: 0':s:nil:add -> 0':s:nil:add
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APPEND :: 0':s:nil:add -> 0':s:nil:add -> c3:c4
nil :: 0':s:nil:add
c3 :: c3:c4
add :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
c4 :: c3:c4 -> c3:c4
SPLIT :: 0':s:nil:add -> 0':s:nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7 -> c5:c6 -> c5:c6
F_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> c7
split :: 0':s:nil:add -> 0':s:nil:add -> pair
pair :: 0':s:nil:add -> 0':s:nil:add -> pair
c7 :: c8:c9 -> c:c1:c2 -> c7
F_2 :: true:false -> c8:c9
lt :: 0':s:nil:add -> 0':s:nil:add -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c8:c9
QSORT :: 0':s:nil:add -> c10:c11
c10 :: c10:c11
c11 :: c12:c13 -> c5:c6 -> c10:c11
F_3 :: pair -> 0':s:nil:add -> c12:c13
c12 :: c3:c4 -> c10:c11 -> c12:c13
qsort :: 0':s:nil:add -> 0':s:nil:add
c13 :: c3:c4 -> c10:c11 -> c12:c13
append :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
f_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 0':s:nil:add
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s:nil:add2_14 :: 0':s:nil:add
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c75_14 :: c7
hole_pair6_14 :: pair
hole_c8:c97_14 :: c8:c9
hole_true:false8_14 :: true:false
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_0':s:nil:add12_14 :: Nat -> 0':s:nil:add
gen_c3:c413_14 :: Nat -> c3:c4
gen_c5:c614_14 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c211_14(0) <=> c
gen_c:c1:c211_14(+(x, 1)) <=> c2(gen_c:c1:c211_14(x))
gen_0':s:nil:add12_14(0) <=> 0'
gen_0':s:nil:add12_14(+(x, 1)) <=> s(gen_0':s:nil:add12_14(x))
gen_c3:c413_14(0) <=> c3
gen_c3:c413_14(+(x, 1)) <=> c4(gen_c3:c413_14(x))
gen_c5:c614_14(0) <=> c5
gen_c5:c614_14(+(x, 1)) <=> c6(c7(c8, c), gen_c5:c614_14(x))


The following defined symbols remain to be analysed:
LT, APPEND, SPLIT, split, lt, QSORT, qsort, append

They will be analysed ascendingly in the following order:
APPEND < QSORT
split < SPLIT
SPLIT < QSORT
split < QSORT
split < qsort
qsort < QSORT
append < qsort

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

(35) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
LT(gen_0':s:nil:add12_14(n16_14), gen_0':s:nil:add12_14(+(1, n16_14))) -> gen_c:c1:c211_14(n16_14), rt in Omega(1 + n16_14)

Induction Base:
LT(gen_0':s:nil:add12_14(0), gen_0':s:nil:add12_14(+(1, 0))) ->_R^Omega(1)
c

Induction Step:
LT(gen_0':s:nil:add12_14(+(n16_14, 1)), gen_0':s:nil:add12_14(+(1, +(n16_14, 1)))) ->_R^Omega(1)
c2(LT(gen_0':s:nil:add12_14(n16_14), gen_0':s:nil:add12_14(+(1, n16_14)))) ->_IH
c2(gen_c:c1:c211_14(c17_14))

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

(36)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(s(z0), 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
APPEND(nil, z0) -> c3
APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
SPLIT(z0, nil) -> c5
SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1), SPLIT(z0, z2))
F_1(pair(z0, z1), z2, z3) -> c7(F_2(lt(z2, z3)), LT(z2, z3))
F_2(true) -> c8
F_2(false) -> c9
QSORT(nil) -> c10
QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z1), SPLIT(z0, z1))
F_3(pair(z0, z1), z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
F_3(pair(z0, z1), z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
lt(0', s(z0)) -> true
lt(s(z0), 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
append(nil, z0) -> z0
append(add(z0, z1), z2) -> add(z0, append(z1, z2))
split(z0, nil) -> pair(nil, nil)
split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1)
f_1(pair(z0, z1), z2, z3) -> f_2(lt(z2, z3), z3, z0, z1)
f_2(true, z1, z3, z4) -> pair(z3, add(z1, z4))
f_2(false, z1, z3, z4) -> pair(add(z1, z3), z4)
qsort(nil) -> nil
qsort(add(z0, z1)) -> f_3(split(z0, z1), z1)
f_3(pair(z0, z1), z3) -> append(qsort(z0), add(z3, qsort(z1)))

Types:
LT :: 0':s:nil:add -> 0':s:nil:add -> c:c1:c2
0' :: 0':s:nil:add
s :: 0':s:nil:add -> 0':s:nil:add
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APPEND :: 0':s:nil:add -> 0':s:nil:add -> c3:c4
nil :: 0':s:nil:add
c3 :: c3:c4
add :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
c4 :: c3:c4 -> c3:c4
SPLIT :: 0':s:nil:add -> 0':s:nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7 -> c5:c6 -> c5:c6
F_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> c7
split :: 0':s:nil:add -> 0':s:nil:add -> pair
pair :: 0':s:nil:add -> 0':s:nil:add -> pair
c7 :: c8:c9 -> c:c1:c2 -> c7
F_2 :: true:false -> c8:c9
lt :: 0':s:nil:add -> 0':s:nil:add -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c8:c9
QSORT :: 0':s:nil:add -> c10:c11
c10 :: c10:c11
c11 :: c12:c13 -> c5:c6 -> c10:c11
F_3 :: pair -> 0':s:nil:add -> c12:c13
c12 :: c3:c4 -> c10:c11 -> c12:c13
qsort :: 0':s:nil:add -> 0':s:nil:add
c13 :: c3:c4 -> c10:c11 -> c12:c13
append :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
f_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 0':s:nil:add
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s:nil:add2_14 :: 0':s:nil:add
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c75_14 :: c7
hole_pair6_14 :: pair
hole_c8:c97_14 :: c8:c9
hole_true:false8_14 :: true:false
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_0':s:nil:add12_14 :: Nat -> 0':s:nil:add
gen_c3:c413_14 :: Nat -> c3:c4
gen_c5:c614_14 :: Nat -> c5:c6


Generator Equations:
gen_c:c1:c211_14(0) <=> c
gen_c:c1:c211_14(+(x, 1)) <=> c2(gen_c:c1:c211_14(x))
gen_0':s:nil:add12_14(0) <=> 0'
gen_0':s:nil:add12_14(+(x, 1)) <=> s(gen_0':s:nil:add12_14(x))
gen_c3:c413_14(0) <=> c3
gen_c3:c413_14(+(x, 1)) <=> c4(gen_c3:c413_14(x))
gen_c5:c614_14(0) <=> c5
gen_c5:c614_14(+(x, 1)) <=> c6(c7(c8, c), gen_c5:c614_14(x))


The following defined symbols remain to be analysed:
LT, APPEND, SPLIT, split, lt, QSORT, qsort, append

They will be analysed ascendingly in the following order:
APPEND < QSORT
split < SPLIT
SPLIT < QSORT
split < QSORT
split < qsort
qsort < QSORT
append < qsort

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

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

(39)
BOUNDS(n^1, INF)

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

(40)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(s(z0), 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
APPEND(nil, z0) -> c3
APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
SPLIT(z0, nil) -> c5
SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1), SPLIT(z0, z2))
F_1(pair(z0, z1), z2, z3) -> c7(F_2(lt(z2, z3)), LT(z2, z3))
F_2(true) -> c8
F_2(false) -> c9
QSORT(nil) -> c10
QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z1), SPLIT(z0, z1))
F_3(pair(z0, z1), z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
F_3(pair(z0, z1), z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
lt(0', s(z0)) -> true
lt(s(z0), 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
append(nil, z0) -> z0
append(add(z0, z1), z2) -> add(z0, append(z1, z2))
split(z0, nil) -> pair(nil, nil)
split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1)
f_1(pair(z0, z1), z2, z3) -> f_2(lt(z2, z3), z3, z0, z1)
f_2(true, z1, z3, z4) -> pair(z3, add(z1, z4))
f_2(false, z1, z3, z4) -> pair(add(z1, z3), z4)
qsort(nil) -> nil
qsort(add(z0, z1)) -> f_3(split(z0, z1), z1)
f_3(pair(z0, z1), z3) -> append(qsort(z0), add(z3, qsort(z1)))

Types:
LT :: 0':s:nil:add -> 0':s:nil:add -> c:c1:c2
0' :: 0':s:nil:add
s :: 0':s:nil:add -> 0':s:nil:add
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APPEND :: 0':s:nil:add -> 0':s:nil:add -> c3:c4
nil :: 0':s:nil:add
c3 :: c3:c4
add :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
c4 :: c3:c4 -> c3:c4
SPLIT :: 0':s:nil:add -> 0':s:nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7 -> c5:c6 -> c5:c6
F_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> c7
split :: 0':s:nil:add -> 0':s:nil:add -> pair
pair :: 0':s:nil:add -> 0':s:nil:add -> pair
c7 :: c8:c9 -> c:c1:c2 -> c7
F_2 :: true:false -> c8:c9
lt :: 0':s:nil:add -> 0':s:nil:add -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c8:c9
QSORT :: 0':s:nil:add -> c10:c11
c10 :: c10:c11
c11 :: c12:c13 -> c5:c6 -> c10:c11
F_3 :: pair -> 0':s:nil:add -> c12:c13
c12 :: c3:c4 -> c10:c11 -> c12:c13
qsort :: 0':s:nil:add -> 0':s:nil:add
c13 :: c3:c4 -> c10:c11 -> c12:c13
append :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
f_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 0':s:nil:add
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s:nil:add2_14 :: 0':s:nil:add
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c75_14 :: c7
hole_pair6_14 :: pair
hole_c8:c97_14 :: c8:c9
hole_true:false8_14 :: true:false
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_0':s:nil:add12_14 :: Nat -> 0':s:nil:add
gen_c3:c413_14 :: Nat -> c3:c4
gen_c5:c614_14 :: Nat -> c5:c6


Lemmas:
LT(gen_0':s:nil:add12_14(n16_14), gen_0':s:nil:add12_14(+(1, n16_14))) -> gen_c:c1:c211_14(n16_14), rt in Omega(1 + n16_14)


Generator Equations:
gen_c:c1:c211_14(0) <=> c
gen_c:c1:c211_14(+(x, 1)) <=> c2(gen_c:c1:c211_14(x))
gen_0':s:nil:add12_14(0) <=> 0'
gen_0':s:nil:add12_14(+(x, 1)) <=> s(gen_0':s:nil:add12_14(x))
gen_c3:c413_14(0) <=> c3
gen_c3:c413_14(+(x, 1)) <=> c4(gen_c3:c413_14(x))
gen_c5:c614_14(0) <=> c5
gen_c5:c614_14(+(x, 1)) <=> c6(c7(c8, c), gen_c5:c614_14(x))


The following defined symbols remain to be analysed:
APPEND, SPLIT, split, lt, QSORT, qsort, append

They will be analysed ascendingly in the following order:
APPEND < QSORT
split < SPLIT
SPLIT < QSORT
split < QSORT
split < qsort
qsort < QSORT
append < qsort

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

(41) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
lt(gen_0':s:nil:add12_14(n681_14), gen_0':s:nil:add12_14(+(1, n681_14))) -> true, rt in Omega(0)

Induction Base:
lt(gen_0':s:nil:add12_14(0), gen_0':s:nil:add12_14(+(1, 0))) ->_R^Omega(0)
true

Induction Step:
lt(gen_0':s:nil:add12_14(+(n681_14, 1)), gen_0':s:nil:add12_14(+(1, +(n681_14, 1)))) ->_R^Omega(0)
lt(gen_0':s:nil:add12_14(n681_14), gen_0':s:nil:add12_14(+(1, n681_14))) ->_IH
true

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

(42)
Obligation:
Innermost TRS:
Rules:
LT(0', s(z0)) -> c
LT(s(z0), 0') -> c1
LT(s(z0), s(z1)) -> c2(LT(z0, z1))
APPEND(nil, z0) -> c3
APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
SPLIT(z0, nil) -> c5
SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1), SPLIT(z0, z2))
F_1(pair(z0, z1), z2, z3) -> c7(F_2(lt(z2, z3)), LT(z2, z3))
F_2(true) -> c8
F_2(false) -> c9
QSORT(nil) -> c10
QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z1), SPLIT(z0, z1))
F_3(pair(z0, z1), z3) -> c12(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z0))
F_3(pair(z0, z1), z3) -> c13(APPEND(qsort(z0), add(z3, qsort(z1))), QSORT(z1))
lt(0', s(z0)) -> true
lt(s(z0), 0') -> false
lt(s(z0), s(z1)) -> lt(z0, z1)
append(nil, z0) -> z0
append(add(z0, z1), z2) -> add(z0, append(z1, z2))
split(z0, nil) -> pair(nil, nil)
split(z0, add(z1, z2)) -> f_1(split(z0, z2), z0, z1)
f_1(pair(z0, z1), z2, z3) -> f_2(lt(z2, z3), z3, z0, z1)
f_2(true, z1, z3, z4) -> pair(z3, add(z1, z4))
f_2(false, z1, z3, z4) -> pair(add(z1, z3), z4)
qsort(nil) -> nil
qsort(add(z0, z1)) -> f_3(split(z0, z1), z1)
f_3(pair(z0, z1), z3) -> append(qsort(z0), add(z3, qsort(z1)))

Types:
LT :: 0':s:nil:add -> 0':s:nil:add -> c:c1:c2
0' :: 0':s:nil:add
s :: 0':s:nil:add -> 0':s:nil:add
c :: c:c1:c2
c1 :: c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
APPEND :: 0':s:nil:add -> 0':s:nil:add -> c3:c4
nil :: 0':s:nil:add
c3 :: c3:c4
add :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
c4 :: c3:c4 -> c3:c4
SPLIT :: 0':s:nil:add -> 0':s:nil:add -> c5:c6
c5 :: c5:c6
c6 :: c7 -> c5:c6 -> c5:c6
F_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> c7
split :: 0':s:nil:add -> 0':s:nil:add -> pair
pair :: 0':s:nil:add -> 0':s:nil:add -> pair
c7 :: c8:c9 -> c:c1:c2 -> c7
F_2 :: true:false -> c8:c9
lt :: 0':s:nil:add -> 0':s:nil:add -> true:false
true :: true:false
c8 :: c8:c9
false :: true:false
c9 :: c8:c9
QSORT :: 0':s:nil:add -> c10:c11
c10 :: c10:c11
c11 :: c12:c13 -> c5:c6 -> c10:c11
F_3 :: pair -> 0':s:nil:add -> c12:c13
c12 :: c3:c4 -> c10:c11 -> c12:c13
qsort :: 0':s:nil:add -> 0':s:nil:add
c13 :: c3:c4 -> c10:c11 -> c12:c13
append :: 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add
f_1 :: pair -> 0':s:nil:add -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 0':s:nil:add
hole_c:c1:c21_14 :: c:c1:c2
hole_0':s:nil:add2_14 :: 0':s:nil:add
hole_c3:c43_14 :: c3:c4
hole_c5:c64_14 :: c5:c6
hole_c75_14 :: c7
hole_pair6_14 :: pair
hole_c8:c97_14 :: c8:c9
hole_true:false8_14 :: true:false
hole_c10:c119_14 :: c10:c11
hole_c12:c1310_14 :: c12:c13
gen_c:c1:c211_14 :: Nat -> c:c1:c2
gen_0':s:nil:add12_14 :: Nat -> 0':s:nil:add
gen_c3:c413_14 :: Nat -> c3:c4
gen_c5:c614_14 :: Nat -> c5:c6


Lemmas:
LT(gen_0':s:nil:add12_14(n16_14), gen_0':s:nil:add12_14(+(1, n16_14))) -> gen_c:c1:c211_14(n16_14), rt in Omega(1 + n16_14)
lt(gen_0':s:nil:add12_14(n681_14), gen_0':s:nil:add12_14(+(1, n681_14))) -> true, rt in Omega(0)


Generator Equations:
gen_c:c1:c211_14(0) <=> c
gen_c:c1:c211_14(+(x, 1)) <=> c2(gen_c:c1:c211_14(x))
gen_0':s:nil:add12_14(0) <=> 0'
gen_0':s:nil:add12_14(+(x, 1)) <=> s(gen_0':s:nil:add12_14(x))
gen_c3:c413_14(0) <=> c3
gen_c3:c413_14(+(x, 1)) <=> c4(gen_c3:c413_14(x))
gen_c5:c614_14(0) <=> c5
gen_c5:c614_14(+(x, 1)) <=> c6(c7(c8, c), gen_c5:c614_14(x))


The following defined symbols remain to be analysed:
append, QSORT, qsort

They will be analysed ascendingly in the following order:
qsort < QSORT
append < qsort