diff --git a/constraints.tex b/constraints.tex
index 9ef6c51..39d31d9 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -1,4 +1,3 @@
-
 \section{Constraint generation}
 Our type inference algorithm is split into two parts.
 A constraint generation step \textbf{TYPE} and a \unify{} step.
@@ -248,7 +247,8 @@ C = \left\{ \begin{array}{l}
 
 $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
 %TODO: Do an example where wildcards are inserted and we need capture conversion
-%\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
+
+\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
 
 % \\[1em]
 % \noindent
@@ -335,3 +335,70 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
 \section{Result Generation}
 If \unify{} returns atleast one type solution $(\Delta, \sigma)$
 the last step of the type inference algorithm is to generate a typed class.
+
+This section presents our type inference algorithm.
+The algorithm is given method assumptions $\mv\Pi$ and applied to a
+single class $\mv L$ at a time:
+\begin{gather*}
+\fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
+\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
+\quad \quad \begin{array}[t]{rll}
+  \textbf{let}\ 
+  (\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
+  \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
+                                                                     \text{// constraint generation}\\
+              {(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
+              \generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
+  \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
+  %TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
+\end{array}\\
+\textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
+\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
+\textbf{in}\ \mtypeEnvironment \cup
+\set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
+% \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
+\end{gather*}
+
+The overall algorithm is nondeterministic. The function $\unify{}$ may
+return finitely many times as there may be multiple solutions for a constraint
+set.  A local solution for class $\mv C$ may not
+be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
+local solution; if thats fail we have to backtrack further to an earlier class.
+
+% \begin{gather*}
+%   \textbf{ApplyTypes}(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
+%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
+%   \quad \quad \begin{array}[t]{rl}
+%     \textbf{let}\ 
+%     \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
+%   \end{array}\\
+%   \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
+%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
+% \end{gather*}
+
+% %TODO: Rules to create let statements
+% % Input is type solution and untyped program.
+% % Output is typed program
+% % describe conversion for each expression
+
+% Given a result $(\Delta, \sigma)$ and the type placeholders generated by $\TYPE{}$
+% we can construct a \wildFJ{} program.
+
+% %TODO: show soundness by comparing constraints and type rules
+% % untyped expression | constraints | typed expression (making use of constraints and sigma)
+% $\begin{array}{l|c|r}
+% m(x) = e & r m(p x) = e & \Delta \sigma(r) m(\sigma(p) x) = |e| \\
+% e \elvis{} e' \\
+% e.m(\ol{e}) & (e:a).m(\ol{e:p}) & a <. T, p <. T & let x : sigma(a) = e in e.m(x); %TODO
+% \end{array}$
+% \begin{displaymath}
+% \begin{array}[c]{l}
+%    \\ 
+% \hline
+% \vspace*{-0.4cm}\\
+% \wildcardEnv
+%  \vdash C \cup \, \set{ 
+%  \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
+% \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
+% \end{array}
+% \end{displaymath}
\ No newline at end of file
diff --git a/soundness.tex b/soundness.tex
index 13f4b36..db731b3 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -1,6 +1,15 @@
 \section{Soundness}
 
-
+\begin{theorem}\label{testenv-theorem}
+Type inference produces a correctly typed program.
+\begin{description}
+    \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
+    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
+    \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
+    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
+    with $\ol{M} = $
+\end{description}
+\end{theorem}
 
 % %This lemma can be used to proof Normalize rule!
 % \begin{lemma}\label{lemma:wildcardReplacement}