1 files changed, 16 insertions, 0 deletions
diff --git a/test/phase7/structure-obligation-batch.tex b/test/phase7/structure-obligation-batch.tex
new file mode 100644
index 0000000..c71d6cd
--- /dev/null
+++ b/test/phase7/structure-obligation-batch.tex
@@ -0,0 +1,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}