\section{Soundness}

\newcommand{\CC}{\text{CC}}

\begin{theorem}\label{testenv-theorem}
Type inference produces a correctly typed program.
\begin{description}
    \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
    \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
    with $\ol{M} = $
\end{description}
\end{theorem}

\begin{lemma}{Soundness:}
    \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
    \begin{description}
    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } }$
    and $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
    and $\vdash \ol{L} : \mtypeEnvironment{}$
    and $\Gamma \subseteq \mtypeEnvironment{}$
    \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
    and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
    %and $\Delta \vdash \sigma(\type{S}), \sigma(\type{T})\ \ok$
    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$
    \end{description}
\end{lemma}
Regular type placeholders represent type annotations.
These are the only types a \wildFJ{} program needs to be correctly typed.
The type placeholders flagged as wildcard placeholders are intermediate types
used in let statements and as type parameters for generic method calls.

%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
% only used inside the constraint the wildcard variable occurs
% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost

% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?

\textit{Proof:}
By structural induction over the expression $\texttt{e}$.
\begin{description}
    \item[$\texttt{e}.\texttt{f}$] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{r})$ by assumption.
    $\Delta', \Delta\vdash \CC{}(\sigma(\tv{r})) <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
    Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
    %TODO: Proof this: The reason is that r is not flagged with a ? and we only add free variables here, that are in \Delta
    Then $\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \text{dom}(\Delta)$
    and therefore $\text{fv}(\type{N}) \subseteq \text{dom}(\Delta, \Delta')$.
    This implies $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$,
    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$
    and $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
    and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.

%    Set $\sigma(\tv{r}) = \type{T} = \wcNtype{\Delta'}{N}$.
%    Then $\Delta | \Gamma \vdash e : \type{T}$ by assumption. $\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N}$ by S-Refl.
%    $\textit{fields}(\type{N}) = \overline{\type{U}\ f}$ by definition.
%    $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$ by premise.

    $\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO
    %Easy, because unify only generates substitutions for normal type placeholders which are OK

    \item[$\texttt{e}.\texttt{m}(\ol{e})$] 
    \begin{gather}
        \label{sp:1}
        \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
        \label{sp:2}
        \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 \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 
    $\Delta, \Delta' \vdash CC(\sigma(\tv{r})) <: \type{T}$.

    If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
    then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
    % X.List<X> <. List<a?>
    % set \sigma(r) = X.N
    % If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r
    % If  CC(X.N) <: T, then N <: T
    % R <: X.N due to S-Refl.
    % \Delta, X \vdash N <: T due to assumption and S-Exists.
    % What if X.N <: Y (where is this Y coming from?)
    % %TODO:
    % We have to show, that all constraints using the same wtv's C = X1.T1 <. X2.T2 ,...
    % with a? \in T1, T2, ....
    % then \Delta' \subseteq X1, X2, ... for \Delta, \Delta \vdash sigma(T1) <: sigma(X2.T2), ....

    % when only wildcards in the top level domain from the constraints involving the a? variables are involved
    % 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}

\begin{lemma}
\begin{description}
    \item[If] $(\sigma, \Delta) = \unify{}( C )$
    \item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
\end{description}
\end{lemma}
\textit{Proof:} by induction over the \unify{} algorithm.
A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
$\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
%UNIFY fails when there are free variables on the right side of a a =. T constraint

\begin{lemma}
    \unify{} only produces well-formed type substitutions.
    % Could this be done via the GenSigma rule? just check if substitutions are well-formed?
    % L <. U
    % not possible because well-formedness depends on the input, which is not checked (should we check it? is that possible?)
    %only type variables have to be OK

    % TODO: Problem: how to proof \ol{S} ok for T-Call.
    % a <. List<x?> --> here the type substituted for x? must be ok. Proof that by changing Unify to not return type insertions for this type and assume there is a correct substitution for x
\end{lemma}

% %This lemma can be used to proof Normalize rule!
% \begin{lemma}\label{lemma:wildcardReplacement}
%     Wildcards with the same upper and lower bound can be replaced by their bounds without breaking subtype relations.
%     \begin{description}
%         \item[If] $\Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash \type{T} <: \type{S}$
%         \item[and] $\type{U} = \type{L}$ and $\text{fv}(\type{U}) = \emptyset$
%         \item[Then] $\Delta \vdash [\type{U}/\type{X}]\type{T} <: [\type{U}/\type{X}]\type{S}$
%         \end{description}
% \end{lemma}
% \textit{Proof:} %TODO
% %By structural induction over the subtype relation
% %S-Refl: by assumption L <: L implies [\type{U}/\type{X}]L

% \begin{lemma}\label{lemma:noAdditionalFV}
%     Type solution $\sigma$ does not add additional free variables.
%     \begin{description}
%         \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup C)$
%         \item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
%         \item[Then] $fv(\sigma(\overline{ \type{S} })) = \emptyset, fv(\sigma(\overline{ \type{T} })) = \emptyset$
%         \end{description}
% \end{lemma}

% \begin{lemma}
% % https://math.libretexts.org/Bookshelves/Mathematical_Logic_and_Proof/Book%3A_Mathematical_Reasoning__Writing_and_Proof_(Sundstrom)/07%3A_Equivalence_Relations/7.03%3A_Equivalence_Classes
% $\doteq$ is an equivalence relation on a constraint set $C$.

% \begin{description}
% \item[If] $\Delta \vdash \overline{\type{T} <: \type{S}}$ and $\type{T} \doteq \type{S}$
% \item[Then] $\Delta \vdash [\type{T}/\type{S}](\overline{\type{T} <: \type{S}})$
% \end{description}
% \end{lemma}

\begin{lemma} \label{lemma:unifyCC}
Free variables do not leave their scope.
\begin{description}
    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdot \type{S} } } )$
    \item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$, 
        $\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
    \item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $

    % \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
    % \item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
    % \item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
\end{description}

Their scope is the set of constraints, which contain the same free variable placeholders.

    % Wildcard place holders only use free variables occuring in the same constraint as them.
    % \begin{description}
    %     \item[If] $(\sigma, \Delta) = \unify{}( C )$
    %     \item[Then] $\text{fv}(\sigma(\tv{a})) \subseteq \set{ \text{fv}(\type{T}) \cup \text{fv}(\type{S}) \mid \tv{a} \in \text{tph}(\type{T},\type{S}), (\type{T} \lessdot \type{S}) \in C }$
    % \end{description}
\end{lemma}
\textit{Proof:}
%TODO: is it true even?
The input set does not contain free variables, only free variable placeholders.
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
This rule is only applied for the outer wildcard environments for each type.

%where to get a Box<Box<a?>> ?

% Box<Box<a?>> <. Box<? super Box<?>>

% %What is with wildcards in the lower bounds of type
% Box<Box<a?>> <. X_Y.Box<Y>.Box<X>
% Y.Box<Y> <. Box<a?>
% Y =. a?

% Box<Y.Box<Y>> <. Box<? extends Box<a>>
% Y.Box<Y> <. Box<a>

% Problem: für tvs dürfen keine Wildcards eingesetzt werden, außer für die 

\begin{lemma}
The \unify{} algorithm only produces correct output for constraints not containing free variables.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
\item[Then] there exists a $\Delta'$ with:
$\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
and $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.

The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$


% Unify cannot guarantee that only wildcards declared on the left side are used. Example input:
% List<b?> <. List<b?>
% b? =. X
% but if the left side is a normal type (no fv's) then this can be guaranteed (maybe?)
%String <. X_String % here X is not in the environment

% What is the problem?
% a? can only use wildcards, which are declared in \Delta or on the left side 
% Otherwise constraints of the form a <. T cannot ensure soundness!

% We could say that a? only gets free variables hold by the constraints a? appears in

% a constraint a <. T means that there are free variables 
\end{description}
\end{lemma}

% \begin{lemma} % a lemma where we distinguis between free variable on the left or the right side of a constraint (not needed anymore)
%     The \unify{} algorithm only produces correct output for constraints not containing free variables.    
% \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \wcNtype{\Delta'}{N} \lessdot \type{T'} } \cup \overline{ \type{S'} \lessdot \wcNtype{\Delta'}{N'} })$ 
% \item[and] $fv(\overline{ \type{S} }) = \emptyset, fv(\overline{ \type{T} }) = \emptyset, fv(\overline{ \type{T'} }) = \emptyset, fv(\overline{ \type{S'} }) = \emptyset$
% \item[Then] $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
% and $\Delta, \Delta' \vdash \overline{\sigma(\type{N}) <: \sigma(\type{T'})}, \overline{\sigma(\type{S'}) <: \sigma(\type{N'})}$
% %TODO: Rephrase (\Delta' is used three times!)
% %The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
% \end{description}
% \end{lemma}
\textit{Proof:}
%(we are going backwards over the algorithm)
%first we have to determine the \Delta'' -> it's only the wildcards which are free in N
% during this proof we can use Delta'' as we like

For every step in the \unify{} algorithm:
Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
constraint set $C$ before the transformation.
% \begin{description}
% \item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
% \item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$   
% \end{description}

\unify{} terminates with $C = \emptyset$ for which the preposition holds:
$\Delta \vdash \sigma(\emptyset)$

We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
the preposition holds for $C$ using the assumption that it holds for $C'$ :
$\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$

\begin{description}
\item[AddDelta] $C$ is not changed
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
\item[GenSigma] by definition and S-Refl.
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
\item[Ground] Assumption and S-Bot
\item[Sub-Elim] Assumption and S-Refl
\item[Force] by assumption and $\rwildcard{X} = \type{U}$ %TODO: step 5 should remove all X^T_T with T (make wildcards with same upper and lower bounds to normal types)
\item[Raise] Assumption, S-Trans
\item[Settle] Assumption, S-Trans
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
\item[\generalizeRule{}] by Assumption, because $C \subset C'$
\item[Adapt] Assumption, S-Extends, S-Trans
\item[Adopt] Assumption, because $C \subset 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:
\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:4}
\text{dom}(\overline{\wildcard{B}{U}{L}}) \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
\end{gather}
\ref{rp:4} is always true.

\item[Capture]
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ the preposition holds because
$\Delta, \Delta' \vdash [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} <: \wctype{\Delta}{C}{\ol{T}}$ $\implies$
$\Delta' \Delta \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$

%we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
%which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh.

% If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$
% we have to show $\set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}, \Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$,
% which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$.
% The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh.

%If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$.
%$\Delta \vdash \sigma([\ol{C}/\ol{B}]\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ holds by assumption and
%the variables $\ol{B}$ in $\ol{S}$ can be renamed to $\ol{C}$, because $\ol{C} \notin \ol{S}$ ($\ol{C}$ are fresh).
%The assumption implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{C}{\type{U'}}{\type{L'}}}})$
%, which implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}})$.

%We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation.
\item[Reduce]

%Assumption and S-Exists.
% Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
% \begin{description} 
%     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset, \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$:]
%     the preposition holds by Assumption and S-Exists.
%     \item[$\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$:]
%     then $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$ with $\Delta' = \overline{\wildcard{A}{\type{U}}{\type{L}}}$ 
%     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$] $\Delta' = \emptyset$
% \end{description}
% List<X> <. Y.List<Y>, free variables are either in 
If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
Otherwise 
$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
\item[Match] Assumption, S-Trans
\item[Trim] Assumption and S-Exists
\item[Remove] $C$ is not changed
\item[Circle] S-Refl
\item[Swap] by definition
\item[Erase] S-Refl
\item[Equals] by definition
% \item[Reduce]
% The renaming from $\rwildcard{C}$ to $\rwildcard{B}$ is not a problem. It's allowed to rename wildcards inside a type.
% Removing $\rwildcard{C}$ from the environment does not change anything because it was freshly generated and is used nowhere.

% The rest follows directly from S-Exists.
% We can say: $\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$,
% because the input to the \unify{} algorithm has no free type variables and we never substitute a type with free type variables
% and none of the other steps of the algorithm generates a $\lessdot$ constraint containing free type variables on the right side. %TODO: proof

% $\text{fv}(\ol{T}) \subseteq \text{dom}(\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}})$
% TODO: The capture conversion has to be when substituting a $\wtv{a}$ variable. Then we have to rename!
% %Lets first try it without the capture conversion. And involve the wtvs in the second step
% % The algorithm works by never substituting wildcards



% \unify{} cannot guarantee the premise $\text{dom}(\Delta, \Delta') \cap \text{fv}(\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N}) = \emptyset$.
% We loosen the soundness requirements and allow a arbitrary environment $\Delta''$ to be added to the right side of the subtype relation.
% This is still sufficient to proof soundness for the whole algorithm.
% We show that the need for the additional environment $\Delta''$ can be satisfied by a let statement.

% \begin{itemize}
% \item $\Delta, \Delta' \vdash [\ol{T}/\ol{X}]\ol{L} <: \ol{T}$: S-Exists 
% \item $\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}]\ol{U}$: S-Exists
% \item $\textit{fv}(\ol{T}) \subseteq \text{dom}{\Delta, \Delta'}$: $\wildcardEnv$ holds all variables %TODO: Proof
% \end{itemize}
\item[Normalize] Assumption and lemma 5 \emph{substitution preserves subtyping}.%\ref{lemma:wildcardReplacement}. (Or Lemma 5 from the wildcard paper. \emph{substitution preserves subtyping})
% The GenSigma step replaces both sides of $\rwildcard{A} \doteq \rwildcard{B}$ with the upper bound $\type{U}$.
% This works for every constraint, whether it contains free variables or not.
% It does not add to free variables of constraints because the upper bound does not contain any.
The GenSigma and Gen Delta steps remove Wildcards which have the same upper and lower bound.
$\rwildcard{A},\rwildcard{B} \notin \sigma(C)$

% sigma(T) = sigma(U) we have to show that T = U means \Delta \vdash [T/U]C \implies \Delta \vdash [U/T]C 
% the constraints L <. U, U <. L lead to L =. U
%If L is List<X> with X being free wildcard
%then U <. L will fail if U is type variable




% this is because bounds never contain free variables (is that true?)

%This type contains free variables when A is replaced by an CC wildcard

%This must fail:
\begin{verbatim}
<A> A m(List<? extends List<A>> l, A)

m(List<List<? super String>> l, "hi") 
\end{verbatim}
%This fails because of Equals rule (TODO: proof)

\item[Tame] same reasoning as Normalize
\item[Bot] S-Bot
\item[Pit] S-Bot
\item[Upper] S-Trans and S-VarLeft
\item[Lower] S-Trans and S-VerRight
\item[Subst-WC] by S-Refl
\item[Subst]
$\sigma(C \cup \set{\tv{a} \doteq \type{T}}) = \sigma([\type{T}/\tv{a}]C \cup \set{\tv{a} \doteq \type{T}})$
and
$\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
\item[Subst-WC]
%Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}.
Same as Subst
\end{description}