From 5e64e63c1ea1272378e85f5af0ccd7446d9f0c58 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Mon, 9 Oct 2023 13:43:01 -0400
Subject: [PATCH] formalism: Fix some analytic zipper rules for marked zexp
 lambda

---
 formalism/typed.tex | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/formalism/typed.tex b/formalism/typed.tex
index 13a8176..7442847 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -1058,33 +1058,39 @@ \subsubsection{Analytic expression actions}
 \paragraph{Zipper Cases} \ \\
 \begin{mathparpagebreakable}
   \inferrule[AAEZipLamT1]{
-    \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\
-    \consistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}}
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
   }{
-    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV'}{\ECMV}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamT2]{
-    \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\
-    \inconsistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} \\
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
-    \consistent{\cursorErase{\ZTMV'}}{\TMV_1} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+    \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCLamT{x}{\ZTMV'}{\ECMV'}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamT3]{
-    \AUTAction{\ZTMV}{\ZTMV'}{\AMV} \\
-    \inconsistent{\cursorErase{\ZTMV}}{\cursorErase{\ZTMV'}} \\
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV'}} \\
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
-    \inconsistent{\cursorErase{\ZTMV'}}{\TMV_1} \\
+    \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
     \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV'}{\ECMV'}}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}}{\TMV}{\AMV}
   }
 
-  \inferrule[AAEZipLamE]{
+  \inferrule[AAEZipLamT4]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamE1]{
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
     \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV}
   }{