diff --git a/vortrag.tex b/vortrag.tex
index 2ecb981..a5cf70b 100644
--- a/vortrag.tex
+++ b/vortrag.tex
@@ -62,7 +62,7 @@
 		%frame=single,			% Rahmen an
 		%frameround=ffff,
 		rulecolor=\color{darkgray},	% Rahmenfarbe
-		fillcolor=\color{ListingBackground}
+		fillcolor=\color{ListingBackground},
         showtabs=false,
         %breaklines=true,
         %breakatwhitespace=true,
@@ -213,243 +213,45 @@
 
 \newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-0.5em] \ \end{array}}
 
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
-\rulename{T-Call} \\[1em]
-\begin{center}
-$\begin{array}{l}
-    \begin{array}{@{}c}
-        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
-    \end{array}
-\end{array}$
-\end{center}
-
-\textbf{Example:}
-$\generics{\type{String}}\texttt{emptyList}() : \exptype{List}{\type{String}}$
-\\[2em]
-\rulename{TI-Call} \\[1em]
-\begin{center}
-$\begin{array}{l}
-    \begin{array}{@{}c}
-        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
-    \end{array}
-\end{array}$
-\end{center}
-
-\textbf{Example:}
-$\texttt{emptyList}() : \exptype{List}{\type{String}}$
-\end{frame}
-
-
-% \begin{frame}[fragile]
-% \frametitle{Java Method Call}
-% \rulename{M-Class} \\[1em]
-% \begin{center}
-% $\begin{array}{l}
-%     \begin{array}{@{}c}
-%     \generics{\ol{X}}\ \type{T} \ \texttt{m}(\ol{T\ x}) \set{ \ldots }
-%         \\
-%         \hline
-%     \vspace*{-0.3cm}\\
-%        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T}
-%     \end{array}
-% \end{array}$
-% \end{center}
-
-% \textbf{Beispiele:}\\
-% \begin{verbatim}
-% X head(List<X> l) { ... }
-% \end{verbatim}
-% \begin{itemize}
-% \item 
-% $\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$
-% \end{itemize}
-
-% \begin{verbatim}
-% <X> List<X> emptyList() { ... }
-% \end{verbatim}
-% \begin{itemize}
-% \item 
-% $\textit{mtype}(\texttt{emptyList}) = \generics{\type{X}}\ [] \to \exptype{List}{\type{X}}$
-% \end{itemize}
-% \end{frame}
-
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
-\rulename{T-Call} \\[1em]
-\begin{center}
-$\begin{array}{l}
-    \begin{array}{@{}c}
-        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \Delta \vdash  \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta \vdash \expr{v}.\generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
-    \end{array}
-\end{array}$
-\end{center}
-\textbf{Beispiel:}\\
-\begin{verbatim}
-<X> X head(List<X> l){ ... }
-
-head(new List<String>());
-\end{verbatim}
-\pause
-$\begin{array}{l}
-    \begin{array}{@{}c}
-        \textit{mtype}(\texttt{head}) = \generics{\ol{X}}\ \exptype{List}{\type{X}} \to \type{X} \\
-        \texttt{new List<String>}() : [\type{String}/\type{X}]\exptype{List}{\type{X}}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : [\type{String}/\type{X}]\type{X}
-    \end{array}
-\end{array}$\\[1em]
-\pause
-% $\begin{array}{l}
-%     \begin{array}{@{}c}
-%         \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-%         \texttt{new List<String>}() : \exptype{List}{\type{String}}
-%         \\
-%         \hline
-%     \vspace*{-0.3cm}\\
-%         \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : \type{String}
-%     \end{array}
-% \end{array}$
-
-\begin{itemize}
-    \item \texttt{head(new List<String>()) : String}
-\end{itemize}
-\end{frame}
-
-% \begin{frame}[fragile]
-% \frametitle{Java Method Call}
-
-% \begin{verbatim}
-% head(head(emptyList()))
-% \end{verbatim}
-
-% $
-% \begin{array}[b]{c}
-% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-% \\
-% \hline
-% \texttt{head(emptyList())} : \exptype{List}{\type{String}}
-% \end{array} \rulenameAfter{T-Call}
-% $
-% \end{frame}
-
-% \begin{frame}[fragile]
-% \frametitle{Java Method Call}
-% $
-% \begin{array}[b]{c}
-% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-% \\
-% \hline
-% \generics{\exptype{List}{\exptype{List}{\type{String}}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-% \end{array} \rulenameAfter{T-Call}
-% $
-
-% $
-% \begin{array}[b]{c}
-% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-% \\
-% \hline
-% \generics{\exptype{List}{\type{String}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-% \end{array} \rulenameAfter{T-Call}
-% $
-% \end{frame}
-
-% \begin{frame}[fragile]
-% \frametitle{Java Method Call}
-
-% $
-% \begin{array}[b]{c}
-% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-% \\
-% \hline
-% \generics{\exptype{List}{\type{String}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-% \end{array} \rulenameAfter{T-Call}
-% $
-% \end{frame}
-
-% \begin{frame}[fragile]
-% \frametitle{Java Method Call}
-% $
-% \begin{array}[b]{c}
-% \begin{array}[b]{c}
-% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}}
-% \\
-% \hline
-% \texttt{emptyList().get()} : \exptype{List}{\type{String}}
-% \end{array} \rulenameAfter{T-Call}
-% \\
-% \hline
-% \texttt{emptyList().get().get()} : \type{String}
-% \end{array} \rulenameAfter{T-Call}
-% $
-% \end{frame}
-
-% \begin{frame}[fragile]
-% \frametitle{Method Call with Wildcards}
-% Eigentlich kann man mit Wildcard Typen keine Methodenaufrufe durchführen.
-% Der eigentliche Typ ist nicht bekannt.
-% ? sind auch nicht reflexiv
-% Es geht dennoch, weil sich hinter einem Wildcard Typ ein konkreter Typ verbirgt.
-% Dieser muss ausgepackt werden.
-% Die entstehende freie Typvariable kann nun als Typ benutzt werden.
-
-% \end{frame}
-
-
-\begin{frame}[fragile]
-    \frametitle{Typeinference ohne Wildcards}
-    \rulename{TI-Call} \\[1em]
-    \begin{center}
-    $\begin{array}{l}
-        \begin{array}{@{}c}
-            \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-            \Delta \vdash  \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
-            \\
-            \hline
-        \vspace*{-0.3cm}\\
-            \Delta \vdash \expr{v}.\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
-        \end{array}
-    \end{array}$
-    \end{center}
-\begin{verbatim}
-untypedMethod(l){
-    shuffle(l);
+\begin{frame}[fragile]{Global Type Inference}
+\begin{lstlisting}
+(*@\only<1>{\color{gray}\texttt{List<? extends Object>} }@*)someList(){
+    if(Math.random > 0.5){
+        return new List(*@\only<1>{\color{gray}\texttt{<String>}}@*)("String");
+    } else {
+        return new List(*@\only<1>{\color{gray}\texttt{<Integer>}}@*)(42);
+    }
 }
-\end{verbatim}
+\end{lstlisting}
+\pause
+\end{frame}
+
+\begin{frame}[fragile]{Wildcards as Existential Types}
+\begin{lstlisting}
+(*@\only<2>{\color{red}$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$ }@*)someList(){
+    if(Math.random > 0.5){
+        return new List("String");
+    } else {
+        return new List(42);
+    }
+}
+\end{lstlisting}
+\pause
 \begin{itemize}
-    \item $\lessdot $
+\item \texttt{List<? extends Object>} $\implies$ $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$
+\item \texttt{List<? super String>} $\implies$ $\wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}$
 \end{itemize}
 \end{frame}
 
 \begin{frame}[fragile]{Capture Conversion}
 \rulename{T-Call-Wildcards} \\[1em]
+\alt<-2>{
 \begin{center}
 $\begin{array}{l}
     \begin{array}{@{}c}
         \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
         \Delta \vdash  \ol{v} : \ol{\wctype{\Delta}{C}{\ol{T}}} \\
-        \overline{\exptype{C}{\ol{T}}} <: [\ol{T'}/\ol{X}]\ol{T} \quad \quad [\ol{T'}/\ol{X}]\type{T} <: \type{R}
+        \Delta, \overline{\Delta} \vdash \overline{\exptype{C}{\ol{T}}} <: [\ol{T'}/\ol{X}]\ol{T} \quad \quad \Delta, \overline{\Delta} \vdash [\ol{T'}/\ol{X}]\type{T} <: \type{R}
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -457,45 +259,35 @@ $\begin{array}{l}
     \end{array}
 \end{array}$
 \end{center}
-%Wildcard Capture
-\begin{verbatim}
-<X> List<X> shuffle(List<X> l){ ... }
-
-List<?> l;
-
-shuffle(l) : List<?>
-\end{verbatim}
-%why do we need capture constraints?
-% List<List<?>> not a subtype of List<List<X>> for any X
-
+}{
 \begin{center}
     $\begin{array}{l}
         \begin{array}{@{}c}
-            \textit{mtype}(\texttt{shuffle}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
-            \texttt{l} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \quad \quad
-            \exptype{List}{\type{A}} <: [\type{A}/\type{X}]\exptype{List}{\type{X}} \\
-            \ [\type{A}/\type{X}]\exptype{List}{\type{X}} <: \wctype{\rwildcard{A}}{List}{\rwildcard{A}}
+            \textit{mtype}(\texttt{shuffle}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \quad \quad 
+            \texttt{l} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \\
+            \wildcard{A}{\type{Object}}{\bot} \vdash \exptype{List}{\type{A}} <: [\type{A}/\type{X}]\exptype{List}{\type{X}} \quad \quad
+            \ [\type{A}/\type{X}]\exptype{List}{\type{X}} <: \wctype{\rwildcard{B}}{List}{\rwildcard{B}}
             \\
             \hline
         \vspace*{-0.3cm}\\
-            \texttt{shuffle}(\expr{l}) : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}
+            \texttt{shuffle}(\expr{l}) : \wctype{\rwildcard{B}}{List}{\rwildcard{N}}
         \end{array}
     \end{array}$
     \end{center}
-\end{frame}
-    
-\begin{frame}[fragile,t]
-%Explain why ? cannot be used as a regular type
-\begin{verbatim}
-<X> List<X> concat(List<X> l1, List<X> l2){
-    return l1.addAll(l2);
 }
+\pause
+%Wildcard Capture
+\begin{lstlisting}
+<X> List<X> shuffle(List<X> l){ ... }
 
-List<?> l1;
-List<?> l2;
+List<? extends Object> l;
+
+shuffle(l) (*@\only<3>{\color{red}\texttt{: List<? extends Object>}}@*)
+\end{lstlisting}
+%why do we need capture constraints?
+% List<List<?>> not a subtype of List<List<X>> for any X
+\pause
 
-concat(l1, l2); //Error
-\end{verbatim}
 \end{frame}
 
 \begin{frame}[fragile,t]
@@ -514,137 +306,100 @@ concat(l1, l2); //Error (würde l2 an ls anfügen!)
 \end{verbatim}
 \end{frame}
 
-\begin{frame}[fragile]
-%Wildcard Capture
+\begin{frame}[fragile,t]
+%Explain why ? cannot be used as a regular type
 \begin{verbatim}
-<X> void shuffle2D(List<List<X>> l){ 
-    //randomly exchange every element
-    // in the two dimensional list l
+<X> List<X> concat(List<X> l1, List<X> l2){
+    return l1.addAll(l2);
 }
 
-List<List<?>> l;
+List<?> l1;
+List<?> l2;
 
-shuffle2D(l); // Error
+concat(l1, l2); //Error
 \end{verbatim}
-
-$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \nless: \exptype{List}{\rwildcard{A}}$
+\pause
+\vfill
+\begin{center}
+    $\begin{array}{l}
+        \begin{array}{@{}c}
+            \textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
+            \texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \\
+            \exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad
+\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}}
+            \\
+            \hline
+        \vspace*{-0.3cm}\\
+            \texttt{shuffle}(\expr{l}) : {\color{red}\textbf{Errror}}
+        \end{array}
+    \end{array}$
+\end{center}
 \end{frame}
 
-\begin{frame}[fragile]
-    %Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
-    \frametitle{Capture Constraint}
-\begin{verbatim}
-<X> List<List<X>> shuffle2D(List<? extends List<X>> l) {...}
-
-List<List<?>> l = ...;
-shuffle2D(l); // Fehler!
-\end{verbatim}
-\begin{itemize}
-    \item hier ergibt sich ein Subtype-Constraint der keine Capture Conversion zulässt:
-    \item $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{x}}$
-    \pause
-    \item $\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{a}}) = \emptyset$
-\end{itemize}
-
-\end{frame}
-
-\begin{frame}[fragile]
-    %Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
-    \frametitle{Capture Constraint}
-\begin{verbatim}
-<X> List<List<X>> shuffle2D(List<? extends List<X>> l) {...}
-
-List<List<?>> l = ...;
-shuffle2D(l); // Fehler!
-\end{verbatim}
-\begin{itemize}
-    \item hier ergibt sich ein Subtype-Constraint der keine Capture Conversion zulässt:
-    \item $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{x}}$
-    \pause
-    \item $\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{a}}) = \emptyset$
-\end{itemize}
-
-\end{frame}
-
-\begin{frame}[fragile]
-    \frametitle{Capture Constraint}
-    $\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{a}}) = \emptyset$
-    $\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{a}}) = \set{\tv{a} \to \rwildcard{A}}$
-\end{frame}
-
-% TODO: 
-% Folie zu aktueller Stand Unify: Es gibt <. Constraints. Unify löst diese
-% Folie zu <? constraints: sie werden benötigt, weil unify während der Lösungsfindung Capture Conversion durchführen muss
-%why do we need capture constraints?
-% List<List<?>> not a subtype of List<List<X>> for any X
-
-
-
-%TODO Unify erklären
 % - es gibt die Capture Regel, welche Capture Conversion durchführt
 % - die subst-Regel, welche keine Typen mit freien Variablen in normale Typvariablen einsetzt
-\begin{frame}[fragile]{Reduce}
-    \rulename{Reduce} $
-        \begin{array}[c]{@{}ll}
-        \begin{array}[c]{l}
-            \wildcardEnv \vdash 
-            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
-            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
-          \hline
-          \vspace*{-0.4cm}\\
-          \wildcardEnv
-           \vdash C \cup \, \set{ 
-           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
-\overline{\wtv{a} \lessdot \type{U}}, \overline{\type{L} \lessdot \wtv{a}}}
-        \end{array}
-         %\quad \ol{Y} = \textit{fresh}(\ol{X})
-         \quad \begin{array}[c]{l}
-          \ol{\wtv{a}} \ \text{fresh}\\
-          %\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
-          %\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
-          %\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
-          \end{array}
-        \end{array}
-        $\\[1em]
-\begin{itemize}
-    \item \textbf{Example:}
-    $\begin{array}[t]{c}
-    \exptype{List}{\type{String}} \lessdot \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\type{A}}\\
-    \hline
-    \type{String} \doteq \wtv{a}, \wtv{a} \lessdot \type{Object}, \bot \lessdot \wtv{a}
-    \end{array}$
-\end{itemize}\\ \vfill
-\pause 
-\rulename{Capture} $
-   \begin{array}[c]{@{}ll}
-   \begin{array}[c]{l}
-       \wildcardEnv \vdash 
-       C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
-     \hline
-     \vspace*{-0.4cm}\\
-     \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
-      \vdash C \cup \, \set{  
-       [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
-   \end{array}
-    %\quad \ol{Y} = \textit{fresh}(\ol{X})
-    \quad \begin{array}[c]{l}
-     \ol{\rwildcard{C}} \ \text{fresh}\\
-     %\text{fv}(\type{T}) \neq \emptyset
-     \end{array}
-   \end{array}
-   $\\[1em]
-\begin{itemize}
-\item \textbf{Example:}
-    $\begin{array}[t]{c}
-    \wctype{\wildcard{A}{\type{U}}{\type{L}}}{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}\\
-    \hline
- \wildcard{A}{\type{U}}{\type{L}} \vdash \exptype{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}
-\\
-    \hline
-    \wildcard{A}{\type{U}}{\type{L}} \vdash \type{A} \doteq \wtv{x}
-    \end{array}$
-\end{itemize}
-\end{frame}
+% \begin{frame}[fragile]{Reduce}
+%     \rulename{Reduce} $
+%         \begin{array}[c]{@{}ll}
+%         \begin{array}[c]{l}
+%             \wildcardEnv \vdash 
+%             C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+%             \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
+%           \hline
+%           \vspace*{-0.4cm}\\
+%           \wildcardEnv
+%            \vdash C \cup \, \set{ 
+%            \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+% \overline{\wtv{a} \lessdot \type{U}}, \overline{\type{L} \lessdot \wtv{a}}}
+%         \end{array}
+%          %\quad \ol{Y} = \textit{fresh}(\ol{X})
+%          \quad \begin{array}[c]{l}
+%           \ol{\wtv{a}} \ \text{fresh}\\
+%           %\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
+%           %\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
+%           %\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+%           \end{array}
+%         \end{array}
+%         $\\[1em]
+% \begin{itemize}
+%     \item \textbf{Example:}
+%     $\begin{array}[t]{c}
+%     \exptype{List}{\type{String}} \lessdot \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\type{A}}\\
+%     \hline
+%     \type{String} \doteq \wtv{a}, \wtv{a} \lessdot \type{Object}, \bot \lessdot \wtv{a}
+%     \end{array}$
+% \end{itemize}\\ \vfill
+% \pause 
+% \rulename{Capture} $
+%    \begin{array}[c]{@{}ll}
+%    \begin{array}[c]{l}
+%        \wildcardEnv \vdash 
+%        C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
+%      \hline
+%      \vspace*{-0.4cm}\\
+%      \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
+%       \vdash C \cup \, \set{  
+%        [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
+%    \end{array}
+%     %\quad \ol{Y} = \textit{fresh}(\ol{X})
+%     \quad \begin{array}[c]{l}
+%      \ol{\rwildcard{C}} \ \text{fresh}\\
+%      %\text{fv}(\type{T}) \neq \emptyset
+%      \end{array}
+%    \end{array}
+%    $\\[1em]
+% \begin{itemize}
+% \item \textbf{Example:}
+%     $\begin{array}[t]{c}
+%     \wctype{\wildcard{A}{\type{U}}{\type{L}}}{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}\\
+%     \hline
+%  \wildcard{A}{\type{U}}{\type{L}} \vdash \exptype{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}
+% \\
+%     \hline
+%     \wildcard{A}{\type{U}}{\type{L}} \vdash \type{A} \doteq \wtv{x}
+%     \end{array}$
+% \end{itemize}
+% \end{frame}
 
 \begin{frame}[fragile]{Wildcard Creation}
     \begin{lstlisting}
@@ -735,17 +490,80 @@ $
 $
 \end{frame}
 
-\begin{frame}[fragile]
+\begin{frame}[fragile]{Reduce}
 $
 \begin{array}{l}
 \exptype{List}{String} \lessdot \highlight{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},
 \exptype{List}{Integer} \lessdot \highlight{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
-\\
-\hline
-\type{String} \doteq \wtv{x1}, \type{Integer} \doteq \wtv{x2}
 \end{array}
 \rulenameAfter{Reduce}
+$\\[1em]
+    \rulename{Reduce} $
+        \begin{array}[c]{@{}ll}
+        \begin{array}[c]{l}
+            \wildcardEnv \vdash 
+            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
+            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
+          \hline
+          \vspace*{-0.4cm}\\
+          \wildcardEnv
+           \vdash C \cup \, \set{ 
+           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+\overline{\wtv{a} \lessdot \type{U}}, \overline{\type{L} \lessdot \wtv{a}}}
+        \end{array}
+         %\quad \ol{Y} = \textit{fresh}(\ol{X})
+         \quad \begin{array}[c]{l}
+          \ol{\wtv{a}} \ \text{fresh}\\
+          %\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
+          %\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
+          %\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
+          \end{array}
+        \end{array}
+        $\\[1em]
 $
+\begin{array}{l}
+\exptype{List}{String} \lessdot {\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},
+\exptype{List}{Integer} \lessdot {\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
+\\
+\hline
+\type{String} \doteq \wtv{x1}, \wtv{x1} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x1}, \\
+\type{Integer} \doteq \wtv{x2}, \wtv{x2} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x2}
+\pause \\
+\hline
+\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},\\
+\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}
+\end{array}$
+\end{frame}
+
+\begin{frame}[fragile]
+    %Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
+    \frametitle{Wildcards are bound to Type}
+\begin{lstlisting}
+<X> List<List<X>> shuffle2D(List<List<X>> l) {...}
+
+List<List<?>> l = ...;
+shuffle2D(l); // Fehler!
+\end{lstlisting}
+
+\end{frame}
+
+\begin{frame}[fragile]
+    %Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
+    \frametitle{Wildcards are bound to Type}
+\begin{lstlisting}
+<X> List<List<X>> shuffle2D(List<List<X>> l) {...}
+
+(*@$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$@*) l = ...;
+shuffle2D(l); // Fehler!
+\end{lstlisting}
+\pause
+\vfill
+\begin{lstlisting}
+<X> List<List<X>> shuffle2D(List<List<X>> l) {...}
+
+(*@$\color{red}\wctype{\rwildcard{A}}{List}{\exptype{List}{\rwildcard{A}}}$@*) l = ...;
+shuffle2D(l); // (*@\color{red}\textbf{Correct!}@*)
+\end{lstlisting}
 \end{frame}
 
 \begin{frame}[fragile]{Wildcard Elminiation}
@@ -795,7 +613,6 @@ $
 
 \end{frame}
 
-
 \begin{frame}[fragile]{Wildcard Elminiation}
 
 \textit{Continue ...}\\
@@ -844,6 +661,47 @@ $
 $
 \end{frame}
 
+\begin{frame}[fragile]{Capture Conversion during Unify}
+\rulename{Capture} $
+   \begin{array}[c]{@{}ll}
+   \begin{array}[c]{l}
+       \wildcardEnv \vdash 
+       C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
+     \hline
+     \vspace*{-0.4cm}\\
+     \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
+      \vdash C \cup \, \set{  
+       [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
+   \end{array}
+    %\quad \ol{Y} = \textit{fresh}(\ol{X})
+    \quad \begin{array}[c]{l}
+     \ol{\rwildcard{C}} \ \text{fresh}\\
+     %\text{fv}(\type{T}) \neq \emptyset
+     \end{array}
+   \end{array}
+   $\\[1em]
+\begin{itemize}
+\item Constraints: ${\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
+{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}$
+\end{itemize}
+\pause
+\vfill
+$\begin{array}{l}
+{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
+{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}
+\pause 
+\\
+\hline
+\highlight{\wildcard{X}{\tv{u}}{\tv{l}}} \vdash \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
+{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}
+\pause
+\\
+\hline
+\wildcard{X}{\tv{u}}{\tv{l}}, \highlight{\wildcard{Y}{\tv{u}}{\tv{l}}} \vdash \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
+{\exptype{List}{\highlight{\rwildcard{Y}}}} \lessdotCC \exptype{List}{\wtv{x}}
+\end{array}$
+\end{frame}
+
 \begin{frame}[fragile]{Wildcard Elimination}
 \textit{Continue ...}\\
 $
@@ -934,9 +792,9 @@ $\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \highlight{\type{Object}} \lessdot \t
 <X> List<X> concat(List<X> l1, List<X> l2){ ... }
 (*@\color{red}\texttt{List<Object>}@*) someList(){
     if(Math.random > 0.5){
-        return new List("String");
+        return new List(*@\color{red}\texttt{<Object>}@*)("String");
     } else {
-        return new List(42);
+        return new List(*@\color{red}\texttt{<Object>}@*)(42);
     }
 }
 
@@ -946,93 +804,83 @@ concat(someList(), someList())
 
 % wieso dürfen normale Typvariablen keine freien Variablen enthalten?
 % sonst könnte man der shuffle2D Method ein 
-\begin{frame}[fragile]
-\begin{verbatim}
-    <A> List<A> shuffle(List<A> l){...}
-    <A,B> List<B> map(List<A> l, Function<A,B> f) { ... }
-    List<List<?>> l;
-    l.map((List<?> x) -> shuffle(x));
-\end{verbatim}
-$
-\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}},
-\exptype{List}{\tv{x}} \lessdot \tv{r}
-$
-\end{frame}
-\begin{frame}[fragile]
-\begin{verbatim}
-    List<List<?>> l;
-    l2 = l.map(x -> shuffle(x));
-    shuffle2D(l2);
-\end{verbatim}
+% \begin{frame}[fragile]
+% \begin{verbatim}
+%     <A> List<A> shuffle(List<A> l){...}
+%     <A,B> List<B> map(List<A> l, Function<A,B> f) { ... }
+%     List<List<?>> l;
+%     l.map((List<?> x) -> shuffle(x));
+% \end{verbatim}
+% $
+% \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}},
+% \exptype{List}{\tv{x}} \lessdot \tv{r}
+% $
+% \end{frame}
 
+\begin{frame}[fragile]{Wildcard Placeholders}
+\begin{lstlisting}
+    List<List<?>> l;
+    (*@\only<2>{\color{red}$\exptype{List}{\exptype{List}{\rwildcard{A}}}$}@*)l2 = l.map(x -> shuffle(x)(*@\only<2>{\color{red} : $\exptype{List}{\rwildcard{A}}$}@*));
+    shuffle2D(l2); (*@\only<2>{\color{red} // ERROR!}@*)
+\end{lstlisting}
+\vfill
+\textbf{Constraints:}\\
 $
 \begin{array}{l}
-\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}}, \\
-\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \tv{l2}, \\
-\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
+\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, \\
+\exptype{List}{\exptype{List}{\wtv{x}}} \lessdot \tv{l2}, \\
+\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\wtv{y}}}
 \end{array}
 $
-
+\\ \pause
+\vfill
 \begin{itemize}
     \item Falsche Lösung:
-    $
+$\color{red}\tv{l2} \doteq \exptype{List}{\exptype{List}{\rwildcard{A}}}$\\
+% $
+% \begin{array}{l}
+% \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\highlight{\rwildcard{A}}}, \\
+% \exptype{List}{\exptype{List}{\tv{x}}} \lessdot \exptype{List}{\exptype{List}{\tv{x}}},
+% \tv{r} \lessdot \tv{l2},
+% \tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
+% \end{array}
+% $
+$
 \begin{array}{l}
 \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\highlight{\rwildcard{A}}}, \\
-\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \exptype{List}{\exptype{List}{\tv{x}}},
-\tv{r} \lessdot \tv{l2},
-\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
+\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{A}}}, \\
+\exptype{List}{\exptype{List}{\rwildcard{A}}} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
 \end{array}
 $
+\pause
+\item Korrekte Lösung = $\emptyset$. Programm ist inkorrekt
 \end{itemize}
 \end{frame}
 
-\begin{frame}[fragile]{Lösung durch Unify}
-$
-\begin{array}{l}
-\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}}, \\
-\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \tv{l2}, \\
-\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
-\end{array}
-$
-
-\begin{itemize}
-    \item Falsche Lösung:
-    $
-\begin{array}{l}
-\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\highlight{\rwildcard{A}}}, \\
-\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \exptype{List}{\exptype{List}{\tv{x}}},
-\tv{r} \lessdot \tv{l2},
-\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
-\end{array}
-$
-\end{itemize}
-\end{frame}
-
-\begin{frame}[fragile]
-\begin{verbatim}
-    List<List<?>> l;
-    l2 = l.map(x -> shuffle(x));
-    shuffle2D(l2);
-\end{verbatim}
-
-$
-\begin{array}{l}
-\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}}, \\
-\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \tv{r},
-\tv{r} \lessdot \tv{l2},
-\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
-\end{array}
-$
-\end{frame}
-
-% könnte es nicht well-formed typen geben, wenn man beliebige substitutionen zulässt?
-% (brauchen wir die wildcard-TVs überhaupt? es wird eigentlich nur für den Soundness-Beweis gebraucht)
-
 \begin{frame}[fragile]{Conclusion}
 \begin{itemize}
+\item Wildcard creation at $\type{T} \lessdot \tv{a}$ constraints
+\begin{itemize}
+\item Wildcards are bound to a type
+\end{itemize}
+\pause
 \item Eliminate Wildcards by setting upper = lower bound
+\begin{itemize}
 \item Removes Wildcards without backtracking
 \end{itemize}
+\pause
+\item Capture Constraints for Capture Conversion during \unify{}
+\pause
+\item Wildcard Type Placeholders to keep free variables in scope
+\pause
+\vfill
+\item \unify{} is Sound
+\begin{itemize}
+\pause
+\item (but no completeness proof yet)
+\end{itemize}
+\end{itemize}
+
 \end{frame}
 
 \end{document}