Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new in the AFP: List_Inversions

view this post on Zulip Email Gateway (Aug 22 2022 at 19:12):

From: Gerwin.Klein@data61.csiro.au
The Inversions of a List
by Manuel Eberl

This entry defines the set of inversions of a list, i.e. the pairs
of indices that violate sortedness. It also proves the correctness
of the well-known O(n log n) divide-and-conquer algorithm to compute
the number of inversions.

https://www.isa-afp.org/entries/List_Inversions.html

Enjoy!
Gerwin

Last updated: Apr 25 2024 at 04:18 UTC