I'm working with the size-change termination principle to show program termination. In the system I work with, there is a so-called bit-vector ordering that goes as follows:
Given two sequences of arguments $s_1,s_2$.
Filter the bitvector arguments (long/int/short/byte)
Divide each sequence of arguments $s$ according to length (so one group is int, other short and so on). Denote the arguments of type $t$ in sequence $s$ as $s.t$.
If $s.t$ is defined for $s_1,s_2$, compare $s_1.t$ with $s_2.t$ lexicographically.
We define $s_1 < s_2$ when there exists a type $t$ such that $s_1.t < s_2.t$.
I have confirmed that this behaviour is wrong. Indeed, if one has two sequences $s_1,s_2$ that contain ints and shorts where $s_1.int < s_2.int$ and $s_2.short < s_1.short$ we would deduce that $s_1 < s_2$ and $s_2 < s_1$.
What is the standard orders for lists of bitvectors while using the size-change termination principle?