Dear Cafe, some years ago I formalized the mergesort implementation [1] from http://hackage.haskell.org/package/base-4.11.1.0/docs/src/Data.OldList.html#... (as far as I can tell it didn't change since 2012) in the proof assistant Isabelle/HOL [2]. More specifically, I proved its functional correctness (the result is sorted and contains all elements of the input with exactly the same multiplicities) and that it is a stable sorting algorithm. Very recently I also formalized a complexity result in Isabelle/HOL, namely that the number of comparisons is bounded from above by n + n * ⌈log 2 n⌉ for lists of length n. For this proof I had to change the definition of "sequences", "ascending", and "descending" slightly. Now here is my question: Does anyone now of reasons why the current implementation of "sequences" is allowed to produce spurious empty lists in its result? The version I used in my formalization only differs in the following three spots: sequences [x] = [[x]] -- this is the only important change, since sequences [] = [] -- then the result does not contain empty lists instead of sequences xs = [xs] and ascending a as [] = let !x = as [a] in [x] instead of ascending a as bs = let !x = as [a] in x : sequences bs and descending a as [] = [a:as] instead of descending a as bs = (a:as) : sequences bs [1] https://www.isa-afp.org/entries/Efficient-Mergesort.html [2] http://isabelle.in.tum.de/