Well-quasi-ordering (source code)

= Well-quasi-ordering
{title2=$\forall(x_i)\ \exists i<j\ (x_i\leq x_j)$}
{wiki}

= Well-quasi-order
{synonym}

= Well-quasi-ordered
{synonym}

A <preorder> is a <well-quasi-ordering> if every infinite <sequence> has indices $i<j$ with $x_i\leq 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.