diff --git a/conclusion.tex b/conclusion.tex
index 7fbd2de..6561e2e 100644
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,4 +1,6 @@
 \section{Properties of the Algorithm}
+
+%TODO: how are the challenges solved: Describe this in the last chapter with examples!
 \section{Soundness}\label{sec:soundness}
 
 \section{Completeness}\label{sec:completeness}
diff --git a/constraints.tex b/constraints.tex
index 7d2b72e..8f35764 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -42,11 +42,6 @@ We preemptively enclose every expression in a let statement before using it as a
 % Even variables have to be catched by a let statement first.
 % This behaviour emulates Java's implicit capture conversion.
 
-
-%TODO: how are the challenges solved:
-The \unify{} algorithm only sees the constraints with no information about the program they originated from.
-
-
 \subsection{ANF transformation}\label{sec:anfTransformation}
 \newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
 %https://en.wikipedia.org/wiki/A-normal_form)
@@ -118,6 +113,7 @@ The parameter types given to a generic method also affect their return type.
 During constraint generation the algorithm does not know the parameter types yet.
 We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
 $\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
+% TODO: Challenge examples!
 
 At points where a well-formed type is needed we use a normal type placeholder.
 Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
@@ -167,9 +163,18 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
     \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
                                                        assumption}\\
     \mtypeEnvironment & ::= \overline{\methodAssumption} &
-                & \text{method type environment} \\
-    \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
+                & \text{method type environment}
   \end{align*}
+\begin{tabular}{lcll}
+    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
+    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
+    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
+    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
+    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
+    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
+    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
+\end{tabular}
   \caption{Syntax of constraints and type assumptions}
   \label{fig:syntax-constraints}
 \end{figure}
diff --git a/introduction.tex b/introduction.tex
index 02295bd..9c95e50 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -345,8 +345,8 @@ let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) =
 %Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
 
 The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
-First \fjtype{} generates constraints
-and afterwards \unify{} computes a solution for the given constraint set.
+First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
+and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
 Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
 \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
 A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
diff --git a/prolog.tex b/prolog.tex
index 7ada4f5..5038afa 100755
--- a/prolog.tex
+++ b/prolog.tex
@@ -102,6 +102,7 @@
 \newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
 \newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
+\newcommand{\gtype}[1]{\type{#1}}
 \newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\anyType}[1]{\mathit{#1}}
 \newcommand{\gType}[1]{\texttt{#1}}
diff --git a/tRules.tex b/tRules.tex
index 4cb2230..8da4174 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -370,7 +370,7 @@ $\begin{array}{l}
         %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\
         \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
         \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
-        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C}
+        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
         \\
         \hline
     \vspace*{-0.3cm}\\
diff --git a/unify.tex b/unify.tex
index 86e72f4..893a0a7 100644
--- a/unify.tex
+++ b/unify.tex
@@ -276,7 +276,6 @@ The normal type placeholder $\ntv{r}$ has to be replaced by a type without free
 
 \subsection{Algorithm}
 
-\newcommand{\gtype}[1]{\type{#1}}
 %\newcommand{\tw}[1]{\tv{#1}_?}
 \begin{description}
   \item[Input:] An environment $\Delta'$