1. Spezifizieren sie einen Listen-basierten Quicksort-Algorithmus funktional in HOL.

2. Beweisen Sie, dass die Ergebnisliste sortiert ist.

3. Erzeugen Sie ausführbaren Code für den Algorithmus.

4. Sortieren Sie die Listen [], [3,7,4,0] und ["c","ab","e","d"] mit dem erzeugen Code!