From ba4b78b57bb8d13cfa5ead9280373a7e232f0c29 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Wed, 24 Jan 2024 13:18:48 +0100
Subject: [PATCH] Soundness method call

---
 soundness.tex | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/soundness.tex b/soundness.tex
index 7e069ca..5e9b2c0 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -76,7 +76,7 @@ So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r})
         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
         \label{sp:4}
-        \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} \\
+        \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
     \end{gather}
     \ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$.
     $\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with 
@@ -84,8 +84,13 @@ So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r})
 
     If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
     then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
-    \ref{sp:4} is not using $\ol{\Delta}$.
-    $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$
+    Let $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$, then
+    \ref{sp:4} by lemma \ref{lemma:unifySoundness} and \ref{lemma:tvsNoFV}.
+    The environments $\overline{\Delta}$ are not needed,
+    because none of the variables in $\text{dom}(\overline{\Delta})$ are used in $\ol{T}$ or $\Delta, \Delta'$.
+
+\ref{sp:3}
+%TODO: S is not in \sigma. They are generated by a local type inference algorithm
 
 Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
 %TODO: show that only those wildcards in the parameters and receiver type are used ($\ol{\Delta}$)
@@ -106,9 +111,6 @@ Method calls generate multiple constraints that share the same wildcard placehol
     % then they are all contained in $\Delta, \Delta', \overline{Delta}$, which makes S ok true! (does it?)
     % and due to r <. T, the judgements N <: [S/X]U and T_r <: \Delta.N are true!
 
-    %TODO for Unify:
-    We have to make sure, that wildcards are correctly saved in the Wildcard environment
-    
     % If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses
 \end{description}