WORST_CASE(Omega(n^1),O(n^2))
proof of input_mu3Z94uzu6.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
    (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
    (4) CdtProblem
    (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (6) CdtProblem
    (7) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 199 ms]
    (8) CdtProblem
    (9) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 1478 ms]
    (12) CdtProblem
    (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 710 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 686 ms]
    (16) CdtProblem
    (17) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (18) BOUNDS(1, 1)
(19) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CdtProblem
    (21) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) CpxRelTRS
    (23) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (24) CpxRelTRS
    (25) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (26) typed CpxTrs
    (27) OrderProof [LOWER BOUND(ID), 0 ms]
    (28) typed CpxTrs
    (29) RewriteLemmaProof [LOWER BOUND(ID), 372 ms]
    (30) BEST
        (31) proven lower bound
            (32) LowerBoundPropagationProof [FINISHED, 0 ms]
            (33) BOUNDS(n^1, INF)
        (34) typed CpxTrs
            (35) RewriteLemmaProof [LOWER BOUND(ID), 113 ms]
            (36) typed CpxTrs


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

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


The TRS R consists of the following rules:

   lt(0, s(X)) -> true
   lt(s(X), 0) -> false
   lt(s(X), s(Y)) -> lt(X, Y)
   append(nil, Y) -> Y
   append(add(N, X), Y) -> add(N, append(X, Y))
   split(N, nil) -> pair(nil, nil)
   split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
   f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
   f_2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
   f_2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
   qsort(nil) -> nil
   qsort(add(N, X)) -> f_3(split(N, X), N, X)
   f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

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

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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)))
Tuples:
   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))
S tuples:
   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))
K tuples:none
Defined Rule Symbols:   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

Compound Symbols:   c, c1, c2_1, c3, c4_1, c5, c6_2, c7_2, c8, c9, c10, c11_2, c12_2, c13_2


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

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 7 trailing nodes:
   F_2(false, z0, z1, z2, z3, z4) -> c9
   LT(s(z0), 0) -> c1
   QSORT(nil) -> c10
   F_2(true, z0, z1, z2, z3, z4) -> c8
   APPEND(nil, z0) -> c3
   LT(0, s(z0)) -> c
   SPLIT(z0, nil) -> c5

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

(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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   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))
   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))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   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))
   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))
K tuples:none
Defined Rule Symbols:   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

Compound Symbols:   c2_1, c4_1, c6_2, c7_2, c11_2, c12_2, c13_2


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

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 1 trailing tuple parts
----------------------------------------

(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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(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

Defined Pair Symbols:   LT_2, APPEND_2, SPLIT_2, QSORT_1, F_3_3, F_1_4

Compound Symbols:   c2_1, c4_1, c6_2, c11_2, c12_2, c13_2, c7_1


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

(7) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(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)
   lt(s(z0), 0) -> false
   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)
   lt(0, s(z0)) -> true
   lt(s(z0), s(z1)) -> lt(z0, z1)
And the Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(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(F_1(x_1, x_2, x_3, x_4)) = 0
   POL(F_3(x_1, x_2, x_3)) = x_1
   POL(LT(x_1, x_2)) = 0
   POL(QSORT(x_1)) = x_1
   POL(SPLIT(x_1, x_2)) = 0
   POL(add(x_1, x_2)) = [1] + x_2
   POL(append(x_1, x_2)) = [1] + x_2
   POL(c11(x_1, x_2)) = x_1 + x_2
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c13(x_1, x_2)) = x_1 + x_2
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   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)) = x_1 + x_5 + x_6
   POL(f_3(x_1, x_2, x_3)) = [1] + x_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)) = [1] + x_1
   POL(s(x_1)) = [1] + x_1
   POL(split(x_1, x_2)) = x_2
   POL(true) = [1]

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

(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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
K tuples:
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
Defined Rule Symbols:   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, F_1_4

Compound Symbols:   c2_1, c4_1, c6_2, c11_2, c12_2, c13_2, c7_1


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

(9) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   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))
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))
   QSORT(add(z0, z1)) -> c11(F_3(split(z0, z1), z0, z1), SPLIT(z0, z1))

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

(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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   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(LT(z2, z3))
K tuples:
   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))
Defined Rule Symbols:   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, F_1_4

Compound Symbols:   c2_1, c4_1, c6_2, c11_2, c12_2, c13_2, c7_1


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

(11) 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)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(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)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(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(F_1(x_1, x_2, x_3, x_4)) = [1]
   POL(F_3(x_1, x_2, x_3)) = [2]x_3 + [2]x_1^2
   POL(LT(x_1, x_2)) = 0
   POL(QSORT(x_1)) = [2]x_1^2
   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] + x_2^2 + x_1*x_2 + x_1^2
   POL(c11(x_1, x_2)) = x_1 + x_2
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c13(x_1, x_2)) = x_1 + x_2
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   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

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

(12)
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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
S tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
K tuples:
   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))
   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(LT(z2, z3))
Defined Rule Symbols:   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, F_1_4

Compound Symbols:   c2_1, c4_1, c6_2, c11_2, c12_2, c13_2, c7_1


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

(13) 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)) -> c2(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)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(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(F_1(x_1, x_2, x_3, x_4)) = [2]x_2*x_3
   POL(F_3(x_1, x_2, x_3)) = x_1^2
   POL(LT(x_1, x_2)) = [2]x_1*x_2
   POL(QSORT(x_1)) = x_1^2
   POL(SPLIT(x_1, x_2)) = [2]x_1*x_2
   POL(add(x_1, x_2)) = x_1 + x_2
   POL(append(x_1, x_2)) = [2] + x_2^2 + x_1*x_2 + x_1^2
   POL(c11(x_1, x_2)) = x_1 + x_2
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c13(x_1, x_2)) = x_1 + x_2
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   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

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

(14)
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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
S tuples:
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
K tuples:
   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))
   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(LT(z2, z3))
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
Defined Rule Symbols:   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, F_1_4

Compound Symbols:   c2_1, c4_1, c6_2, c11_2, c12_2, c13_2, c7_1


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

(15) 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) -> c4(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)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(0) = [2]
   POL(APPEND(x_1, x_2)) = x_1
   POL(F_1(x_1, x_2, x_3, x_4)) = 0
   POL(F_3(x_1, x_2, x_3)) = [2]x_1 + x_1^2
   POL(LT(x_1, x_2)) = 0
   POL(QSORT(x_1)) = x_1^2
   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(c11(x_1, x_2)) = x_1 + x_2
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c13(x_1, x_2)) = x_1 + x_2
   POL(c2(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1, x_2)) = x_1 + x_2
   POL(c7(x_1)) = x_1
   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] + [2]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)) = [2]x_1
   POL(s(x_1)) = 0
   POL(split(x_1, x_2)) = x_2
   POL(true) = 0

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

(16)
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)))
Tuples:
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
   SPLIT(z0, add(z1, z2)) -> c6(F_1(split(z0, z2), z0, z1, z2), SPLIT(z0, z2))
   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))
   F_1(pair(z0, z1), z2, z3, z4) -> c7(LT(z2, z3))
S tuples:none
K tuples:
   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))
   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(LT(z2, z3))
   LT(s(z0), s(z1)) -> c2(LT(z0, z1))
   APPEND(add(z0, z1), z2) -> c4(APPEND(z1, z2))
Defined Rule Symbols:   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, F_1_4

Compound Symbols:   c2_1, c4_1, c6_2, c11_2, c12_2, c13_2, c7_1


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

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

(18)
BOUNDS(1, 1)

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

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

(20)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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)))
Tuples:
   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))
S tuples:
   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))
K tuples:none
Defined Rule Symbols:   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

Compound Symbols:   c, c1, c2_1, c3, c4_1, c5, c6_2, c7_2, c8, c9, c10, c11_2, c12_2, c13_2


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

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

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


The TRS R consists of the following rules:

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

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

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


The TRS R consists of the following rules:

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

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

(26)
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, 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))
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)))

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 -> 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 -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 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 -> 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 -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 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

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

(27) 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

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

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

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 -> 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 -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 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 -> 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 -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 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

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

(29) 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).
----------------------------------------

(30)
Complex Obligation (BEST)

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

(31)
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, 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))
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)))

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 -> 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 -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 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 -> 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 -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 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

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

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

(33)
BOUNDS(n^1, INF)

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

(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, 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))
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)))

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 -> 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 -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 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 -> 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 -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 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

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

(35) 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).
----------------------------------------

(36)
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, 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))
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)))

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 -> 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 -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 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 -> 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 -> 0':s:nil:add -> pair
f_2 :: true:false -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> 0':s:nil:add -> pair
f_3 :: pair -> 0':s:nil:add -> 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