diff --git a/prolog.tex b/prolog.tex
index af553a4..53d8271 100755
--- a/prolog.tex
+++ b/prolog.tex
@@ -121,8 +121,8 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
-%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
-\newcommand{\ntv}[1]{\tv{#1}}
+\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+%\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}
diff --git a/unify.tex b/unify.tex
index 8405932..ad8bd48 100644
--- a/unify.tex
+++ b/unify.tex
@@ -146,21 +146,28 @@ The \unify{} algorithm internally uses the following data types:
 The algorithm is split into multiple parts:
 \begin{description}
 \item[Step 1:]
-Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively.
-Starting with the \rulename{circle} rule.
+Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively,
+starting with the \rulename{circle} rule.
 
 \item[Step 2:]
 %If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
 %resume with step 4.
 
-The rules in figure \ref{fig:step2-rules} offer multiple possibilities to deal with constraints of the form $\type{N} \lessdot \tv{a}$.
-This builds a search tree over multiple possible solutions.
-\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
+The second step is nondeterministic.
+%\unify{} has to pick the right transformation for each constraint of the form $\type{N} \lessdot \tv{a}$.
+%The rules in figure \ref{fig:step2-rules} offer three possibilities to deal with constraints $\type{N} \lessdot \tv{a}$.
+For every $\type{T} \lessdot \tv{a}$ constraint \unify{} has to pick exactly one transformation from figure \ref{fig:step2-rules}.
+The same principle goes for constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$ and the two transformations in figure \ref{fig:step2-rules2}.
+%They have to be applied until the constraint set holds no constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$.
+If atleast one transformation was applied in this step revert to step 1.
+Otherwise proceed with step 3.
+%This builds a search tree over multiple possible solutions.
+%\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
 
-$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
+%$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
 
 \item[Step 3:]
-We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 4.
+Apply the rules in figure \ref{fig:cleanup-rules} exhaustively and move on with step 4.
 
 \item[Step 4:] \textit{(Generating Result)} 
 Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
@@ -263,6 +270,12 @@ To only rename the respective wildcards the reduce rule renames wildcards up to
 \item[Free Variables:]
 The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
 % TODO: describe a function which determines free variables? or do an example?
+\begin{align*}
+\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
+\text{fv}(\ntv{a}) &= \emptyset \\
+\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
+\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
+\end{align*}
 
 \item[Fresh Wildcards:]
 $\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
@@ -445,11 +458,11 @@ $
     \hline
     \vspace*{-0.4cm}\\
     \wildcardEnv \vdash C 
-    \end{array}
+    \end{array} 
     $
-    \\\\
+    \quad
     \rulename{Pit}
-    & $
+    $
     \begin{array}[c]{l}
     \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ 
     \hline
@@ -530,10 +543,7 @@ $
         \vspace*{-0.4cm}\\
         \wildcardEnv \vdash C
     \end{array}
-    $
-    \\\\
-    \rulename{Erase}
-    & $
+    \quad
     \begin{array}[c]{l}
         \wildcardEnv \vdash C \cup \, \set{ \type{T} \lessdot \type{T} } \\ 
         \hline
@@ -970,7 +980,7 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
 }
     \end{center}
   \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
-  \label{fig:step2-rules}
+  \label{fig:step2-rules2}
   \end{figure}
 
 \begin{figure}