From 3398cccd9684e89f499e878c1b45fb5cc9b5a59a Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Wed, 14 Feb 2024 05:32:47 +0100
Subject: [PATCH] Move Crunch

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

diff --git a/unify.tex b/unify.tex
index 7db53b6..1017038 100644
--- a/unify.tex
+++ b/unify.tex
@@ -574,6 +574,34 @@ Their upper and lower bounds are fresh type variables.
   \end{array}
   \end{array}
   $
+\\\\ 
+\rulename{Crunch}
+& $\begin{array}[c]{@{}ll}
+\begin{array}[c]{l}
+\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ 
+\hline
+\vspace*{-0.4cm}\\
+\wildcardEnv \vdash
+C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} 
+\end{array}
+&\begin{array}[c]{l}
+  \ol{U} = \ol{L}
+\end{array}
+\end{array}$
+\\\\ 
+\rulename{Crunch}
+& $\begin{array}[c]{@{}ll}
+\begin{array}[c]{l}
+\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ 
+\hline
+\vspace*{-0.4cm}\\
+\wildcardEnv \vdash
+C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} 
+\end{array}
+&\begin{array}[c]{l}
+  \ol{U} = \ol{L}
+\end{array}
+\end{array}$
     \end{tabular}}
   \end{center}
 \caption{Constraint reduce rules}\label{fig:reduce-rules}
@@ -1148,34 +1176,6 @@ C \cup \set{ \tv{a} \doteq \bot }
 %\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1
 \end{array}
 \end{array}$
-\\\\ 
-\rulename{Crunch}
-& $\begin{array}[c]{@{}ll}
-\begin{array}[c]{l}
-\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ 
-\hline
-\vspace*{-0.4cm}\\
-\wildcardEnv \vdash
-C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} 
-\end{array}
-&\begin{array}[c]{l}
-  \ol{U} = \ol{L}
-\end{array}
-\end{array}$
-\\\\ 
-\rulename{Crunch}
-& $\begin{array}[c]{@{}ll}
-\begin{array}[c]{l}
-\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ 
-\hline
-\vspace*{-0.4cm}\\
-\wildcardEnv \vdash
-C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} 
-\end{array}
-&\begin{array}[c]{l}
-  \ol{U} = \ol{L}
-\end{array}
-\end{array}$
 % \\\\  % The force rule is unnecessary because every type placeholder has an upper bound Object (a <. Object) The match rule eliminates those wildcards
 % \rulename{Force} &$
 %   \begin{array}[c]{@{}ll}