 Set of well-order codes

The set of well-order codes $\mathrm{WF}\subseteq {\omega }^{\omega }$ consists of codes for strict well-orders $(D,R)$ on subsets $D\subseteq \omega$. The norm $\Vert x\Vert$ is their order type. Every countable ordinal, including finite ordinals and zero, has such a code.

For a coding convenient for games, ignore $x(0)$ as a tag. At coordinate $x(n+1)$ record the domain bit for $n$ and the finitely many relation bits $R(i,j)$ with $\max (i,j)=n$, in a fixed order. Read these bits from the binary expansion, ignoring unused higher bits. The code belongs to $\mathrm{WF}$ exactly when the decoded relation is a strict well-order of its decoded domain. This convention makes local recoding operations explicit and allows an arbitrary domain subset, rather than incorrectly requiring every well-order to have domain all of $\omega$.