formalism: Move type meet occurrences to premise in typed hazelnut model

hazelgrove · Oct 10, 2023 · f31e520 · f31e520
1 parent fabbbec
commit f31e520
Showing 1 changed file with 16 additions and 12 deletions.
diff --git a/formalism/typed.tex b/formalism/typed.tex
@@ -786,9 +786,10 @@ \subsubsection{Synthetic expression actions}
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_1} \\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\\\
     \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\
-    \consistent{\TMV_1'}{\TMV_2}
+    \consistent{\TMV_1'}{\TMV_2} \\
+    \TMV' = \TMeet{\TMV_1'}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV}
+    \ASEAction{\ctx}{\ZCIfL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipIfL2]{
@@ -804,9 +805,10 @@ \subsubsection{Synthetic expression actions}
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\
     \ctxSynTypeM{\ctx}{\cursorErase{\ZCMV}}{\TMV_2} \\\\
     \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_2'}
+    \consistent{\TMV_1}{\TMV_2'} \\
+    \TMV' = \TMeet{\TMV_1}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV}
+    \ASEAction{\ctx}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipIfR2]{
@@ -825,32 +827,34 @@ \subsubsection{Synthetic expression actions}
   }
 
   \inferrule[ASEZipInconsistentBranchesL1]{
-    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\
-    \consistent{\TMV_1'}{\TMV_2}
+    \consistent{\TMV_1'}{\TMV_2} \\
+    \TMV' = \TMeet{\TMV_1'}{\TMV_2}
   }{
-    \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMeet{\TMV_1'}{\TMV_2}}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCIfL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesL2]{
-    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\
+    \ASEAction{\ctx}{\ZCMV}{\TMV_1}{\ZCMV'}{\TMV_1'}{\AMV} \\\\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_2} \\
     \inconsistent{\TMV_1'}{\TMV_2}
   }{
     \ASEAction{\ctx}{\ZCInconBrL{\ECMV_1}{\ZCMV}{\ECMV_2}}{\TMV}{\ZCInconBrL{\ECMV_1}{\ZCMV'}{\ECMV_2}}{\TUnknown}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesR1]{
-    \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\
+    \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV_1} \\\\
     \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\
-    \consistent{\TMV_1}{\TMV_2'}
+    \consistent{\TMV_1}{\TMV_2'} \\
+    \TMV' = \TMeet{\TMV_1}{\TMV_2'}
   }{
-    \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMeet{\TMV_1}{\TMV_2'}}{\AMV}
+    \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCIfL{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TMV'}{\AMV}
   }
 
   \inferrule[ASEZipInconsistentBranchesR2]{
+    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\\\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\
-    \ASEAction{\ctx}{\ZCMV}{\TMV_2}{\ZCMV'}{\TMV_2'}{\AMV} \\
     \inconsistent{\TMV_1}{\TMV_2'}
   }{
     \ASEAction{\ctx}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV}}{\TMV}{\ZCInconBrR{\ECMV_1}{\ECMV_2}{\ZCMV'}}{\TUnknown}{\AMV}