Due Fri, 2 Mar in class
Read the notes from Feb 27. It walks through a proof of equivalence between quick sort and insertion sort, but six assumptions (marked *1, *2, ..., *6) are left unproved. Prove each one. Note that the lemmas are stated partially in English; take care to state and prove the right thing.
You may do this by hand; I won't require you to convince ACL2 that qsort = isort until after the break. But feel free to get a jump on that if you are up to it.