Thanks for bearing with me, and responding, even if it might be more efficient for me to wait and read the next parts. It seems like if the quicksort of a list

Thanks for bearing with me, and responding, even if it might be more efficient for me to wait and read the next parts. It seems like if the quicksort of a list L is defined as equal to the concatenation of 1) the quicksort of the subsequence of L consisting of items less than the pivot item, 2) (the list containing) the pivot item, and 3) the quicksort of the subsequence of L consisting of items greater than the pivot, then we can prove properties like "any two items of the resulting list are in sorted order" by case analysis on whether each item is part of (1), (2), or (3). Maybe you would interpret "the quicksort of L is defined as..." to mean "if you're in state quicksort(L), you can proceed to state the-concatenation-of"? If we're working in the realm of mathematics, don't we get definitions, equations, and inductive proofs for free, without making a state machine do it? Edit: Reading more, I guess I'm just doing the sorting inside the "next-state relation" of a state machine, so it's done in one state transition, and saying you could look at quicksort as one way to factor the relation, which by math is equivalent to other ways to factor the relation that resemble other sorting algorithms.