WORST_CASE(Omega(n^1),?) proof of input_rn5anCT3ty.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 193 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 36 ms] (4) CdtProblem (5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxRelTRS (7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (10) typed CpxTrs (11) OrderProof [LOWER BOUND(ID), 32 ms] (12) typed CpxTrs (13) RewriteLemmaProof [LOWER BOUND(ID), 313 ms] (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 138 ms] (16) typed CpxTrs (17) RewriteLemmaProof [LOWER BOUND(ID), 1189 ms] (18) BEST (19) proven lower bound (20) LowerBoundPropagationProof [FINISHED, 0 ms] (21) BOUNDS(n^1, INF) (22) typed CpxTrs (23) RewriteLemmaProof [LOWER BOUND(ID), 0 ms] (24) typed CpxTrs (25) RewriteLemmaProof [LOWER BOUND(ID), 118 ms] (26) typed CpxTrs (27) RewriteLemmaProof [LOWER BOUND(ID), 945 ms] (28) typed CpxTrs (29) RewriteLemmaProof [LOWER BOUND(ID), 52 ms] (30) typed CpxTrs (31) RewriteLemmaProof [LOWER BOUND(ID), 63 ms] (32) typed CpxTrs (33) RewriteLemmaProof [LOWER BOUND(ID), 67 ms] (34) typed CpxTrs (35) RewriteLemmaProof [LOWER BOUND(ID), 54 ms] (36) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: quicksort(Cons(x, Cons(x', xs))) -> part(x, Cons(x', xs)) quicksort(Cons(x, Nil)) -> Cons(x, Nil) quicksort(Nil) -> Nil partLt(x', Cons(x, xs)) -> partLt[Ite][True][Ite](<(x, x'), x', Cons(x, xs)) partLt(x, Nil) -> Nil partGt(x', Cons(x, xs)) -> partGt[Ite][True][Ite](>(x, x'), x', Cons(x, xs)) partGt(x, Nil) -> Nil app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) app(Nil, ys) -> ys notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False part(x, xs) -> app(quicksort(partLt(x, xs)), Cons(x, quicksort(partGt(x, xs)))) goal(xs) -> quicksort(xs) The (relative) TRS S consists of the following rules: <(S(x), S(y)) -> <(x, y) <(0, S(y)) -> True <(x, 0) -> False >(S(x), S(y)) -> >(x, y) >(0, y) -> False >(S(x), 0) -> True partLt[Ite][True][Ite](True, x', Cons(x, xs)) -> Cons(x, partLt(x', xs)) partGt[Ite][True][Ite](True, x', Cons(x, xs)) -> Cons(x, partGt(x', xs)) partLt[Ite][True][Ite](False, x', Cons(x, xs)) -> partLt(x', xs) partGt[Ite][True][Ite](False, x', Cons(x, xs)) -> partGt(x', xs) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: quicksort(Cons(x, Cons(x', xs))) -> part(x, Cons(x', xs)) quicksort(Cons(x, Nil)) -> Cons(x, Nil) quicksort(Nil) -> Nil partLt(x', Cons(x, xs)) -> partLt[Ite][True][Ite](<(x, x'), x', Cons(x, xs)) partLt(x, Nil) -> Nil partGt(x', Cons(x, xs)) -> partGt[Ite][True][Ite](>(x, x'), x', Cons(x, xs)) partGt(x, Nil) -> Nil app(Cons(x, xs), ys) -> Cons(x, app(xs, ys)) app(Nil, ys) -> ys notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False part(x, xs) -> app(quicksort(partLt(x, xs)), Cons(x, quicksort(partGt(x, xs)))) goal(xs) -> quicksort(xs) The (relative) TRS S consists of the following rules: <(S(x), S(y)) -> <(x, y) <(0, S(y)) -> True <(x, 0) -> False >(S(x), S(y)) -> >(x, y) >(0, y) -> False >(S(x), 0) -> True partLt[Ite][True][Ite](True, x', Cons(x, xs)) -> Cons(x, partLt(x', xs)) partGt[Ite][True][Ite](True, x', Cons(x, xs)) -> Cons(x, partGt(x', xs)) partLt[Ite][True][Ite](False, x', Cons(x, xs)) -> partLt(x', xs) partGt[Ite][True][Ite](False, x', Cons(x, xs)) -> partGt(x', xs) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: <(S(z0), S(z1)) -> <(z0, z1) <(0, S(z0)) -> True <(z0, 0) -> False >(S(z0), S(z1)) -> >(z0, z1) >(0, z0) -> False >(S(z0), 0) -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Tuples: <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0, S(z0)) -> c1 <'(z0, 0) -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0, z0) -> c4 >'(S(z0), 0) -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) S tuples: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) K tuples:none Defined Rule Symbols: quicksort_1, partLt_2, partGt_2, app_2, notEmpty_1, part_2, goal_1, <_2, >_2, partLt[Ite][True][Ite]_3, partGt[Ite][True][Ite]_3 Defined Pair Symbols: <'_2, >'_2, PARTLT[ITE][TRUE][ITE]_3, PARTGT[ITE][TRUE][ITE]_3, QUICKSORT_1, PARTLT_2, PARTGT_2, APP_2, NOTEMPTY_1, PART_2, GOAL_1 Compound Symbols: c_1, c1, c2, c3_1, c4, c5, c6_1, c7_1, c8_1, c9_1, c10_1, c11, c12, c13_2, c14, c15_2, c16, c17_1, c18, c19, c20, c21_3, c22_3, c23_1 ---------------------------------------- (5) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (6) 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: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) The (relative) TRS S consists of the following rules: <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0, S(z0)) -> c1 <'(z0, 0) -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0, z0) -> c4 >'(S(z0), 0) -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0, S(z0)) -> True <(z0, 0) -> False >(S(z0), S(z1)) -> >(z0, z1) >(0, z0) -> False >(S(z0), 0) -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Rewrite Strategy: INNERMOST ---------------------------------------- (7) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (8) 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: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) The (relative) TRS S consists of the following rules: <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Rewrite Strategy: INNERMOST ---------------------------------------- (9) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (10) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 ---------------------------------------- (11) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: QUICKSORT, PARTLT, <, <', PARTGT, >, >', APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTLT < QUICKSORT PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT < < PARTLT <' < PARTLT < < partLt > < PARTGT >' < PARTGT > < partGt partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (12) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: <, QUICKSORT, PARTLT, <', PARTGT, >, >', APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTLT < QUICKSORT PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT < < PARTLT <' < PARTLT < < partLt > < PARTGT >' < PARTGT > < partGt partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (13) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) Induction Base: <(gen_S:0'16_24(0), gen_S:0'16_24(+(1, 0))) ->_R^Omega(0) True Induction Step: <(gen_S:0'16_24(+(n21_24, 1)), gen_S:0'16_24(+(1, +(n21_24, 1)))) ->_R^Omega(0) <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) ->_IH True We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (14) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: <', QUICKSORT, PARTLT, PARTGT, >, >', APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTLT < QUICKSORT PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT <' < PARTLT > < PARTGT >' < PARTGT > < partGt partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (15) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) Induction Base: <'(gen_S:0'16_24(0), gen_S:0'16_24(+(1, 0))) ->_R^Omega(0) c1 Induction Step: <'(gen_S:0'16_24(+(n463_24, 1)), gen_S:0'16_24(+(1, +(n463_24, 1)))) ->_R^Omega(0) c(<'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24)))) ->_IH c(gen_c:c1:c217_24(c464_24)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (16) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: PARTLT, QUICKSORT, PARTGT, >, >', APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTLT < QUICKSORT PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT > < PARTGT >' < PARTGT > < partGt partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (17) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) Induction Base: PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, 0))) Induction Step: PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, +(n1240_24, 1)))) ->_R^Omega(1) c13(PARTLT[ITE][TRUE][ITE](<(0', gen_S:0'16_24(1)), gen_S:0'16_24(1), Cons(0', gen_Cons:Nil15_24(+(1, n1240_24)))), <'(0', gen_S:0'16_24(1))) ->_L^Omega(0) c13(PARTLT[ITE][TRUE][ITE](True, gen_S:0'16_24(1), Cons(0', gen_Cons:Nil15_24(+(1, n1240_24)))), <'(0', gen_S:0'16_24(1))) ->_R^Omega(0) c13(c6(PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24)))), <'(0', gen_S:0'16_24(1))) ->_IH c13(c6(*20_24), <'(0', gen_S:0'16_24(1))) ->_L^Omega(0) c13(c6(*20_24), gen_c:c1:c217_24(0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (18) Complex Obligation (BEST) ---------------------------------------- (19) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: PARTLT, QUICKSORT, PARTGT, >, >', APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTLT < QUICKSORT PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT > < PARTGT >' < PARTGT > < partGt partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (20) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (21) BOUNDS(n^1, INF) ---------------------------------------- (22) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: >, QUICKSORT, PARTGT, >', APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT > < PARTGT >' < PARTGT > < partGt partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (23) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) Induction Base: >(gen_S:0'16_24(0), gen_S:0'16_24(0)) ->_R^Omega(0) False Induction Step: >(gen_S:0'16_24(+(n12269_24, 1)), gen_S:0'16_24(+(n12269_24, 1))) ->_R^Omega(0) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) ->_IH False We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (24) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: >', QUICKSORT, PARTGT, APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT >' < PARTGT partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (25) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) Induction Base: >'(gen_S:0'16_24(0), gen_S:0'16_24(0)) ->_R^Omega(0) c4 Induction Step: >'(gen_S:0'16_24(+(n12788_24, 1)), gen_S:0'16_24(+(n12788_24, 1))) ->_R^Omega(0) c3(>'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24))) ->_IH c3(gen_c3:c4:c518_24(c12789_24)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (26) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: PARTGT, QUICKSORT, APP, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: PARTGT < QUICKSORT APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (27) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24))) -> *20_24, rt in Omega(n13735_24) Induction Base: PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, 0))) Induction Step: PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, +(n13735_24, 1)))) ->_R^Omega(1) c15(PARTGT[ITE][TRUE][ITE](>(0', gen_S:0'16_24(0)), gen_S:0'16_24(0), Cons(0', gen_Cons:Nil15_24(+(1, n13735_24)))), >'(0', gen_S:0'16_24(0))) ->_L^Omega(0) c15(PARTGT[ITE][TRUE][ITE](False, gen_S:0'16_24(0), Cons(0', gen_Cons:Nil15_24(+(1, n13735_24)))), >'(0', gen_S:0'16_24(0))) ->_R^Omega(0) c15(c9(PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24)))), >'(0', gen_S:0'16_24(0))) ->_IH c15(c9(*20_24), >'(0', gen_S:0'16_24(0))) ->_L^Omega(0) c15(c9(*20_24), gen_c3:c4:c518_24(0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (28) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24))) -> *20_24, rt in Omega(n13735_24) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: APP, QUICKSORT, quicksort, partLt, partGt, app They will be analysed ascendingly in the following order: APP < QUICKSORT quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (29) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: APP(gen_Cons:Nil15_24(n28052_24), gen_Cons:Nil15_24(b)) -> gen_c17:c1819_24(n28052_24), rt in Omega(1 + n28052_24) Induction Base: APP(gen_Cons:Nil15_24(0), gen_Cons:Nil15_24(b)) ->_R^Omega(1) c18 Induction Step: APP(gen_Cons:Nil15_24(+(n28052_24, 1)), gen_Cons:Nil15_24(b)) ->_R^Omega(1) c17(APP(gen_Cons:Nil15_24(n28052_24), gen_Cons:Nil15_24(b))) ->_IH c17(gen_c17:c1819_24(c28053_24)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (30) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24))) -> *20_24, rt in Omega(n13735_24) APP(gen_Cons:Nil15_24(n28052_24), gen_Cons:Nil15_24(b)) -> gen_c17:c1819_24(n28052_24), rt in Omega(1 + n28052_24) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: partLt, QUICKSORT, quicksort, partGt, app They will be analysed ascendingly in the following order: quicksort < QUICKSORT partLt < QUICKSORT partGt < QUICKSORT partLt < quicksort partGt < quicksort app < quicksort ---------------------------------------- (31) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(n29358_24)) -> gen_Cons:Nil15_24(n29358_24), rt in Omega(0) Induction Base: partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(0)) ->_R^Omega(0) Nil Induction Step: partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(n29358_24, 1))) ->_R^Omega(0) partLt[Ite][True][Ite](<(0', gen_S:0'16_24(1)), gen_S:0'16_24(1), Cons(0', gen_Cons:Nil15_24(n29358_24))) ->_L^Omega(0) partLt[Ite][True][Ite](True, gen_S:0'16_24(1), Cons(0', gen_Cons:Nil15_24(n29358_24))) ->_R^Omega(0) Cons(0', partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(n29358_24))) ->_IH Cons(0', gen_Cons:Nil15_24(c29359_24)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (32) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24))) -> *20_24, rt in Omega(n13735_24) APP(gen_Cons:Nil15_24(n28052_24), gen_Cons:Nil15_24(b)) -> gen_c17:c1819_24(n28052_24), rt in Omega(1 + n28052_24) partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(n29358_24)) -> gen_Cons:Nil15_24(n29358_24), rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: partGt, QUICKSORT, quicksort, app They will be analysed ascendingly in the following order: quicksort < QUICKSORT partGt < QUICKSORT partGt < quicksort app < quicksort ---------------------------------------- (33) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: partGt(gen_S:0'16_24(0), gen_Cons:Nil15_24(n30883_24)) -> gen_Cons:Nil15_24(0), rt in Omega(0) Induction Base: partGt(gen_S:0'16_24(0), gen_Cons:Nil15_24(0)) ->_R^Omega(0) Nil Induction Step: partGt(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(n30883_24, 1))) ->_R^Omega(0) partGt[Ite][True][Ite](>(0', gen_S:0'16_24(0)), gen_S:0'16_24(0), Cons(0', gen_Cons:Nil15_24(n30883_24))) ->_L^Omega(0) partGt[Ite][True][Ite](False, gen_S:0'16_24(0), Cons(0', gen_Cons:Nil15_24(n30883_24))) ->_R^Omega(0) partGt(gen_S:0'16_24(0), gen_Cons:Nil15_24(n30883_24)) ->_IH gen_Cons:Nil15_24(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (34) Obligation: Innermost TRS: Rules: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24))) -> *20_24, rt in Omega(n13735_24) APP(gen_Cons:Nil15_24(n28052_24), gen_Cons:Nil15_24(b)) -> gen_c17:c1819_24(n28052_24), rt in Omega(1 + n28052_24) partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(n29358_24)) -> gen_Cons:Nil15_24(n29358_24), rt in Omega(0) partGt(gen_S:0'16_24(0), gen_Cons:Nil15_24(n30883_24)) -> gen_Cons:Nil15_24(0), rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: app, QUICKSORT, quicksort They will be analysed ascendingly in the following order: quicksort < QUICKSORT app < quicksort ---------------------------------------- (35) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: app(gen_Cons:Nil15_24(n32420_24), gen_Cons:Nil15_24(b)) -> gen_Cons:Nil15_24(+(n32420_24, b)), rt in Omega(0) Induction Base: app(gen_Cons:Nil15_24(0), gen_Cons:Nil15_24(b)) ->_R^Omega(0) gen_Cons:Nil15_24(b) Induction Step: app(gen_Cons:Nil15_24(+(n32420_24, 1)), gen_Cons:Nil15_24(b)) ->_R^Omega(0) Cons(0', app(gen_Cons:Nil15_24(n32420_24), gen_Cons:Nil15_24(b))) ->_IH Cons(0', gen_Cons:Nil15_24(+(b, c32421_24))) 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: QUICKSORT(Cons(z0, Cons(z1, z2))) -> c10(PART(z0, Cons(z1, z2))) QUICKSORT(Cons(z0, Nil)) -> c11 QUICKSORT(Nil) -> c12 PARTLT(z0, Cons(z1, z2)) -> c13(PARTLT[ITE][TRUE][ITE](<(z1, z0), z0, Cons(z1, z2)), <'(z1, z0)) PARTLT(z0, Nil) -> c14 PARTGT(z0, Cons(z1, z2)) -> c15(PARTGT[ITE][TRUE][ITE](>(z1, z0), z0, Cons(z1, z2)), >'(z1, z0)) PARTGT(z0, Nil) -> c16 APP(Cons(z0, z1), z2) -> c17(APP(z1, z2)) APP(Nil, z0) -> c18 NOTEMPTY(Cons(z0, z1)) -> c19 NOTEMPTY(Nil) -> c20 PART(z0, z1) -> c21(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partLt(z0, z1)), PARTLT(z0, z1)) PART(z0, z1) -> c22(APP(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))), QUICKSORT(partGt(z0, z1)), PARTGT(z0, z1)) GOAL(z0) -> c23(QUICKSORT(z0)) <'(S(z0), S(z1)) -> c(<'(z0, z1)) <'(0', S(z0)) -> c1 <'(z0, 0') -> c2 >'(S(z0), S(z1)) -> c3(>'(z0, z1)) >'(0', z0) -> c4 >'(S(z0), 0') -> c5 PARTLT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c6(PARTLT(z0, z2)) PARTLT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c7(PARTLT(z0, z2)) PARTGT[ITE][TRUE][ITE](True, z0, Cons(z1, z2)) -> c8(PARTGT(z0, z2)) PARTGT[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(PARTGT(z0, z2)) <(S(z0), S(z1)) -> <(z0, z1) <(0', S(z0)) -> True <(z0, 0') -> False >(S(z0), S(z1)) -> >(z0, z1) >(0', z0) -> False >(S(z0), 0') -> True partLt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partLt(z0, z2)) partLt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partLt(z0, z2) partGt[Ite][True][Ite](True, z0, Cons(z1, z2)) -> Cons(z1, partGt(z0, z2)) partGt[Ite][True][Ite](False, z0, Cons(z1, z2)) -> partGt(z0, z2) quicksort(Cons(z0, Cons(z1, z2))) -> part(z0, Cons(z1, z2)) quicksort(Cons(z0, Nil)) -> Cons(z0, Nil) quicksort(Nil) -> Nil partLt(z0, Cons(z1, z2)) -> partLt[Ite][True][Ite](<(z1, z0), z0, Cons(z1, z2)) partLt(z0, Nil) -> Nil partGt(z0, Cons(z1, z2)) -> partGt[Ite][True][Ite](>(z1, z0), z0, Cons(z1, z2)) partGt(z0, Nil) -> Nil app(Cons(z0, z1), z2) -> Cons(z0, app(z1, z2)) app(Nil, z0) -> z0 notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False part(z0, z1) -> app(quicksort(partLt(z0, z1)), Cons(z0, quicksort(partGt(z0, z1)))) goal(z0) -> quicksort(z0) Types: QUICKSORT :: Cons:Nil -> c10:c11:c12 Cons :: S:0' -> Cons:Nil -> Cons:Nil c10 :: c21:c22 -> c10:c11:c12 PART :: S:0' -> Cons:Nil -> c21:c22 Nil :: Cons:Nil c11 :: c10:c11:c12 c12 :: c10:c11:c12 PARTLT :: S:0' -> Cons:Nil -> c13:c14 c13 :: c6:c7 -> c:c1:c2 -> c13:c14 PARTLT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c6:c7 < :: S:0' -> S:0' -> True:False <' :: S:0' -> S:0' -> c:c1:c2 c14 :: c13:c14 PARTGT :: S:0' -> Cons:Nil -> c15:c16 c15 :: c8:c9 -> c3:c4:c5 -> c15:c16 PARTGT[ITE][TRUE][ITE] :: True:False -> S:0' -> Cons:Nil -> c8:c9 > :: S:0' -> S:0' -> True:False >' :: S:0' -> S:0' -> c3:c4:c5 c16 :: c15:c16 APP :: Cons:Nil -> Cons:Nil -> c17:c18 c17 :: c17:c18 -> c17:c18 c18 :: c17:c18 NOTEMPTY :: Cons:Nil -> c19:c20 c19 :: c19:c20 c20 :: c19:c20 c21 :: c17:c18 -> c10:c11:c12 -> c13:c14 -> c21:c22 quicksort :: Cons:Nil -> Cons:Nil partLt :: S:0' -> Cons:Nil -> Cons:Nil partGt :: S:0' -> Cons:Nil -> Cons:Nil c22 :: c17:c18 -> c10:c11:c12 -> c15:c16 -> c21:c22 GOAL :: Cons:Nil -> c23 c23 :: c10:c11:c12 -> c23 S :: S:0' -> S:0' c :: c:c1:c2 -> c:c1:c2 0' :: S:0' c1 :: c:c1:c2 c2 :: c:c1:c2 c3 :: c3:c4:c5 -> c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 True :: True:False c6 :: c13:c14 -> c6:c7 False :: True:False c7 :: c13:c14 -> c6:c7 c8 :: c15:c16 -> c8:c9 c9 :: c15:c16 -> c8:c9 partLt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil partGt[Ite][True][Ite] :: True:False -> S:0' -> Cons:Nil -> Cons:Nil part :: S:0' -> Cons:Nil -> Cons:Nil app :: Cons:Nil -> Cons:Nil -> Cons:Nil notEmpty :: Cons:Nil -> True:False goal :: Cons:Nil -> Cons:Nil hole_c10:c11:c121_24 :: c10:c11:c12 hole_Cons:Nil2_24 :: Cons:Nil hole_S:0'3_24 :: S:0' hole_c21:c224_24 :: c21:c22 hole_c13:c145_24 :: c13:c14 hole_c6:c76_24 :: c6:c7 hole_c:c1:c27_24 :: c:c1:c2 hole_True:False8_24 :: True:False hole_c15:c169_24 :: c15:c16 hole_c8:c910_24 :: c8:c9 hole_c3:c4:c511_24 :: c3:c4:c5 hole_c17:c1812_24 :: c17:c18 hole_c19:c2013_24 :: c19:c20 hole_c2314_24 :: c23 gen_Cons:Nil15_24 :: Nat -> Cons:Nil gen_S:0'16_24 :: Nat -> S:0' gen_c:c1:c217_24 :: Nat -> c:c1:c2 gen_c3:c4:c518_24 :: Nat -> c3:c4:c5 gen_c17:c1819_24 :: Nat -> c17:c18 Lemmas: <(gen_S:0'16_24(n21_24), gen_S:0'16_24(+(1, n21_24))) -> True, rt in Omega(0) <'(gen_S:0'16_24(n463_24), gen_S:0'16_24(+(1, n463_24))) -> gen_c:c1:c217_24(n463_24), rt in Omega(0) PARTLT(gen_S:0'16_24(1), gen_Cons:Nil15_24(+(1, n1240_24))) -> *20_24, rt in Omega(n1240_24) >(gen_S:0'16_24(n12269_24), gen_S:0'16_24(n12269_24)) -> False, rt in Omega(0) >'(gen_S:0'16_24(n12788_24), gen_S:0'16_24(n12788_24)) -> gen_c3:c4:c518_24(n12788_24), rt in Omega(0) PARTGT(gen_S:0'16_24(0), gen_Cons:Nil15_24(+(1, n13735_24))) -> *20_24, rt in Omega(n13735_24) APP(gen_Cons:Nil15_24(n28052_24), gen_Cons:Nil15_24(b)) -> gen_c17:c1819_24(n28052_24), rt in Omega(1 + n28052_24) partLt(gen_S:0'16_24(1), gen_Cons:Nil15_24(n29358_24)) -> gen_Cons:Nil15_24(n29358_24), rt in Omega(0) partGt(gen_S:0'16_24(0), gen_Cons:Nil15_24(n30883_24)) -> gen_Cons:Nil15_24(0), rt in Omega(0) app(gen_Cons:Nil15_24(n32420_24), gen_Cons:Nil15_24(b)) -> gen_Cons:Nil15_24(+(n32420_24, b)), rt in Omega(0) Generator Equations: gen_Cons:Nil15_24(0) <=> Nil gen_Cons:Nil15_24(+(x, 1)) <=> Cons(0', gen_Cons:Nil15_24(x)) gen_S:0'16_24(0) <=> 0' gen_S:0'16_24(+(x, 1)) <=> S(gen_S:0'16_24(x)) gen_c:c1:c217_24(0) <=> c1 gen_c:c1:c217_24(+(x, 1)) <=> c(gen_c:c1:c217_24(x)) gen_c3:c4:c518_24(0) <=> c4 gen_c3:c4:c518_24(+(x, 1)) <=> c3(gen_c3:c4:c518_24(x)) gen_c17:c1819_24(0) <=> c18 gen_c17:c1819_24(+(x, 1)) <=> c17(gen_c17:c1819_24(x)) The following defined symbols remain to be analysed: quicksort, QUICKSORT They will be analysed ascendingly in the following order: quicksort < QUICKSORT