From fabbbecdda4f3f04137a0fb744d3484bc36cf114 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Tue, 10 Oct 2023 01:18:13 -0400
Subject: [PATCH] formalism: Fix and add missing analytic zipper rules for
 zippered marked lambda

---
 formalism/typed.tex | 57 +++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 53 insertions(+), 4 deletions(-)

diff --git a/formalism/typed.tex b/formalism/typed.tex
index 7442847..0d27e78 100644
--- a/formalism/typed.tex
+++ b/formalism/typed.tex
@@ -997,7 +997,7 @@ \subsubsection{Analytic expression actions}
     \notMatchedArrow{\TMV} \\
     \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TUnknown}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
   }{
-    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}}{\TMV}{\SLam{x}}
+    \AACon{\ctx}{\ZCCursor{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTCursor{\TUnknown}}{\ECMV'}}{\TMV}{\SLam{x}}
   }
 
   \inferrule[AAEConLetL]{
@@ -1079,15 +1079,51 @@ \subsubsection{Analytic expression actions}
     \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV'}} \\
     \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
     \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
-    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\TMV_1}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCInconType{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamT4]{
     \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT5]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\\\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TUnknown}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT6]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \equal{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT7]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
+    \consistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamT8]{
+    \AUTAction{\ZTMV_3}{\ZTMV_3'}{\AMV} \\
+    \notEqual{\cursorErase{\ZTMV_3}}{\cursorErase{\ZTMV_3'}} \\
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\\\
+    \inconsistent{\cursorErase{\ZTMV_3'}}{\TMV_1} \\
+    \ctxAnaFixedInto{\extendCtx{\ctx}{x}{\cursorErase{\ZTMV_3'}}}{\erase{\ECMV}}{\ECMV'}{\TMV_2}
   }{
-    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowT{x}{\ZTMV_3}{\ECMV}}{\ZCLamT{x}{\ZTMV_3'}{\ECMV}}{\TMV}{\AMV}
+    \AAAction{\ctx}{\ZCLamInconAscT{x}{\ZTMV_3}{\ECMV}}{\ZCLamInconAscT{x}{\ZTMV_3'}{\ECMV'}}{\TMV}{\AMV}
   }
 
   \inferrule[AAEZipLamE1]{
@@ -1097,6 +1133,19 @@ \subsubsection{Analytic expression actions}
     \AAAction{\ctx}{\ZCLamE{x}{\TMV_3}{\ZCMV}}{\ZCLamE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
   }
 
+  \inferrule[AAEZipLamE2]{
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TUnknown}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV}}{\ZCLamAnaNonMatchedArrowE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
+  \inferrule[AAEZipLamE3]{
+    \matchedArrow{\TMV}{\TMV_1}{\TMV_2} \\
+    \AAAction{\extendCtx{\ctx}{x}{\TMV_3}}{\ZCMV}{\ZCMV'}{\TMV_2}{\AMV}
+  }{
+    \AAAction{\ctx}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV}}{\ZCLamInconAscE{x}{\TMV_3}{\ZCMV'}}{\TMV}{\AMV}
+  }
+
   \inferrule[AAEZipLetL1]{
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
     \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\