Is there an explicit linear extension for the subsequence partial order? Consider the set of finite sequences (of bounded length $\leq k$, if necessary) whose elements are taken from some finite alphabet $\Sigma$. We define a partial order on this set so that
$X = (X_1,...,X_{m}) \prec Y = (Y_1,...,Y_{n})$ whenever $X$ is a subsequence of $Y$.
Formally, this means that there's a strictly increasing sequence of indices $1 \leq i_1 < i_2 < \cdots < i_m \leq n$ such that $X_j = Y_{i_j}$ for all $1 \leq j \leq m$.
It is known (in ZFC) that every partial order admits a linear extension, but I'm interested in an explicit linear extension for the partial order above. Feel free to interpret "explicit" as liberally as you'd like, but certainly an algorithm that compares $X$ and $Y$ as above running in polynomial time in $m + n$, will count as explicit.

*

*Closely related questions are whether the set of subsets (respectively, multisets) whose elements are taken from $\Sigma$, ordered by $\subseteq$, admits an explicit linear extension. I'd appreciate any information related to these questions too.

 A: Note that two words of the same lengths are comparable if and only if they are equal. So you can order the words in the following way:
$$X\prec^* Y\iff |X|<|Y|\text{ or } (X<_{\rm Lex}Y \text{ and } |X|=|Y|).$$
Here $|X|$ is the length of the word $X$. By $<_{\rm Lex}$ we mean that we fix an enumeration of the alphabet and then $X<_{\rm Lex}Y$ if and only if the smallest $k$ such that $X_k\neq Y_k$ is such that $X_k$ appears before $Y_k$ in the enumeration.
It is not hard to verify that this is linear, and if $X\prec Y$, then $|X|<|Y|$, and so $X\prec^* Y$ as well.
Note that this will work even if the alphabet is infinite (you need to fix a well-order of the alphabet, of course).

Another way to do this is to let $\sup X$ be the largest index of a letter appearing in $X$ and then define $$X\prec^{**}Y\iff \sup X<\sup Y\text{ or }(\sup X=\sup Y\text{ and }X\prec^*Y).$$
So first we have the sequences $(),(X_0),(X_0,X_0),\dots$, then $(X_1),(X_0,X_1)$, etc.
And if you want to have some better length optimisation you can fix a pairing function for the natural numbers (or rather the alphabet and the natural numbers) $(n,m)\mapsto e(n,m)$ and then interleave $\sup X$ and $|X|$ based on $n,m$ when $e(\sup X,|X|)<e(\sup Y,|Y|)$ as natural numbers.
This will prioritise shorter sequences, depending on their supremum. There's all kind of shenanigans you can do here.
The most classic method which I used to give as a guided exercise back when I was teaching set theory in Jerusalem was to define such an order on the finite subsets of $\Bbb N$ and prove it is a well-order: $A\triangleleft B\iff\max(A\mathbin\triangle B)\in B$. It follows that $A\triangleleft\{0,\dots,n-1\}\iff\max A<n$, and therefore every proper initial segment of the order is finite, and therefore there is an order isomorphism to $\Bbb N$.
For sequences it's slightly trickier (since finite sets are finite binary sequences with the last letter being $1$) but we can be clever and interleave those extra $0$s if necessary, or if we have more letters we can resort to the lexicographic ordering when needed.
