Trying to prove sort algorithm correctness (for specific n), in search for hints

[mwuttke97]

@LessnessR

Algorithm textbook by Cormen et al abstracts everything away and uses decision tree model for the proof. Correspondence between sorting algorithm and decision tree isn’t obvious even for me as a human.

Incidently, in a survey paper recently announced on the Coq Club, there is a link to a formalisation in Isabelle/HOL of the bound of comparisons.