1 files changed, 56 insertions, 0 deletions
diff --git a/test/phase5/exact-contextual-abbreviation.tex b/test/phase5/exact-contextual-abbreviation.tex
new file mode 100644
index 0000000..9b4387e
--- /dev/null
+++ b/test/phase5/exact-contextual-abbreviation.tex
@@ -0,0 +1,56 @@
+\begin{signature}\label{phase5_context_apply}
+    $\apply{f}{x}$ is a set.
+\end{signature}
+
+\begin{signature}\label{phase5_context_pair}
+    $(a,b)$ is a set.
+\end{signature}
+
+\begin{struct}\label{phase5_context_magma}
+    A phase five context magma $A$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\phasefivecombine$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{phase5_context_refl} $A = A$.
+    \end{enumerate}
+\end{struct}
+
+\begin{struct}\label{phase5_context_unital_magma}
+    A phase five context unital magma $A$ is a phase five context magma.
+\end{struct}
+
+\begin{abbreviation}\label{phase5_context_dot}
+    %! infixl 4
+    $a\phasefivedot b = \phasefivecombine(a,b)$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{phase5_context_commutes}
+    $a$ phase five commutes with $b$ iff
+    $a\phasefivedot b = b\phasefivedot a$.
+\end{abbreviation}
+
+\begin{proposition}\label{phase5_context_dot_explicit}
+    Let $A$ be a phase five context magma.
+    Let $a,b$ be sets.
+    Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
+\end{proposition}
+
+\begin{proposition}\label{phase5_context_inherited}
+    Let $A$ be a phase five context unital magma.
+    Let $a,b$ be sets.
+    Then $a\phasefivedot b = \phasefivecombine[A](a,b)$.
+\end{proposition}
+
+\begin{proposition}\label{phase5_context_nested}
+    Let $A$ be a phase five context magma.
+    Let $a,b$ be sets.
+    Then $a$ phase five commutes with $b$ iff
+        $\phasefivecombine[A](a,b) = \phasefivecombine[A](b,a)$.
+\end{proposition}
+
+\begin{proposition}\label{phase5_context_explicit_unique}
+    Let $A,a,b$ be sets.
+    Then $\phasefivecombine[A](a,b) = \phasefivecombine[A](a,b)$.
+\end{proposition}