Optimal Binary Search Trees. - Tobias Nipkow; Dániel Somogyi (Arch. Formal Proofs, 2018)