diff --git a/report/report.tex b/report/report.tex
index 082d026..ecd3608 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -23,7 +23,7 @@
 \setlength{\textheight}{680pt}
 \pagestyle{fancy}
 \fancyhf{}
-\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - ProVerif}
+\fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - \fstar}
 \fancyhead[C]{}
 \fancyhead[R]{Group \groupnumber}
 \renewcommand{\headrulewidth}{0.4pt}
@@ -116,7 +116,7 @@ It is allowed to reduce \texttt{step\_simp te cs} to \texttt{cs}, because
 \texttt{cs} is already final.
 
 Now it is possible to prove the lemma \texttt{progress}: \texttt{cs ==
-step\_simp te cs} $\rightarrow$ \texttt{isFinal cs}. Since, \texttt{step\_simp}
+step\_simp te cs} $\rightarrow$ \texttt{isFinal cs}. Since \texttt{step\_simp}
 has the same value as the \texttt{step} function, when the outcome is
 \texttt{Next}, the call stack is different from \texttt{cs}. This means that the
 left side of the lemma does not hold and therefore the right side does not have
@@ -135,17 +135,59 @@ equality and therefore propositional equality is needed.
 \section{Uniqueness of call stacks}
 
 \paragraph{Paper proofs}
-%TODO
 
-\paragraph{Explanation on lemma \texttt{order\_ineq}}
+Note: The previously defined measure is written as \texttt{|cs|}, where
+\texttt{cs} is a call stack.
+
+To prove \texttt{order\_decreases} it needs to be shown that from \texttt{nsteps
+n te cs == cs'} and $n > 0$ follows \texttt{|cs'| << |cs|} for all
+$n\in\mathbb{N}$. The proof is by induction on \texttt{n}. For \texttt{n = 1},
+\texttt{nsteps 1 te cs} is equal to \texttt{step\_simp te cs}. Similarly to
+Exercise 2.2 it follows that the hypothesis holds, because \texttt{cs} is not a
+final state. After that, the induction step is \texttt{nsteps (n+1) te cs ==
+cs'}, which can be rewritten as \texttt{nsteps n te (step\_simp te cs) == cs'}
+(definition of \texttt{nsteps}). With the reasoning from the base case where
+\texttt{n = 1}, it follows that \texttt{|step\_simp te cs| << |cs|}. Now there
+are two cases: either the call stack \texttt{|step\_simp te cs} is final or not.
+For the first case, the lemma \texttt{nsteps\_stop} can be used to derive
+\texttt{step\_simp te cs == cs'} from \texttt{nsteps n te (step\_simp te cs) ==
+cs'}, where \texttt{|step\_simp te cs| << |cs|} holds. For the second case, we
+simply take the induction hypothesis to conclude that the induction holds.
+
+Taking the previous proof, for \texttt{callstacks\_unique} it is evident that
+\texttt{|cs'| << |cs|} holds. It follows that \texttt{cs'} $\neq$ \texttt{cs} by
+proof of contradiction: Assuming that \texttt{cs' == cs} and \texttt{|cs'| <<
+|cs|} is true, it would require that the top constant in both lists
+\texttt{LexTop} satisfies \texttt{LexTop << LexTop}. Since this is impossible,
+it contradicts the assumption and therefore it follows that \texttt{cs'} $\neq$
+\texttt{cs}.
 
 \section{Exception Propagation}
 
 \paragraph{Paper proof}
-%TODO
 
-\paragraph{Explanation on alternative formulations}
-%TODO
+Proof by induction:
+
+\begin{verbatim}
+length ps = 0
+
+nsteps (2 * (length [])) te (Ter ExcState []) == (Ter ExcState [])
+nsteps 0 te (Ter ExcState []) == (Ter ExcState [])
+(Ter ExcState []) == (Ter ExcState [])
+\end{verbatim}
+
+\begin{verbatim}
+length ps to (length ps) + 1
+
+nsteps (2 * (length ps)) te (Ter ExcState ps) == (Ter ExcState [])
+nsteps ((2 * (length ps)) - 1) te (step simp (Ter ExcState ps)) == (Ter ExcState [])
+nsteps ((2 * (length ps)) - 1) te (Exec (apply returneffects ts s)::ps’) == (Ter ExcState [])
+nsteps ((2 * (length ps)) - 1) te (Exec s’::ps’) == (Ter ExcState [])
+nsteps ((2 * (length ps)) - 2) te (step simp (Exec s’::ps’)) == (Ter ExcState [])
+nsteps ((2 * (length ps)) - 2) te (Ter (ExcState ps’)) == (Ter ExcState [])
+nsteps (2 * ((length ps) - 1)) te (Ter (ExcState ps’)) == (Ter ExcState [])
+nsteps (2 * (length ps’)) te (Ter (ExcState ps’)) == (Ter ExcState [])
+\end{verbatim}
 
 \end{document}