diff --git a/aspUnify.tex b/aspUnify.tex
index 4c6acfb..4dcd59b 100644
--- a/aspUnify.tex
+++ b/aspUnify.tex
@@ -71,7 +71,6 @@ exposing promising results.
 Another advantage is that the specification of the algorithm can be translated one on one to ASP code
 leading to less errors in the respective implementation.
 Unfortunately ASP can only be used for type inference for a subset of the Java type system that excludes wildcard types.
-%TODO: Is this correct?
 \end{abstract}
 %
 %
@@ -200,8 +199,8 @@ get either the type \texttt{C1} or \texttt{C2}.
 A first prototype implementation of the \unify{} algorithm simply created the cartesian product of all Or-Constraints,
 16 possibilities in this example, and iteratively tried all of them.
 This leads to a exponential runtime increase with every added overloaded method call.
-Eventhough the current algorithm is equipped with various optimizations as presented in \cite{plue181} and \cite{plue231},
-there is still a runtime increas sensible when dealing with many Or-Constraints.
+Eventhough the current algorithm is equipped with various optimizations as presented in \cite{plue181} and \cite{plue231}
+there are still runtime issues when dealing with many Or-Constraints.
 
 Our global type inference algorithm should construct type solutions in real time.
 Then it can effectively used as a Java compiler which can deal with large inputs of untyped Java code.
@@ -273,8 +272,8 @@ holds the desired $\sigma(\tv{a}) = \type{T}$ literals.
 
 \subsection{Unification Algorithm}\label{sec:implicationRules}
 
-The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints.
-The need to have an upper bound to every type placeholder.
+%The $\tv{a} \lessdot \type{Object}$ rule has to be ensured by the incoming constraints.
+%The need to have an upper bound to every type placeholder.
 
 All the implication rules depicted in this chapter can be translated to ASP statements
 described in chapter \ref{sec:translation}.
@@ -484,8 +483,13 @@ Fail:
 The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
 
 \section{ASP Encoding}\label{sec:translation}
+Answer Set Programming is a declarative way of formulating search problems.
+ASP statements consist of a head and a body separated by a implication operator \textquotedbl{}\texttt{:-}\textquotedbl{}:
+\texttt{head :- body}.
+This statement is interpreted as an implication rule.
+If the premises in the body are satisfied the facts stated in the head are deducted.
 \newcommand{\aspify}{\nabla}
-The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program
+The implication rules defined in chapter \ref{sec:implicationRules} are formulated in a way that can be translated to an ASP program
 (see figure \ref{fig:aspTransformationRules}).
 
 % \begin{tabular}{l | r}
@@ -505,7 +509,8 @@ The implication rules defined in chapter \ref{sec:implicationRules} can be trans
     c_1, c_2
 }{
     c
-}\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2)
+}\right) =& \aspify(c)\ \texttt{:-} \aspify(c_1), \aspify(c_2) \\
+c_1 \ || \ c_2 =& \texttt{orcons}(\aspify(c_1), \aspify(c_2))
 \end{align*}
 \caption{Transformation to ASP code}\label{fig:aspTransformationRules}
 \end{figure}
@@ -523,7 +528,13 @@ Capital letters like \texttt{X} are variables in ASP and the former statement ca
 literal like \texttt{subtype(type("C", params(tph("a"))))} to imply the literal
 \texttt{subtype(type("C", params(tph("a"))), type("D", params(tph("a"))))}.
 
+The vital part is the generation of the cartesian product of the Or-Constraints.\\
+{{\texttt{subcons(A,B); orCons(C,D) :- orCons(subcons(A,B), subcons(C,D)).}}}\\
+The operator \textquotedbl{}\texttt{;}\textquotedbl{} tells ASP to consider either the left or the right side.
+By supplying multiple Or-Constraints this way the ASP interpreter will consider all combinations, the cartesian product of the or constraints.
 
+The rules implying a failure $\emptyset$ are translated by leaving the head of the asp statement empty.
+If the body of such rules is satisfied the algorithm considers the deduction as incorrect.
 % \section{Proofs}
 % \begin{lemma}{Substitution:}
 % For every $\tv{a} \doteq \type{T}$ and every constraint $c$,