\begin{datatype}\label{phase5_data}
    Define $\phasefivedata$ inductively as follows.
    \begin{enumerate}
        \item $\phasefivezero \in \phasefivedata$.
        \item $\phasefiveatom{n} \in \phasefivedata$ for $n \in \unions{\emptyset}$.
        \item $\phasefivejoin{x}{y} \in \phasefivedata$ for $x \in \phasefivedata$ and $y \in \phasefivedata$.
    \end{enumerate}
\end{datatype}