Ordering sequences containing bitvectors for size-change termination
Surely, you want $s_1 &lt; s_2$ if there is a $t$ such that $s_1.t &lt; s_2.t$ and $s_1.u \leq s_2.u$ for every other field $u$. That, at least, gives you a well-founded order.

But there are many other well-founded orders on tuples, e.g. lexicographical order for some order of the fields (though you might need a heuristic to find the order), and various arithmetic combinations of the sizes of each field.

Modern termination checkers will actually simultaneously search for some order that works among a large family of such orders, by generating constraints of the form "There is some lexicographic order, or some polynomial order that shows termination" and trying to satisfy this constraint all at once.

A couple of papers that address termination analysis for bit-vectors and Java, respectively, are:

Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution

and

Automated Termination Proofs for Java Programs with Cyclic Data


by Giesl &amp; al.