From d037f64c19ba468653d7a0727df634988fecb9b9 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Tue, 10 Oct 2023 02:28:00 -0400
Subject: [PATCH] formalism: Fix marked analysis judgment in typed hazelnut
 metatheorem statements

---
 formalism/typed.tex | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/formalism/typed.tex b/formalism/typed.tex
index bc1f869..7a87922 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -1307,7 +1307,7 @@ \subsection{Metatheorems}
       $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and
       $\ctxSynTypeM{\ctx}{\cursorErase{\ZCMV'}}{\TMV'}$.
 
-    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
       $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$, then $\zWellFormed{\ZCMV'}$ and
       $\ctxAnaType{\ctx}{\cursorErase{\ZCMV'}}{\TMV}$.
   \end{enumerate}
@@ -1322,7 +1322,7 @@ \subsection{Metatheorems}
       $\ASEAction{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV'}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and
       $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$ and $\equal{\TMV}{\TMV'}$.
 
-    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
       $\AAEAction{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMove{\MMV}}$, then $\zWellFormed{\ZCMV'}$ and
       $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$.
   \end{enumerate}
@@ -1339,7 +1339,7 @@ \subsection{Metatheorems}
       $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV'}{\TMV}{\AIMV}$.
 
     \item If $\zWellFormed{\ZCMV}$ and $\zWellFormed{\ZCMV'}$ and
-      $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$,
+      $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and $\cursorErase{\ZCMV} = \cursorErase{\ZCMV'}$,
       then there exists $\AIMV$ such that $\movements{\AIMV}$ and
       $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AIMV}$.
   \end{enumerate}
@@ -1354,7 +1354,7 @@ \subsection{Metatheorems}
       $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
       $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$.
 
-    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
       $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
       $\AAEActionIter{\ctx}{\ZCMV}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$.
   \end{enumerate}
@@ -1369,7 +1369,7 @@ \subsection{Metatheorems}
       $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
       $\ASEActionIter{\ctx}{\ZCCursor{\ECMV}}{\TMV}{\ZCMV}{\TMV}{\AIMV}$.
 
-    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
       $\cursorErase{\ZCMV} = \ECMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$ and
       $\AAEActionIter{\ctx}{\ZCCursor{\ECMV}}{\ZCMV}{\TMV}{\AIMV}$.
   \end{enumerate}
@@ -1383,7 +1383,7 @@ \subsection{Metatheorems}
     \item If $\ctxSynTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that
       $\ASEActionIter{\ctx}{\ZCCursor{\EEHole}}{\TUnknown}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$.
 
-    \item If $\ctxAnaType{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that
+    \item If $\ctxAnaTypeM{\ctx}{\ECMV}{\TMV}$, then there exists $\AIMV$ such that
       $\AAEActionIter{\ctx}{\ZCCursor{\EEHole}}{\ZCCursor{\ECMV}}{\TMV}{\AIMV}$.
   \end{enumerate}
 \end{theorem}
@@ -1398,7 +1398,7 @@ \subsection{Metatheorems}
       $\ASEActionIter{\ctx}{\ZCMV}{\TMV}{\ZCMV''}{\TMV''}{\AMV}$, then $\ZCMV' = \ZCMV''$ and
       $\equal{\TMV'}{\TMV''}$.
 
-    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaType{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
+    \item If $\zWellFormed{\ZCMV}$ and $\ctxAnaTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV}$ and
       $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV'}{\TMV}{\AMV}$ and
       $\AAEActionIter{\ctx}{\ZCMV}{\ZCMV''}{\TMV}{\AMV}$, then $\ZCMV' = \ZCMV''$.
   \end{enumerate}