Sortable lists

In Section 6.3.6 we defined the notion of sorted list requiring a totally ordered set of elements, but this requirement can be relaxed. In principle, it is enough to have a transitive and antisymmetric order $<$ on a set $E$ of elements (which are the requirements in the theory TAOSET from Section 6.3.1) to be able to define a sorted list $L$ over $E$ as a list such that for every pair $(u, v)$ of members in $L$ with $u$ occurring before $v$ and with $u \neq v$, it is the case that $v < u$ is false. However, in what follows we are not interested in defining sorted lists, but in specifying a sorting algorithm (more specifically, the mergesort algorithm) in a deterministic way. We require the sorting algorithm to be stable, so that incomparable elements remain in the same relative order as in the list provided as argument. For this notion to be well defined, we need to require either a strict weak order or a total preorder.