diff --git a/constraints.tex b/constraints.tex
index 1ac1330..2d1917d 100644
--- a/constraints.tex
+++ b/constraints.tex
@@ -64,12 +64,10 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
     \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
     \type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\
     % Constraints
-    \simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
-    \orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
-    \constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
+    \constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
     \consSet &::= \set{\constraints} && \text{constraint set}\\
     % Method assumptions:
-    \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y}
+    \methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
                         \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
                                                                 \text{method
                                                                 type assumption}\\
@@ -79,7 +77,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
                 & \text{method type environment} \\
     \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
   \end{align*}
-  \caption{Syntax of constraints and type assumptions.}
+  \caption{Syntax of constraints and type assumptions}
   \label{fig:syntax-constraints}
 \end{figure}
 
@@ -141,6 +139,23 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 % <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
 % \end{verbatim}
 
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\
+                & \begin{array}{ll}
+                    \textbf{let} 
+                    & \tv{e} \ \text{fresh} \\
+                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\
+                    & \constraint =
+                      \set{
+                      \tv{e} \lessdotCC \tv{x} 
+                      }\\
+                    {\mathbf{in}} & {
+                    \consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}})
+                  \end{array} 
+  \end{array}
+\end{displaymath}
+
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
     \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
@@ -168,6 +183,24 @@ The set of method assumptions returned by the \textit{mtypes} function is used t
 
 There are two kinds of method calls.
 The ones to already typed methods and calls to untyped methods.
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+      \typeExpr{}' & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
+      & \begin{array}{ll}
+      \textbf{let}
+      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
+      & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
+                    \ol{S} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, 
+                    \ol{Y} \lessdot \ol{N} }\\
+      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
+      & \mathbf{where}\ \begin{array}[t]{l}
+        \expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
+        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
+      \end{array}
+                    
+      \end{array}
+      \end{array}
+  \end{displaymath}
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
diff --git a/introduction.tex b/introduction.tex
index fb61751..35f6527 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -521,19 +521,34 @@ The \unify{} algorithm only sees the constraints with no information about the p
 The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
 
 \subsection{ANF transformation}
-The input is transformed to A-normal form.
 %TODO: describe ANF syntax (which is different then the one from the wiki: https://en.wikipedia.org/wiki/A-normal_form)
+The input is a \letfj{} program without \texttt{let} statements, which is then transformed to A-normal form \cite{aNormalForm}
+before getting processed by \fjtype{}.
 
 $
-\begin{array}{lrcl}
+\begin{array}{lrcl|l}
 \hline
-\text{Terms} & t & ::= & v \\
-& & \ \ | & \texttt{let}\ x = v \ \texttt{in}\ x.f\\
-& & \ \ | & \texttt{let}\ x_1 = v \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{v} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})\\
-& & \ \ | & t \elvis{} t\\
-\text{Var} & v & ::= & \expr{x} \\
-& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
-\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+& & & \textbf{\letfj{}} & \textbf{A-Normal form}  \\
+\text{Terms} & t & ::=
+& \expr{x}
+& \expr{x}
+\\
+& & \ \ |
+& \texttt{new} \ \type{C}(\overline{t})
+& \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
+\\
+& & \ \ |
+& t.f
+& \texttt{let}\ x = t \ \texttt{in}\ x.f
+\\
+& & \ \ | 
+& t.\texttt{m}(\overline{t})
+& \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{v} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
+\\
+& & \ \ | 
+& t \elvis{} t
+& t \elvis{} t\\
+%
 \hline
 \end{array}
 $
diff --git a/martin.bib b/martin.bib
index eea0ad2..9fdee01 100644
--- a/martin.bib
+++ b/martin.bib
@@ -456,3 +456,13 @@ keywords = {Compilation, Java, generic classes, language design, language semant
   year={1996}
 }
 
+@article{aNormalForm,
+  title={Reasoning about programs in continuation-passing style.},
+  author={Sabry, Amr and Felleisen, Matthias},
+  journal={ACM SIGPLAN Lisp Pointers},
+  number={1},
+  pages={288--298},
+  year={1992},
+  publisher={ACM New York, NY, USA}
+}
+
diff --git a/tRules.tex b/tRules.tex
index 9428d96..0020181 100644
--- a/tRules.tex
+++ b/tRules.tex
@@ -196,72 +196,98 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Field}\\
     \begin{array}{@{}c}
-        \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
-        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+        \Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad 
+        \Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad
         \textit{fields}(\type{N}) = \ol{U\ f} \\
-\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
-\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
-        \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i
     \end{array}
 \end{array}$
 \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-Field}\\
+%     \begin{array}{@{}c}
+%         \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
+%         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+%         \textit{fields}(\type{N}) = \ol{U\ f} \\
+% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-New}\\
+%     \begin{array}{@{}c}
+%         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
+%         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+%         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+%         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+%         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
+%         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
+%         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+%     \end{array}
+% \end{array}$
+% \\[1em] 
 $\begin{array}{l}
     \typerule{T-New}\\
     \begin{array}{@{}c}
         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
-        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
-        \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
-        \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
-        \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
-        \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
-        \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
+        \Delta \vdash  \overline{\type{S}} <: \overline{\type{U}} \\
+        \Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad
+        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} 
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}}
     \end{array}
 \end{array}$
-\\[1em] 
-$\begin{array}{l}
-    \typerule{T-Call}\\
-    \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
-        \\
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
-        \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
-        \\
-        \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
-        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
-    \end{array}
-\end{array}$
-\\[1em]
+\hfill
+% $\begin{array}{l}
+%     \typerule{T-Call}\\
+%     \begin{array}{@{}c}
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+%         \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+%         \\
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+%         \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
+%         \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
+%         \\
+%         \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+%         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
 $\begin{array}{l}
     \typerule{T-Call}\\
     \begin{array}{@{}c}
         \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+        \Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
         \\
         \Delta \vdash \ol{S} \ \ok \quad \quad
-        \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
+        \Delta | \Gamma \vdash  \expr{v}, \ol{v} : \ol{T} \quad \quad
         \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} 
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
@@ -278,7 +304,7 @@ $\begin{array}{l}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{let} \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T}
+        \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
@@ -368,4 +394,5 @@ $\begin{array}{l}
         \text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
     \end{array}
 \end{array}$
+\caption{Field access}
 \end{figure}
\ No newline at end of file