Barrier in better-quasi-order theory (source code)

= Barrier in better-quasi-order theory
{title2=$B\subseteq[A]^{<\omega}$}

A barrier on an infinite $A\subseteq\mathbb N$ is a family of nonempty finite increasing sequences, viewed as finite subsets, no one contained properly in another, such that every infinite subset of $A$ has a member of the family as an initial segment. Write $s\triangleleft t$ if there is a finite increasing sequence $u$ of which $s$ is an initial segment and of which $t$ is an initial segment after its first term is deleted. This shift relation underlies the good-array definition of <better-quasi-ordering>.