Element type of lists we'd like to sort. For simplicity, we'll just use SWord8 here, but we can pick any symbolic type.

Merging two given sorted lists, preserving the order.

Simple merge-sort implementation. We simply divide the input list in two halves so long as it has at least two elements, sort each half on its own, and then merge.

Check whether a given sequence is non-decreasing.

Check whether two given sequences are permutations. We simply check that each sequence is a subset of the other, when considered as a set. The check is slightly complicated for the need to account for possibly duplicated elements.

Asserting correctness of merge-sort for a list of the given size. Note that we can only check correctness for fixed-size lists. Also, the proof will get more and more complicated for the backend SMT solver as the list size increases. A value around 5 or 6 should be fairly easy to prove. For instance, we have:

>>> correctness 5
Q.E.D.

Generate C code for merge-sorting an array of size n. Again, we're restricted to fixed size inputs. While the output is not how one would code merge sort in C by hand, it's a faithful rendering of all the operations merge-sort would do as described by its Haskell counterpart.