diff --git a/soundness.tex b/soundness.tex index 2654791..f7b1c5a 100644 --- a/soundness.tex +++ b/soundness.tex @@ -271,15 +271,25 @@ $\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$ %\item[Capture, Reduce] are always applied together. We have to destinct between two cases: \item[Prepare] To show -$\Delta \vdash \wctype{\overline{\wildcard{B}{U}{L}}}{C}{\ol{S}} <: \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$ by S-Exists we have to proof: +$\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} \\ -\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta) \\ +\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{X}{U}{L}}}{C}{\ol{S}}) = \emptyset +\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{A}{U}{L}}}{C}{\ol{T}}) = \emptyset \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}. \item[Capture] If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.