WORST_CASE(Omega(n^1),O(n^1)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 357 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 76 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 30 ms] (12) CdtProblem (13) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (14) BOUNDS(1, 1) (15) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (16) TRS for Loop Detection (17) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (18) BEST (19) proven lower bound (20) LowerBoundPropagationProof [FINISHED, 0 ms] (21) BOUNDS(n^1, INF) (22) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) The (relative) TRS S consists of the following rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) The (relative) TRS S consists of the following rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) Tuples: QSORT'(nil) -> c9 QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, nil) -> c11 LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, nil) -> c13 GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(nil) -> c15 QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, nil) -> c18 LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, nil) -> c21 GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) S tuples: QSORT''(nil) -> c15 QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, nil) -> c18 LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, nil) -> c21 GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) K tuples:none Defined Rule Symbols: QSORT_1, LOWERS_2, GREATERS_2, qsort_1, lowers_2, greaters_2 Defined Pair Symbols: QSORT'_1, LOWERS'_2, GREATERS'_2, QSORT''_1, LOWERS''_2, GREATERS''_2 Compound Symbols: c9, c10_4, c11, c12_2, c13, c14_2, c15, c16_3, c17_3, c18, c19_1, c20_1, c21, c22_1, c23_1 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 6 trailing nodes: GREATERS''(z0, nil) -> c21 LOWERS''(z0, nil) -> c18 LOWERS'(z0, nil) -> c11 QSORT'(nil) -> c9 QSORT''(nil) -> c15 GREATERS'(z0, nil) -> c13 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) Tuples: QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) S tuples: QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) K tuples:none Defined Rule Symbols: QSORT_1, LOWERS_2, GREATERS_2, qsort_1, lowers_2, greaters_2 Defined Pair Symbols: QSORT'_1, LOWERS'_2, GREATERS'_2, QSORT''_1, LOWERS''_2, GREATERS''_2 Compound Symbols: c10_4, c12_2, c14_2, c16_3, c17_3, c19_1, c20_1, c22_1, c23_1 ---------------------------------------- (7) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Tuples: QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) S tuples: QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) K tuples:none Defined Rule Symbols: lowers_2, greaters_2 Defined Pair Symbols: QSORT'_1, LOWERS'_2, GREATERS'_2, QSORT''_1, LOWERS''_2, GREATERS''_2 Compound Symbols: c10_4, c12_2, c14_2, c16_3, c17_3, c19_1, c20_1, c22_1, c23_1 ---------------------------------------- (9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) We considered the (Usable) Rules: greaters(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) lowers(z0, nil) -> nil And the Tuples: QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(.(x_1, x_2)) = [1] + x_1 POL(<=(x_1, x_2)) = x_2 POL(GREATERS'(x_1, x_2)) = 0 POL(GREATERS''(x_1, x_2)) = 0 POL(LOWERS'(x_1, x_2)) = 0 POL(LOWERS''(x_1, x_2)) = 0 POL(QSORT'(x_1)) = 0 POL(QSORT''(x_1)) = x_1 POL(c10(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c14(x_1, x_2)) = x_1 + x_2 POL(c16(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c17(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(greaters(x_1, x_2)) = x_1 POL(if(x_1, x_2, x_3)) = x_1 POL(lowers(x_1, x_2)) = x_1 POL(nil) = 0 ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Tuples: QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) S tuples: LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) K tuples: QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) Defined Rule Symbols: lowers_2, greaters_2 Defined Pair Symbols: QSORT'_1, LOWERS'_2, GREATERS'_2, QSORT''_1, LOWERS''_2, GREATERS''_2 Compound Symbols: c10_4, c12_2, c14_2, c16_3, c17_3, c19_1, c20_1, c22_1, c23_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) We considered the (Usable) Rules: greaters(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) lowers(z0, nil) -> nil And the Tuples: QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) The order we found is given by the following interpretation: Polynomial interpretation : POL(.(x_1, x_2)) = [1] + x_1 + x_2 POL(<=(x_1, x_2)) = x_2 POL(GREATERS'(x_1, x_2)) = 0 POL(GREATERS''(x_1, x_2)) = [1] + x_2 POL(LOWERS'(x_1, x_2)) = 0 POL(LOWERS''(x_1, x_2)) = [1] + x_2 POL(QSORT'(x_1)) = 0 POL(QSORT''(x_1)) = x_1 POL(c10(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c14(x_1, x_2)) = x_1 + x_2 POL(c16(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c17(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c19(x_1)) = x_1 POL(c20(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c23(x_1)) = x_1 POL(greaters(x_1, x_2)) = x_1 POL(if(x_1, x_2, x_3)) = x_1 POL(lowers(x_1, x_2)) = x_1 POL(nil) = 0 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Tuples: QSORT'(.(z0, z1)) -> c10(QSORT'(lowers(z0, z1)), LOWERS'(z0, z1), QSORT'(greaters(z0, z1)), GREATERS'(z0, z1)) LOWERS'(z0, .(z1, z2)) -> c12(LOWERS'(z0, z2), LOWERS'(z0, z2)) GREATERS'(z0, .(z1, z2)) -> c14(GREATERS'(z0, z2), GREATERS'(z0, z2)) QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) S tuples:none K tuples: QSORT''(.(z0, z1)) -> c16(QSORT''(lowers(z0, z1)), LOWERS'(z0, z1), LOWERS''(z0, z1)) QSORT''(.(z0, z1)) -> c17(QSORT''(greaters(z0, z1)), GREATERS'(z0, z1), GREATERS''(z0, z1)) LOWERS''(z0, .(z1, z2)) -> c19(LOWERS''(z0, z2)) LOWERS''(z0, .(z1, z2)) -> c20(LOWERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c22(GREATERS''(z0, z2)) GREATERS''(z0, .(z1, z2)) -> c23(GREATERS''(z0, z2)) Defined Rule Symbols: lowers_2, greaters_2 Defined Pair Symbols: QSORT'_1, LOWERS'_2, GREATERS'_2, QSORT''_1, LOWERS''_2, GREATERS''_2 Compound Symbols: c10_4, c12_2, c14_2, c16_3, c17_3, c19_1, c20_1, c22_1, c23_1 ---------------------------------------- (13) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (14) BOUNDS(1, 1) ---------------------------------------- (15) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (16) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) The (relative) TRS S consists of the following rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Rewrite Strategy: INNERMOST ---------------------------------------- (17) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence GREATERS(z0, .(z1, z2)) ->^+ c7(GREATERS(z0, z2)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z2 / .(z1, z2)]. The result substitution is [ ]. ---------------------------------------- (18) Complex Obligation (BEST) ---------------------------------------- (19) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) The (relative) TRS S consists of the following rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Rewrite Strategy: INNERMOST ---------------------------------------- (20) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (21) BOUNDS(n^1, INF) ---------------------------------------- (22) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: QSORT(nil) -> c QSORT(.(z0, z1)) -> c1(QSORT(lowers(z0, z1)), LOWERS(z0, z1)) QSORT(.(z0, z1)) -> c2(QSORT(greaters(z0, z1)), GREATERS(z0, z1)) LOWERS(z0, nil) -> c3 LOWERS(z0, .(z1, z2)) -> c4(LOWERS(z0, z2)) LOWERS(z0, .(z1, z2)) -> c5(LOWERS(z0, z2)) GREATERS(z0, nil) -> c6 GREATERS(z0, .(z1, z2)) -> c7(GREATERS(z0, z2)) GREATERS(z0, .(z1, z2)) -> c8(GREATERS(z0, z2)) The (relative) TRS S consists of the following rules: qsort(nil) -> nil qsort(.(z0, z1)) -> ++(qsort(lowers(z0, z1)), .(z0, qsort(greaters(z0, z1)))) lowers(z0, nil) -> nil lowers(z0, .(z1, z2)) -> if(<=(z1, z0), .(z1, lowers(z0, z2)), lowers(z0, z2)) greaters(z0, nil) -> nil greaters(z0, .(z1, z2)) -> if(<=(z1, z0), greaters(z0, z2), .(z1, greaters(z0, z2))) Rewrite Strategy: INNERMOST