Due Tue, 27 Feb in class
This is a short proof attempt / writing assignment. The proof attempt should be manual, not in ACL2.
Read the lecture notes from February 20. At the end is a puzzle that asks you to consider a proof that quicksort behaves the same as insertion sort.
Write a short paragraph (a few sentences at most) that explains why the structural induction principle does not help for this theorem. You will have to attempt the proof using the SIP to see why. The failure occurs pretty early on in the attempt. If you have trouble identifying it then ask questions. Do the proof by hand, not using ACL2.