diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf
index fb7454c..6cb8712 100644
Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ
diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex
index 908fb68..97f6557 100644
--- a/semester4/fmfp/formal-methods-functional-programming-summary.tex
+++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex
@@ -5,6 +5,7 @@
 \usepackage{lmodern}
 \usepackage{ebproof}
 \usepackage{overarrows}
+\usepackage{bm}
 
 \NewOverArrowCommand{\overrightharpoon}{%
     end=\rightharpoonup
@@ -114,7 +115,6 @@
 \input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/05_unfolding-loops.tex}
 \input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/06_deterministic-semantics.tex}
 \input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/07_extensions-of-imp.tex}
-% \input{parts/03_language-semantics/01_operational-semantics/00_big-step-semantics/}
 \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/00_structural-operational-semantics.tex}
 \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/01_rules.tex}
 \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/02_multi-step-derivation-seq.tex}
@@ -122,9 +122,13 @@
 \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/04_proofs.tex}
 \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/05_semantic-equivalence.tex}
 \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/06_extensions.tex}
-% \input{parts/03_language-semantics/01_operational-semantics/01_small-step-semantics/}
 \input{parts/03_language-semantics/01_operational-semantics/02_equiv.tex}
-% \input{parts/03_language-semantics/01_operational-semantics/}
+\input{parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex}
+\input{parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex}
+\input{parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex}
+\input{parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex}
+\input{parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex}
+\input{parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex}
 % \input{parts/03_language-semantics/}
 
 
diff --git a/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex
new file mode 100644
index 0000000..2143887
--- /dev/null
+++ b/semester4/fmfp/parts/03_language-semantics/01_operational-semantics/03_rules-summary.tex
@@ -0,0 +1,184 @@
+\newpage
+\subsubsection{Operational Semantics Rules Overview}
+\paragraph{Big-Step Semantics}
+\[
+    \begin{prooftree}
+        \infer0[\textsc{Skip}$_{NS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow \sigma}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
+        \hypo{\langle s', \sigma' \rangle \rightarrow \sigma''}
+        \infer2[\textsc{Seq}$_{NS}$]{\langle s;s', \sigma \rangle \rightarrow \sigma''}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
+        \infer1[\textsc{IfT}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
+        \infer1[\textsc{IfF}$_{NS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow \sigma'}
+    \end{prooftree}
+\]
+
+\begin{align*}
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
+        \hypo{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma' \rangle \rightarrow \sigma''}
+        \infer2[\textsc{WhT}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma''}
+    \end{prooftree}
+     &  &
+    \begin{prooftree}
+        \infer0[\textsc{WhF}$_{NS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow \sigma}
+    \end{prooftree} \\
+    \text{if }
+    \cB\llbracket b \rrbracket \sigma = \texttt{tt}
+     &  &
+    \text{if }
+    \cB\llbracket b \rrbracket \sigma = \texttt{ff}
+\end{align*}
+
+\[
+    \begin{prooftree}
+        \infer0[\textsc{Ass}$_{NS}$]{\langle x := e, \sigma \rangle \rightarrow \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma]}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[\textsc{Ass}$_{NS}$]{\langle v := v + 1, \sigma_\text{zero} \rangle \rightarrow \sigma[v \mapsto \cA\llbracket v + 1 \rrbracket \sigma_\text{zero}]}
+    \end{prooftree}
+\]
+
+\paragraph{Small-Step Semantics}
+\[
+    \begin{prooftree}
+        \infer0[\textsc{Skip}$_{SOS}$]{\langle \texttt{skip}, \sigma \rangle \rightarrow_1 \sigma}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[\textsc{Ass}$_{SOS}$]{\langle x := e, \sigma \rangle \rightarrow_1 \sigma[x \mapsto \cA\llbracket e \rrbracket \sigma ]}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
+        \infer1[\textsc{Seq1}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s', \sigma' \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
+        \infer1[\textsc{Seq2}$_{SOS}$]{\langle s;s', \sigma \rangle \rightarrow_1 \langle s'';s', \sigma' \rangle}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \infer0[\textsc{IfT}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[\textsc{IfF}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
+        \infer1[\textsc{IfT1}$_{SOS}$]{\langle \texttt{if}\; b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \sigma'}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
+        \infer1[\textsc{IfT2}$_{SOS}$]{\langle \texttt{if}\;b \; \texttt{then} \; s \; \texttt{else} \; s' \; \texttt{end}, \sigma \rangle \rightarrow_1 \langle s''', \sigma' \rangle}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \infer0[\textsc{While}$_{SOS}$]{\langle \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end}, \sigma \rangle \rightarrow_1
+            \langle \texttt{if} \; b \; \texttt{then} \; s; \; \texttt{while} \; b \; \texttt{do} \; s \; \texttt{end else skip end}, \sigma \rangle}
+    \end{prooftree}
+\]
+
+\paragraph{Extensions}
+\subparagraph{Big-Step Semantics}
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle \rightarrow \sigma' }
+        \infer1[\textsc{Loc}$_{NS}$]{\langle \texttt{var x := e in s end}, \sigma \rangle \rightarrow \sigma'[x \mapsto \sigma(x)]}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s, \sigma_\text{zero}[\overrightharpoon{x_i} \mapsto \overrightharpoon{\cA \llbracket e_i \rrbracket \sigma}]
+            [\overrightharpoon{y_j} \mapsto \overrightharpoon{\sigma(z_j)}] \rangle \rightarrow \sigma'}
+        \infer1[\textsc{Call}$_{NS}$]{\langle p(\overrightharpoon{e_i}; \overrightharpoon{z_j}), \sigma \rangle
+            \rightarrow \sigma[\overrightharpoon{z_j} \mapsto \overrightharpoon{\sigma'(y_j)}]}
+    \end{prooftree}
+\]
+
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow \sigma'}
+        \infer1[\textsc{ND1}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s', \sigma \rangle \rightarrow \sigma'}
+        \infer1[\textsc{ND2}$_{NS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow \sigma'}
+    \end{prooftree}
+\]
+
+
+\subparagraph{Small-Step Semantics}
+\[
+    \begin{prooftree}
+        \infer0[\textsc{Loc}$_{SOS}$]{\langle \texttt{var x:= e in s end}, \sigma \rangle \rightarrow_1 \langle \texttt{s;restore }(x, \sigma(x)),
+            \sigma[x \mapsto \cA \llbracket e \rrbracket \sigma] \rangle}
+    \end{prooftree}
+\]
+\[
+    \begin{prooftree}
+        \infer0[\textsc{Ret}$_{SOS}$]{\langle \texttt{restore }(x, \sigma(x)), \sigma \rangle \rightarrow_1 \sigma[x \mapsto v]}
+    \end{prooftree}
+\]
+\[
+    \begin{prooftree}
+        \infer0[\textsc{ND1}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma \rangle}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[\textsc{ND2}$_{SOS}$]{\langle s \bigbox s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle}
+    \end{prooftree}
+\]
+\[
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
+        \infer1[\textsc{Par1}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s'' \texttt{ par } s', \sigma' \rangle}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s, \sigma \rangle \rightarrow_1 \sigma'}
+        \infer1[\textsc{Par2}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s', \sigma' \rangle}
+    \end{prooftree}
+\]
+\[
+    \begin{prooftree}
+        \hypo{\langle s', \sigma \rangle \rightarrow_1 \langle s'', \sigma' \rangle}
+        \infer1[\textsc{Par3}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s \texttt{ par } s'', \sigma' \rangle}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\langle s', \sigma \rangle \rightarrow_1 \sigma'}
+        \infer1[\textsc{Par4}$_{SOS}$]{\langle s \texttt{ par } s', \sigma \rangle \rightarrow_1 \langle s, \sigma' \rangle}
+    \end{prooftree}
+\]
diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex
new file mode 100644
index 0000000..ecb15a4
--- /dev/null
+++ b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/00_intro.tex
@@ -0,0 +1,45 @@
+\newpage
+\subsection{Axiomatic Semantics}
+\subsubsection{Program Correctness}
+\inlinedefinition[Partial Correctness] \textit{if} a program terminates \textit{then} there will be a certain relationship between the initial and final state
+
+\inlinedefinition[Total Correctness] Program terminates \textit{and} is partially correct, i.e.\\
+\texttt{total correctness = partial correctness + termination}
+
+\inlinedefinition[Formal Specification] is used to expressed the aforementioned relationship between the initial and final state.
+It does not include guarantees for termination and can thus only be used to provide a starting point for a prove of partial correctness.
+
+We typically express \bi{Formal Specifications} using Small- or Big-Step semantics.
+
+\inlineexample Consider the factorial statement
+\begin{code}{text}
+    y := 1;
+    while not x = 1 do
+        y := y * x;
+        x := x - 1
+    end
+\end{code}
+The specification that we want to prove is here given by ``The final value of \texttt{y} is the factorial of the initial value \texttt{x}''.
+Do note that this statement is only partially correct, as it does not terminate for $x < 1$.
+
+We can express the specification formally as follows using big-step semantics:
+\[
+    \forall \sigma, \sigma'. \vdash \langle y := 1; \texttt{while not x = 1 do y := y * x; x := x - 1 end}, \sigma \rangle \rightarrow \sigma' 
+    \implies \sigma'(\texttt{y}) = \sigma(\texttt{x})! \land \sigma(\texttt{x}) > 0
+\]
+
+% We then prove the partial correctness in three steps:
+%
+% \bi{Step 1}: The body of the loop
+% \[
+%     \forall \sigma, \sigma''. \vdash \langle \texttt{y := y * x; x := x - 1}, \sigma \rangle \rightarrow \sigma'' \land \sigma''(\texttt{x}) > 0
+%     \implies \sigma(\texttt{y}) \times \sigma(\texttt{x})! = \sigma''(\texttt{y}) \times \sigma''(\texttt{x})! \land \sigma(\texttt{x}) > 0
+% \]
+%
+% \bi{Step 2}: The loop satisfies
+% \[
+%     \forall \sigma, \sigma''. \vdash \langle \texttt{y := y * x; x := x - 1}, \sigma \rangle \rightarrow \sigma'' \land \sigma''(\texttt{x}) > 0
+%     \implies \sigma(\texttt{y}) \times \sigma(\texttt{x})! = \sigma''(\texttt{y}) \times \sigma''(\texttt{x})! \land \sigma(\texttt{x}) > 0
+% \]
+Since these kinds of proofs take a lot of effort and get very complicated rather quickly, axiomatic semantics provide a nice and fast way of proving correctness,
+because we can focus on the essential properties.
diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex
new file mode 100644
index 0000000..8ffd66f
--- /dev/null
+++ b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/00_triples-assertions.tex
@@ -0,0 +1,17 @@
+\newpage
+\subsubsection{Hoare Logic}
+\paragraph{Hoare Triples}
+\inlinedefinition Properties are specified as \bi{Hoare Triples} $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$, with statement $s$, $\bm{P}$ the precondition and $\bm{Q}$ the postcondition.
+Here, $\bm{P}, \bm{Q}$ are assertions and are, together with $\bm{R}$, meta-variables over assertions.
+
+\inlinedefinition[Logical Variables] To keep the original value of a variable, we can ``reassign'' values in the precondition
+(e.g. $x = N$ to then in the postcondition state something regarding $N$).
+
+Pre- and Postconditions are assertions, i.e. they are boolean expressions plus logical variables.
+Often, quantification is used in assertions as well in practice, as well as other expressions such as $x!$ when it is convenient and we also assume that the \bi{substitution lemma}
+still holds:
+\[
+    \cB \llbracket \bm{P}[x \mapsto e] \rrbracket \sigma = \cB \llbracket \bm{P} \rrbracket \sigma [x \mapsto \cA \llbracket e \rrbracket \sigma]
+\]
+
+We use $P_1 \land P_2$ instead of $P_1 \texttt{and} P_2$, $P_1 \lor P_2$ instead of $P_1 \texttt{or} P_2$ and $\neg P$ instead of $\texttt{not} P$
diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex
new file mode 100644
index 0000000..6f42df8
--- /dev/null
+++ b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/01_derivation-systems.tex
@@ -0,0 +1,78 @@
+\paragraph{Derivation Systems}
+We again use derivation trees, where their rules specify which triples can be derived for each statement.
+The premises and conclusions of the derivation rules are Hoare Triples.
+
+Again, we write $\vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \}$ if there exists a (finite) derivation tree ending in $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$, and
+\[
+    \vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \} \Leftrightarrow \exists T. \texttt{root}(T) \equiv \{ \bm{P} \} \ s \ \{ \bm{Q} \}
+\]
+
+
+\subparagraph{The rules}
+\[
+    \begin{prooftree}
+        \infer0[$\textsc{Skip}_{Ax}$]{\{ \bm{P} \} \ \texttt{skip} \ \{ \bm{P} \}}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \infer0[$\textsc{Ass}_{Ax}$]{\{ \bm{P}[x \mapsto e] \} \ \texttt{x := e} \ \{ \bm{P} \}}
+    \end{prooftree}
+\]
+
+Sequential Composition \texttt{s;s'}, loop (\texttt{while b do s end}) and conditional statements (\texttt{if b then s1 else s2 end})
+\[
+    \begin{prooftree}
+        \hypo{\{ \bm{P} \} \ s \ \{ \bm{Q} \}}
+        \hypo{\{ \bm{Q} \} \ s' \ \{ \bm{R} \}}
+        \infer2[$\textsc{Seq}_{Ax}$]{\{ \bm{P} \} \ \texttt{s;s'} \ \{ \bm{P} \}}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\{ b \land \bm{P} \} \ s \ \{ \bm{Q} \}}
+        \hypo{\{ \neg b \land \bm{P} \} \ s' \ \{ \bm{Q} \}}
+        \infer2[$\textsc{If}_{Ax}$]{\{ \bm{P} \} \ \texttt{if b then s else s' end} \ \{ \bm{Q} \}}
+    \end{prooftree}
+\]
+\[
+    \begin{prooftree}
+        \hypo{\{ b \land \bm{P} \} \ s \ \{ \bm{P} \}}
+        \infer1[$\textsc{Wh}_{Ax}$]{\{ \bm{P} \} \ \texttt{while b do s end} \ \{ \neg b \land \bm{P} \}}
+    \end{prooftree}
+\]
+With these rules, we can only evaluate \textit{syntactically}, thus expressions like $\{ x = 4 \land y = 5 \} \ \texttt{skip} \ \{ y = 5 \land x = 4 \}$
+are not an instance of the $\textsc{Skip}_{Ax}$ because the precondition and postcondition are not identical. Thus we often need to apply \textit{semantic} reasoning,
+e.g. applying mathematical properties.
+
+\inlinedefinition[Semantic entailment] expresses the reasoning steps
+``We write $\bm{P} \models \bm{Q}$ if and only if for all states $\sigma$,
+$\cB \llbracket \bm{P} \rrbracket \sigma = \texttt{tt}$ implies $\cB \llbracket \bm{Q} \rrbracket \sigma = \texttt{tt}$''
+
+This leads to the \bi{Rule of Consequence}
+\[
+    \begin{prooftree}
+        \hypo{\{ \bm{P}' \} \ s \ \{ \bm{Q}' \}}
+        \infer1[$\textsc{Cons}_{Ax}$]{\{ \bm{P} \} \ s \ \{ \bm{Q} \}}
+    \end{prooftree}
+    \qquad
+    \text{if } \bm{P} \models \bm{P}' \text{ and } \bm{Q}' \models \bm{Q}
+\]
+a rule, where we can \bi{strengthen preconditions} ($\bm{P}$ cannot be weaker than $\bm{P}'$) and \bi{weaken postconditions} ($\bm{Q}$ cannot be stronger than $\bm{Q}'$)
+
+Since the derivation trees often get quite large, we can group them around each line in the program text.
+
+\shade{gray}{Inline Notation} can be used to make the changes more easily legible.
+For example, to express instances of $\textsc{Skip}_{Ax}$, instead of writing $\vdash \{ \bm{P} \} \ \texttt{skip} \ \{ \bm{P} \}$, we can write. 
+More examples on slides 167 - 170 (pages 30 - 33 in Slide Deck 4)
+\rmvspace
+\begin{align*}
+     & \{ \bm{P} \}        \\
+     & \quad \texttt{skip} \\
+     & \{ \bm{P} \}
+\end{align*}
+
+\shade{gray}{Forward Assignment}
+\[
+    \begin{prooftree}
+        \infer0[$\textsc{AssF}_{Ax}$]{\{ \bm{P} \} \ x := e \ \{ \exists V. \bm{P}[x \mapsto V] \land x = e[x \mapsto V] \}}
+    \end{prooftree}
+\]
diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex
new file mode 100644
index 0000000..0b482a0
--- /dev/null
+++ b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/01_hoare-logic/02_total-correctness.tex
@@ -0,0 +1,12 @@
+\paragraph{Total Correctness}
+We use a different form of Hoare triple $\{ \bm{P} \} \ s \ \{ \Downarrow \bm{Q} \}$, which describes total correctness.
+
+All rules for total correctness are equivalent to the ones for partial correctness, apart from the rule for loops.
+\[
+    \begin{prooftree}
+        \hypo{\{ b \land \bm{P} \land e = Z \} \ s \ \{ \Downarrow \bm{P} \land e < Z \}}
+        \infer1[$\textsc{WhTot}_{Ax}$]{\{ \bm{P} \} \ \texttt{while b do s end} \ \{ \Downarrow \neg b \land \bm{P} \}}
+    \end{prooftree}
+    \qquad
+    \text{if } b \land \bm{P} \models 0 \leq e
+\]
diff --git a/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex
new file mode 100644
index 0000000..879a2db
--- /dev/null
+++ b/semester4/fmfp/parts/03_language-semantics/02_axiomatic-semantics/02_soundness-completeness.tex
@@ -0,0 +1,27 @@
+\subsubsection{Soundness and Completeness}
+\inlinedefinition[Soundness] If a property can be proven, then it holds.
+As a result, an unsound derivation system does not provide any guarantees, as we may miss errors (we may have false negatives).
+
+\inlinedefinition[Completeness] If a property holds, then it can be proven.
+As a result, we may have a correct program that we can't prove in an incomplete derivation system (we may have false positives)
+
+Both can be proven with regard to an operational semantics.
+
+\inlineexample The partial correctness triple $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$ is valid, written $\models \{ \bm{P} \} \ s \ \{ \bm{Q} \}$ if and only if
+\[
+    \forall \sigma, \sigma'. \cB \llbracket \bm{P} \rrbracket \sigma = \texttt{tt} \land \vdash \langle s, \sigma \rangle \rightarrow \sigma'
+    \implies \cB \llbracket \bm{Q} \rrbracket \sigma' = \texttt{tt}
+\]
+
+More generally:
+\begin{itemize}
+    \item \bi{Soundness} $\vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \} \implies \models \{ \bm{P} \} \ s \ \{ \bm{Q} \}$
+    \item \bi{Soundness} $\models \{ \bm{P} \} \ s \ \{ \bm{Q} \} \implies \vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \}$
+\end{itemize}
+
+\begin{theorem}[]{Soundness, Completeness}
+    For all partial correctness triples $\{ \bm{P} \} \ s \ \{ \bm{Q} \}$ of IMP we have
+    \[
+        \vdash \{ \bm{P} \} \ s \ \{ \bm{Q} \} \Leftrightarrow \models \{ \bm{P} \} \ s \ \{ \bm{Q} \}
+    \]
+\end{theorem}