From 521dee7fa2131a58540e39b5cb1846f05d5f6e04 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Tue, 16 Jan 2024 10:00:47 +0100
Subject: [PATCH] Soundness Prepare

---
 soundness.tex | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

diff --git a/soundness.tex b/soundness.tex
index f7b1c5a..ae338c2 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -272,24 +272,29 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Prepare] 
 To show 
 $\Delta \vdash \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof:
-We know
-\begin{gather}
-    \ol{S} = \ol{T}\\
-    \text{fv}(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) = \emptyset\\
-    \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
-    %TODO
-\end{gather}
-
 \begin{gather}
 \Delta', \Delta \vdash [\ol{T}/\ol{\type{A}}]\ol{L} <: \ol{T} \\
 \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
 \label{rp:3}
 \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \overline{\wildcard{B}{U}{L}}) \\
 \label{rp:4}
-\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset
+\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset\\
+[\ol{A}/\ol{T}] = \ol{T} %TODO: rename T
 \end{gather}
-\ref{rp:4} is always true.
-Due to $\text{fv}(\sigma(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}})) = \emptyset$ implies \ref{rp:3}.
+
+We know
+\begin{gather}
+    \ol{S} = [\ol{\wtv{a}}/\ol{A}]\ol{T}\\
+    \text{fv}(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}}) = \emptyset\\
+\label{rp:fv2}
+    \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+    %TODO
+\end{gather}
+
+\ref{rp:fv2} implies \ref{rp:4}.
+Due to $\text{fv}(\sigma(\wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}})) = \emptyset$ implies
+$\text{fv}(\type{T}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U}}{\type{L}}})$
+and therefore \ref{rp:3}.
 
 \item[Capture]
 If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.