\begin{definition}[Definition:Ordinal Addition]
Let $x$ and $y$ be ordinals.
The operation of '''ordinal addition''' $x + y$ is defined using transfinite recursion on $y$, as follows.
\end{definition}