That is actually the sort criteria we end up deciding to try, assuming I'm interpreting your list correctly. But we then prove it's not a total ordering, so we're going to have to use something other than a total ordering sort in order to use it - and that's where we left off before my headphones broke :)
- Casey