From 5c73e0b0f8cfb58e4656eda8690ae42f8b602196 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Mon, 5 Feb 2024 01:33:39 +0100
Subject: [PATCH] Remove Settle and Raise rules

---
 unify.tex | 71 +++++++++++++++++++++++++++++++++----------------------
 1 file changed, 43 insertions(+), 28 deletions(-)

diff --git a/unify.tex b/unify.tex
index 124b0da..84d511d 100644
--- a/unify.tex
+++ b/unify.tex
@@ -128,27 +128,27 @@ $
     \rulename{Upper}
     & $
     \begin{array}[c]{l}
-    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{T} } \\ 
+    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{G} } \\ 
     \hline
     \vspace*{-0.4cm}\\
-    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{T}   }
+    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{G}   }
     \end{array}
     \quad \quad
     \begin{array}[c]{l}
-    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{T} } \\ 
+    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\ 
     \hline
     \vspace*{-0.4cm}\\
-    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{T}   }
+    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G}   }
     \end{array}
     $
     \\\\
     \rulename{Lower}
     & $
     \begin{array}[c]{l}
-    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{A} } \\ 
+    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{A} } \\ 
     \hline
     \vspace*{-0.4cm}\\
-    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup  \set{ \type{T} \lessdot \type{L} }
+    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup  \set{ \type{G} \lessdot \type{L} }
     \end{array}
     $
     \\\\
@@ -607,6 +607,21 @@ This builds a search tree over multiple possible solutions.
 \begin{center}
         \fbox{
         \begin{tabular}[t]{l@{~}l}
+        \rulename{Same}
+        & $
+        \begin{array}[c]{l}
+          \wildcardEnv \vdash
+          C \cup \type{G} \lessdot \tv{a}\\
+          \hline
+          \wildcardEnv \vdash
+          C \cup \set{
+            \tv{a} \doteq \type{G}
+        }
+        \end{array} \quad \begin{array}[c]{l}
+          \text{fv}(\type{G}) \in \Delta_{in}
+        \end{array}
+          $
+      \\\\ 
           \rulename{\generalizeRule}
           & $
           \begin{array}[c]{l}
@@ -665,28 +680,28 @@ This builds a search tree over multiple possible solutions.
         \end{array}
         $
       \\\\ 
-      \rulename{Settle}
-      & $
-      \begin{array}[c]{l}
-        \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-        \tv{a} \lessdot^* \tv{b}}
-        \\
-        \hline
-        \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
-      \end{array}
-      $
-    \\\\ 
-    \rulename{Raise}
-    & $
-    \begin{array}[c]{l}
-      \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
-      \tv{a} \lessdot \tv{b}}
-      \\
-      \hline
-      \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
-    \end{array}
-    $
-  \\\\ 
+  %     \rulename{Settle}
+  %     & $
+  %     \begin{array}[c]{l}
+  %       \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
+  %       \tv{a} \lessdot^* \tv{b}}
+  %       \\
+  %       \hline
+  %       \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N}  }
+  %     \end{array}
+  %     $
+  %   \\\\ 
+  %   \rulename{Raise}
+  %   & $
+  %   \begin{array}[c]{l}
+  %     \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
+  %     \tv{a} \lessdot \tv{b}}
+  %     \\
+  %     \hline
+  %     \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b}  }
+  %   \end{array}
+  %   $
+  % \\\\ 
     \end{tabular}}
   \end{center}
 \caption{Step 2 branching: Multiple rules can be applied to the same constraint}