From 2716a7e2bc04356af1febe0460d4a8613f205fc1 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Tue, 10 Oct 2023 02:41:18 -0400
Subject: [PATCH] formalism: Clean up formatting of untyped hazelnut
 metatheorems

---
 formalism/untyped.tex | 70 ++++++++++++++++++++++++++-----------------
 1 file changed, 43 insertions(+), 27 deletions(-)

diff --git a/formalism/untyped.tex b/formalism/untyped.tex
index 6ab16b0..541203d 100644
--- a/formalism/untyped.tex
+++ b/formalism/untyped.tex
@@ -655,61 +655,77 @@ \subsection{Metatheorems}
 
 \begin{theorem}[name=Movement Erasure Invariance] \
   \begin{enumerate}
-    \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} =
-      \cursorErase{\ZTMV'}$.
+    \item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$,
+      then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$.
 
-    \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZMV} =
-      \cursorErase{\ZMV'}$.
+    \item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$,
+      then $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{theorem}[name=Reachability] \
   \begin{enumerate}
-    \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, then there exists $\AIMV$ such that
-      $\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.
-
-    \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, then there exists $\AIMV$ such that
-      $\movements{\AIMV}$ and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.
+
+    \item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{lemma}[name=Reach Up] \
   \begin{enumerate}
-    \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.
-
-    \item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \TMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.
+
+    \item If $\cursorErase{\ZMV} = \EMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$.
   \end{enumerate}
 \end{lemma}
 
 \begin{lemma}[name=Reach Down] \
   \begin{enumerate}
-    \item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.
-
-    \item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
-      and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$.
+    \item If $\cursorErase{\ZTMV} = \TMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.
+
+    \item If $\cursorErase{\ZMV} = \EMV$,
+      then there exists $\AIMV$
+        such that $\movements{\AIMV}$
+          and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$.
   \end{enumerate}
 \end{lemma}
 
 \begin{theorem}[name=Constructability] \
   \begin{enumerate}
-    \item For every $\TMV$, there exists $\AIMV$ such that
-      $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.
+    \item For every $\TMV$,
+        there exists $\AIMV$
+          such that $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.
 
-    \item For every $\EMV$, there exists $\AIMV$ such that
-      $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$.
+    \item For every $\EMV$,
+        there exists $\AIMV$
+          such that $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$.
   \end{enumerate}
 \end{theorem}
 
 \begin{theorem}[name=Determinism] \
   \begin{enumerate}
-    \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then
-      $\ZTMV' = \ZTMV''$.
+    \item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$
+        and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$,
+      then $\ZTMV' = \ZTMV''$.
 
-    \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, then
-      $\ZMV' = \ZMV''$.
+    \item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$
+        and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$,
+      then $\ZMV' = \ZMV''$.
   \end{enumerate}
 \end{theorem}