test/phase7/structure-obligation-batch.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

\begin{axiom}\label{phase7_batch_prefix}
    $\emptyset = \emptyset$.
\end{axiom}

\begin{struct}\label{phase7_batch_structure}
    A phase seven batch structure $X$ is a onesorted structure equipped with
    \begin{enumerate}
        \item $\phaseSevenPick$
    \end{enumerate}
    such that
    \begin{enumerate}
        \item\label{phase7_batch_first} $X = X$.
        \item\label{phase7_batch_second}
            $\phaseSevenPick[X] = \phaseSevenPick[X]$.
    \end{enumerate}
\end{struct}