From 8b44a5bf5a379942564e026c47806f8ef23b4e8e Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Tue, 13 Feb 2024 19:14:10 +0100
Subject: [PATCH] Remove Normalize rule

---
 unify.tex | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/unify.tex b/unify.tex
index 797d2a7..247be21 100644
--- a/unify.tex
+++ b/unify.tex
@@ -244,17 +244,17 @@ $
     \leavevmode
     \fbox{
     \begin{tabular}[t]{l@{~}l}
-\rulename{normalize}
-    & $
-    \begin{array}[c]{l}
-    \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B}  } \\ 
-    \hline
-    \vspace*{-0.4cm}\\
-    \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'}  }
-    \end{array}
-    % \quad \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
-    $
-    \\\\
+% \rulename{normalize} %obsolete because of Tame
+%     & $
+%     \begin{array}[c]{l}
+%     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B}  } \\ 
+%     \hline
+%     \vspace*{-0.4cm}\\
+%     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'}  }
+%     \end{array}
+%     % \quad \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
+%     $
+%     \\\\
 \rulename{Tame}
     & $
     \begin{array}[c]{l}