diff --git a/introduction.tex b/introduction.tex
index f64f041..6ac1ebe 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -12,29 +12,29 @@
 
 \section{Global Type Inference}
 Java already provides type inference in a restricted form namely local type inference.
-It takes a vital role in method invocations
-by determining type parameters.
-%TODO: Explain Java needs it for capture conversion
-
-Java already uses type inference when it comes to method invocations, local variables or lambda expressions.
-The crucial part for all of this use cases is the surrounding context.
-The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference
-because the expected return type is known. \texttt{List<String>} in this case.
-\begin{lstlisting}[caption=Extract of a valid Java program]
+But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all.
+We will show the different capabilities with an example.
+In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing
+its type parameters.
+Java will infer \texttt{String} for the parameter \texttt{T} by using the type annotations
+\texttt{List<String>} on the left side of the assignment and a matching algorithm \cite{javaTIisBroken}.
+%The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference
+%because the expected return type is known. \texttt{List<String>} in this case.
+\begin{lstlisting}[caption=Extract of a valid Java program, label=lst:tiExample]
 <T> List<T> emptyList() { ... }
 
 List<String> ls = emptyList();
 \end{lstlisting}
 
-Local type inference is based on matching and not unification \cite{javaTIisBroken}.
+%\textit{Local Type Inference limitations:}
 When calling the \texttt{emptyList} method without context its return value will be set to a \texttt{List<Object>}.
-The following Java code snippet is incorrect, because \texttt{emptyList()} returns
+The Java code snippet in \ref{lst:tiLimit} is incorrect, because \texttt{emptyList()} returns
 a \texttt{List<Object>} instead of the required $\exptype{List}{\exptype{List}{String}}$.
-\begin{verbatim}
+\begin{lstlisting}[caption=Limitations of Java's Type Inference, label=lst:tiLimit]
 emptyList().add(new List<String>())
     .get(0)
     .get(0);
-\end{verbatim}
+\end{lstlisting}
 %List<String> <. A
 %List<A> <: List<B>, B <: List<C> 
 % B = A and therefore A on the left and right side of constraints.
@@ -45,34 +45,36 @@ but the second call to \texttt{get} is only possible if \texttt{emptyList} retur
 a list of lists.
 The local type inference algorithm based on matching cannot produce this solution.
 Here a type inference algorithm based on unification is needed.
-\begin{verbatim}
-this.<List<String>>emptyList().add(new List<String>())
-    .get(0)
-    .get(0);
-\end{verbatim}
+% \begin{verbatim}
+% this.<List<String>>emptyList().add(new List<String>())
+%     .get(0)
+%     .get(0);
+% \end{verbatim}
 
-$
-\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}
-\quad  \generics{\type{X}}\exptype{List}{\type{X}} \to \type{X} \in \mtypeEnvironment{}(\texttt{get})1
-\\
-\hline
-\texttt{emptyList().get().get()} : \type{String}
-\end{array} \rulenameAfter{T-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}
+% \quad  \generics{\type{X}}\exptype{List}{\type{X}} \to \type{X} \in \mtypeEnvironment{}(\texttt{get})1
+% \\
+% \hline
+% \texttt{emptyList().get().get()} : \type{String}
+% \end{array} \rulenameAfter{T-Call}
+% $
 
 %motivate constraints: 
-To solve this example we will create constraints
+To solve this example our Type Inference algorithm will create constraints
 $
 \exptype{List}{\tv{a}} \lessdot \tv{b},
 \tv{b} \lessdot \exptype{List}{\tv{c}},
 \tv{c} \lessdot \exptype{List}{\tv{d}}
-$ TODO
+$
+
+TODO
 Local type inference \cite{javaTIisBroken} is able to find a type substitution $\sigma$ satisfying
 $\overline{\type{A} <: \sigma(\type{F}) }, \sigma(\type{R}) <: \type{E}$.
 It is important that $\overline{\type{A}}$ and $\type{E}$ are given types and do not contain