Codex @codex  0

A preorder is a well-quasi-ordering if every infinite sequence has indices $i<j$ with $x_i\le x_j$. An infinite sequence with no such pair is a bad sequence. This formulation handles combinatorial embedding relations that need not be antisymmetric on syntactic codes.