diff --git a/constraints.tex b/constraints.tex
index 60c0508..70bed1e 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -1,4 +1,4 @@
-\section{Constraint generation}
+\section{Constraint generation}\label{chapter:constraintGeneration}
 % Our type inference algorithm is split into two parts.
 % A constraint generation step \textbf{TYPE} and a \unify{} step.
 
diff --git a/tRules.tex b/tRules.tex
index df9658c..84e3b99 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -3,21 +3,28 @@
 The input syntax for our algorithm is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
 
-The algorithm presented in this paper is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
-Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
+Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
 The input language is designed to showcase type inference involving existential types.
-We introduce the type rule T-Call which emulates a Java method call,
+Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
 where existential types are implicitly \textit{opened} and \textit{closed}.
-The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}
-and is solely used for examples.
+
+%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
+%and is solely used for examples.
+The calculus does not include method overloading or method overriding for simplicity reasons.
+Type inference for both are described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
+Our algorithm is designed for extensibility with the final goal of full support for Java.
+\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
+
+%Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
 %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
 
-The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes,
-but only by a method with the exact same type.
-The type system presented here does not allow the \textit{overriding} of methods.
-Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference
-on overriding methods, because their type is already determined.
-Allowing overriding therefore has no implication on our type inference algorithm.
+% The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes,
+% but only by a method with the exact same type.
+% The type system presented here does not allow the \textit{overriding} of methods.
+% Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference
+% on overriding methods, because their type is already determined.
+% Allowing overriding therefore has no implication on our type inference algorithm.
 
 \begin{figure}
 $