Final version report practical 1

1 files changed, 39 insertions, 32 deletions

diff --git a/Practical1/report/algorithm.tex b/Practical1/report/algorithm.tex
index f6272e4..8ed3ccf 100644
--- a/Practical1/report/algorithm.tex
+++ b/Practical1/report/algorithm.tex
@@ -3,21 +3,25 @@
 
 \subsection{Basic structure}
 \label{sec:algorithm:basic-structure}
-The basic structure of the algorithm is fairly simple. For any graph $G=(V,E)$, we pick a vertex $v\in V$. Either that vertex is in an m.i.s. (and none of its neighbours), or it is not. This gives the recurrence: \refeq[basic-structure]{\ms(G) = \max(1 + \ms(G\ex \iN(v)), \ms(G\ex v)).} The rest of the algorithm will be optimising this basic structure by cleverly choosing $v$ and pruning the search tree.
+The basic structure of the algorithm is fairly simple. For any graph $G=(V,E)$, we pick a vertex $v\in V$. Either that vertex is in an m.i.s. (and none of its neighbours), or it is not. This gives the recurrence: \refeq[basic-structure]{\ms(G) = \max(1 + \ms(G\ex \iN(v)), \ms(G\ex v)).}
+
+Every recursive algorithm needs a base case.
 
 \begin{thmproof}[base-case]{lemma}{For a graph $G$ with $|G|\leq1$, we have $\ms(G)=|G|$.}
     For both the cases $|G|=0$ and $|G|=1$, $G$ is an m.i.s. of itself.
 \end{thmproof}
 
+The rest of this section is devoted to optimising this basic structure by cleverly choosing $v$ and pruning the search tree.
+
 \begin{thmproof}[one-neighbour]{lemma}{For a graph $G=(V,E)$ and vertex $v\in V$, if $v$ is not in an m.i.s. there is a neighbour $w\in N(v)$ which is in an m.i.s.}
     By contradiction. Suppose there were an m.i.s. $ms_1$ that does not contain $v$ or one of its neighbours. Then we may create a new m.i.s. $ms_2=ms_1\with v$. We then have $|ms_2| = |ms_1|+1 > |ms_1|$. Therefore, $ms_1$ was not maximal.
 \end{thmproof}
 
 \begin{thmproof}[two-neighbours]{lemma}{For a graph $G=(V,E)$ and vertex $v\in V$, there is an m.i.s. with $v$, or there is an m.i.s. with two distinct elements $w_1,w_2\in N(v)$.}
-    By contradiction. If $v$ is in an m.i.s., we're done. If $v$ is not in an m.i.s., we know by \autoref{lem:one-neighbour} that there is a $w_1\in N(v)$ that is, say in m.i.s. $ms$. Suppose there were no other neighbour $w_2\in N(v), w_2\neq w_1$ with $w_2\in ms$. Then $ms\ex w_1\with v$ is also an m.i.s., and it does contain $v$.
+    By contradiction. If $v$ is in an m.i.s., we're done. If $v$ is not in an m.i.s., we know by \autoref{lem:one-neighbour} that there is a $w_1\in N(v)$ that is in an m.i.s., say $ms$. Suppose there were no other neighbour $w_2\in N(v), w_2\neq w_1$ with $w_2\in ms$. Then $ms\ex w_1\with v$ is also an m.i.s., and it does contain $v$.
 \end{thmproof}
 
-At this point we define, as Robson \cite{robson}, the function $\ms^n(G,S)$ which is the $\ms(G)$ given that the m.i.s. should contain at least $n$ elements of $S$.
+At this point we define, as Robson \cite{robson}, the function $\ms^n(G,S)$ as the $\ms(G)$ given that the m.i.s. should contain at least $n$ elements of $S$.
 
 Based on \autoref{lem:one-neighbour} and \ref{lem:two-neighbours} we may then rewrite \autoref{eq:basic-structure} to \refeq[with-two-neighbours]{\ms(G) = \max(1+\ms(G\ex\iN(v)), \ms^2(G\ex v, N(v))).}
 
@@ -33,15 +37,15 @@ Until now, we have assumed that we have some vertex $v$. Let us now discuss how
     A straightforward implementation of $\ms^2(G\ex v,N(v))$ will consider all pairs of vertices in $N(v)$, which is quadratic. In the left-hand side, $\ms(G\ex\iN(v))$ is only linearly faster with large $d(v)$. Therefore, we should prefer small $d(v)$.
 \end{thmproof}
 
-In general, we'd like to use \autoref{eq:with-two-neighbours}, because the right-hand side of the $\max$ is more restricted than in \autoref{eq:basic-structure}. However, if we have a $v$ with large $d(v)$, this may not be the case. 
+In general, we'd like to use \autoref{eq:with-two-neighbours}, because the right-hand side of the $\max$ is more restricted than in \autoref{eq:basic-structure}. However, if we have a $v$ with large $d(v)$, \ref{eq:basic-structure} may be more efficient.
 
 So, we should try to pick a $v$ with small $d(v)$. We apply \autoref{eq:with-two-neighbours} if $d(v)$ is small enough. If $d(v)$ is too large to ensure efficient usage of \autoref{eq:with-two-neighbours}, we apply \autoref{eq:basic-structure}.
 
-But this latter recurrence is clearly more efficient for \emph{large} $d(v)$. Therefore, if $d(v)$ is too large to use $v$ in \autoref{eq:with-two-neighbours}, we find one of its neighbours, say $w\in N(v)$, with the largest $d(w)$, and apply \autoref{eq:basic-structure} with that vertex. In the next recurrence, $d(v)$ will be at least one smaller, because $w$ has been removed, but in the case of a graph with many three-cycles, $d(v)$ may be much smaller. So, after at most a few applications of \autoref{eq:basic-structure} we may use the more efficient \autoref{eq:with-two-neighbours} again.
+But this latter recurrence is clearly more efficient for \emph{large} $d(v)$. Therefore, if $d(v)$ is too large to use $v$ in \autoref{eq:with-two-neighbours}, we find one of its neighbours, say $w\in N(v)$, with the largest $d(w)$, and apply \autoref{eq:basic-structure} to that vertex. In the next recurrence, $d(v)$ will be at least one smaller, because $w$ has been removed, but in the case of a graph with many three-cycles, $d(v)$ may be much smaller. So, after at most a few applications of \autoref{eq:basic-structure} we may use the more efficient \autoref{eq:with-two-neighbours} again.
 
 \subsubsection{Dominance}
 \label{sec:algorithm:good-v:dominance}
-\begin{thmproof}[dominance]{lemma}{If in graph $G$ with vertices $v,w$ we have $v>w$, we know that $\ms(G)=\ms(G\ex w)$.}
+\begin{thmproof}[dominance]{lemma}{If for a graph $G=(V,E)$ with vertices $v,w\in V$ we know $v>w$, we have $\ms(G)=\ms(G\ex w)$.}
     If there is an m.i.s. $ms$ with $w\in ms$, $ms\ex w\with v$ is an m.i.s. as well.
 \end{thmproof}
 
@@ -54,13 +58,13 @@ This gives us \autoref{alg:with-best-vertex}, which combines \autoref{eq:basic-s
     \label{alg:with-best-vertex}
     \begin{algorithmic}[1]
         \REQUIRE $G=(V,E)$
-        \IF{$|G|=1$}
+        \IF{$|G|\le1$}
             \RETURN $|G|$ \COMMENT{\autoref{lem:base-case}}
         \ELSE
             \STATE $v\gets v\in V$ with minimal $d(v)$
             \IF{$d(v)$ is small enough}
                 \RETURN $\max(1+\ms(G\ex\iN(v)), \ms^2(G\ex v,N(v)))$ \COMMENT{\autoref{eq:with-two-neighbours}}
-            \ELSIF{$v$ dominates $w$}
+            \ELSIF{$v>w$}
                 \RETURN $\ms(G\ex w)$ \COMMENT{\autoref{lem:dominance}}
             \ELSE
                 \STATE $w\gets w\in N(v)$ with maximal $d(w)$
@@ -82,24 +86,24 @@ This gives us \autoref{alg:with-best-vertex}, which combines \autoref{eq:basic-s
     If there were a larger m.i.s. in the graph, there has to be a $v$ in a strongly connected component $C$ in that m.i.s. which is not in the m.i.s. of $C$. If we can add $v$ to the m.i.s. of $C$, that m.i.s. wasn't maximal. If we cannot, then the larger m.i.s. of the whole graph cannot be an independent set.
 \end{thmproof}
 
-Based on \autoref{lem:components} we may write \refeq[with-components]{\ms(G)=\sum_{c\in C} \ms(c),} where $C$ is the set of strongly connected components of $G$. It is not difficult to see that in case a graph has multiple strongly connected components, this recurrence is more efficient than \autoref{alg:with-best-vertex}.
+It is not difficult to see that in case a graph has multiple strongly connected components, this recurrence is more efficient than \autoref{alg:with-best-vertex}.
 
 \subsection{Further optimisations}
 \label{sec:algorithm:further-optimisations}
-Although I have referred to Robson \cite{robson} and used his notation throughout this report, this is how far I got without his help. Robson then introduces a number of further optimisations. In this section, we use $G$ for the graph at hand and $v,w$ for the vertex with the lowest degree, and its neighbour with the highest degree, respectively.
+Although I have referred to Robson \cite{robson} and used his notation already, this is how far I got without his help. Robson then introduces a number of further optimisations. In this section, we use $G$ for the graph at hand and $v,w$ for the vertex with the lowest degree, and its neighbour with the highest degree, respectively.
 
-\begin{thmproof}[robson-ms-d1]{lemma}{If $d(v)=1$, we know $\ms(G)=1+\ms(G\ex\iN(v))$.}
+\begin{thmproof}[robson-ms-d1]{lemma}{If $d(v)=1$, we have $\ms(G)=1+\ms(G\ex\iN(v))$.}
     By contradiction. By \autoref{lem:one-neighbour} we know that if $v$ is not in any m.i.s., then $w$ is in an m.i.s., say $ms$. But then $ms\ex w\with v$ is also independent, and has the same size.
 \end{thmproof}
 
 For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
 
-\begin{thmproof}[robson-ms-d2-edge]{lemma}{If $d(v)=2$ and $e(w,w')$, we know $\ms(G)=1+\ms(G\ex\iN(v))$.}
+\begin{thmproof}[robson-ms-d2-edge]{lemma}{If $d(v)=2$ and $e(w,w')$, we have $\ms(G)=1+\ms(G\ex\iN(v))$.}
     By \autoref{lem:two-neighbours} we know that an m.i.s. will either contain $v$ or both $w$ and $w'$. But since $e(w,w')$, the latter cannot happen. Therefore, it must contain $v$ and neither of its neighbours.
 \end{thmproof}
 
 \begin{thmproof}[robson-ms-d2-noedge]{lemma}{If $d(v)=2$ and $\lnot e(w,w')$, we know $$\ms(G) = \max(2+\ms(G\ex\iN(w)\ex\iN(w')), 1 + \ms^2(G\ex\iN(v), N^2(v))).$$}
-    By \autoref{lem:two-neighbours}, an m.i.s. contains either $v$ or both $w,w'$. In the second case, we remove $w$ and $w'$ and their neighbourhoods from the graph (the left-hand side of $\max$). In the first case, the m.i.s. cannot contain $w$ or $w'$ but must contain two of their neighbours other than $v$. If not, and there is an m.i.s. $ms$ with at most one such neighbour, $u$, then $ms\ex v\ex u\with w\with w'$ is also independent, and has the same size. This gives the right-hand side.
+    By \autoref{lem:two-neighbours}, an m.i.s. contains either $v$ or both $w$ and $w'$. In the second case, we remove $w$ and $w'$ and their neighbourhoods from the graph (the left-hand side of $\max$). In the first case, the m.i.s. cannot contain $w$ or $w'$ but must contain two of their neighbours other than $v$. If not, and there is an m.i.s. $ms$ with at most one such neighbour, $u$, then $ms\ex v\ex u\with w\with w'$ is also independent, and has the same size. This gives the right-hand side.
 \end{thmproof}
 
 \autoref{alg:with-best-vertex} combined with \autoref{lem:components}, \ref{lem:robson-ms-d1}, \ref{lem:robson-ms-d2-edge} and \ref{lem:robson-ms-d2-noedge} gives us \autoref{alg:with-robsons-optimisations}.
@@ -120,7 +124,7 @@ For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
             \IF{$d(v)=1$}
                 \RETURN $1+\ms(G\ex\iN(v))$ \COMMENT{\autoref{lem:robson-ms-d1}}\label{alg:ms:case-d1}
             \ELSIF{$d(v)=2$}
-                \STATE $w'\gets$ the other neighbour of $v$
+                \STATE $\{w'\}\gets N(v)\ex w$
                 \IF{$e(w,w')$}
                     \RETURN $1+\ms(G\ex\iN(v))$ \COMMENT{\autoref{lem:robson-ms-d2-edge}}\label{alg:ms:case-d2-edge}
                 \ELSE
@@ -142,11 +146,11 @@ For the case that $d(v)=2$ we write $w,w'$ for the neighbours of $v$.
 \end{thmproof}
 
 \begin{thmproof}[ms-efficiency]{theorem}{\autoref{alg:ms} is more efficient than \autoref{alg:with-best-vertex}, assuming that conditions are evaluated efficiently.}
-    The algorithm follows the same basic structure. In any case that \autoref{alg:ms} is different, it considers less cases (yet it is still correct by \autoref{thm:ms-correct}). Therefore, it can only be more efficient.
+    The algorithm follows the same basic structure. In any case that \autoref{alg:ms} is different, it considers less cases or smaller graphs (yet it is still correct by \autoref{thm:ms-correct}). Therefore, it can only be more efficient.
 \end{thmproof}
 
 \begin{thmproof}[ms-terminates]{theorem}{\autoref{alg:ms} terminates with every input, if $\ms^2$ terminates with a smaller input.}
-    There is a base case on line \ref{alg:ms:case-g1} which is not recursive and handles the graphs with the lowest $k$ possible orders ($k=2$). In every other case, the same algorithm is run on a smaller input (or $\ms^2$ on a smaller input), so inductively the algorithm terminates with any input.
+    There is a base case on line \ref{alg:ms:case-g1} which is not recursive that handles the graphs with the lowest $k$ possible orders ($k=2$). In every other case, the same algorithm or $\ms^2$ is run on a smaller input, so inductively the algorithm terminates with any input.
 \end{thmproof}
 
 \subsection{The helper function $\ms^n$}
@@ -161,15 +165,15 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
 
 \autoref{lem:helper-general} may be used as a default case, when no clever optimisation can be found.
 
-\begin{thmproof}[helper-1]{lemma}{If $|S|<n$, we know $\ms^n(G,S)=0$.}
-    It is impossible to pick $n$ edges from less than $n$.
+\begin{thmproof}[helper-1]{lemma}{If $|S|<n$, we have $\ms^n(G,S)=0$.}
+    It is impossible to pick $n$ vertices from less than $n$.
 \end{thmproof}
 
 \begin{thmproof}[helper-2-edge]{lemma}{If $|S|=2$ and $e(s_1,s_2)$, then $\ms^2(G,S)=0$.}
-    The only possibility to choose two vertices from $S$, choosing $s_1$ and $s_2$ does not give us an independent set.
+    The only possibility to choose two vertices from $S$, choosing $s_1$ and $s_2$, does not give us an independent set.
 \end{thmproof}
 
-\begin{thmproof}[helper-2-noedge]{lemma}{If $|S|=2$ and $\lnot e(s_1,s_2)$, then $\ms^2(G,S)=2+\ms(G\ex\iN(s_1)\ex\iN(S_2)$.}
+\begin{thmproof}[helper-2-noedge]{lemma}{If $|S|=2$ and $\lnot e(s_1,s_2)$, then $\ms^2(G,S)=2+\ms(G\ex\iN(s_1)\ex\iN(S_2))$.}
     We only have to consider the one possibility of choosing $s_1$ and $s_2$. Then we may remove their inclusive neighbourhoods from the graph.
 \end{thmproof}
 
@@ -197,17 +201,17 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
                 \RETURN $1+\ms^1(G\ex s_i,S\ex s_i)$ \COMMENT{Special case of \autoref{lem:components}}\label{alg:ms2:case-s3-d0}
             \ELSIF{$s_1,s_2,s_3$ form a three-cycle}
                 \RETURN $0$ \COMMENT{Impossible to pick two vertices from a three-cycle}\label{alg:ms2:case-s3-cycle}
-            \ELSIF{$\exists_{i,j,k}[i\neq k \land e(s_i,s_j) \land e(s_i,s_k)]$}
+            \ELSIF{$\exists_{i,j,k}[j\neq k \land e(s_i,s_j) \land e(s_i,s_k)]$}
                 \RETURN $2 + \ms(G\ex\iN(s_j)\ex\iN(s_k))$ \COMMENT{Impossible to choose $s_i$ and another vertex, so we have to choose $s_j$ and $s_k$}\label{alg:ms2:case-s3-path}
             \ELSIF{$\exists_{i,j}[e(s_i,s_j)]$}
-                \STATE $s_k\gets S\ex s_1\ex s_j$
-                    \RETURN $1 + \ms^1(G\ex\iN(s_k), S\ex s_k)$ \COMMENT{Impossible to choose $s_i$ and $s_j$, so we choose $s_k$ and one of $s_i,s_j$}\label{alg:ms2:case-s3-edge}
+                \STATE $\{s_k\}\gets S\ex s_i\ex s_j$
+                \RETURN $1 + \ms^1(G\ex\iN(s_k), S\ex s_k)$ \COMMENT{Impossible to choose $s_i$ and $s_j$, so we choose $s_k$ and one of $s_i,s_j$}\label{alg:ms2:case-s3-edge}
             \ELSIF{$\exists_{i,j}[N(s_i)\cap N(s_j)\neq\emptyset]$}
                 \RETURN $\ms^2(G\ex(N(s_i)\cap N(s_j)), S)$ \COMMENT{m.i.s. contains either $s_i$ or $s_j$, so not their common neighbours}\label{alg:ms2:case-s3-intersection}
             \ELSIF{$\exists_i[d(s_i)=1]$}
                 \RETURN $1+\ms^1(G\ex\iN(s_i),S\ex s_i)$ \COMMENT{Special case of \autoref{lem:one-neighbour}}\label{alg:ms2:case-s3-d1}
             \ELSE
-                \RETURN $\max(1+\ms^1(G\ex\iN(s_1),S\ex s_1), 2 + \ms^2(G\ex\iN(s_2)\ex\iN(s_3)\ex s_1, N(s_1)))$ \COMMENT{Either the m.i.s. does contain $s_1$, and one of $s_2,s_3$, or it doesn't. In the latter case, it must contain $s_2,s_3$, and at least two on $s_1$'s neighbours, using an argument similar to \autoref{lem:two-neighbours}. Robson misses the `$2+$' for this second case, but from the writing it is clear that it should be included.}\label{alg:ms2:case-s3-otherwise}
+                \RETURN $\max(1+\ms^1(G\ex\iN(s_1),S\ex s_1), 2 + \ms^2(G\ex\iN(s_2)\ex\iN(s_3)\ex s_1, N(s_1)))$ \COMMENT{Either the m.i.s. does contain $s_1$, and one of $s_2,s_3$, or it doesn't. In the latter case, it must contain $s_2,s_3$, and at least two of $s_1$'s neighbours, using an argument similar to \autoref{lem:two-neighbours}. Robson misses the `$2+$' for this second case, but from the writing it is clear that it should be there.}\label{alg:ms2:case-s3-otherwise}
             \ENDIF
         \ELSIF{$|S|=4$}
             \IF{$\lnot\exists_i[d(s_i)\leq3]$}
@@ -222,7 +226,7 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
 \end{algorithm}
 
 \begin{thmproof}[ms2-correct]{theorem}{\autoref{alg:ms2} is a correct implementation of the $\ms^2$ function.}
-    This follows from \autoref{lem:helper-general} through \ref{lem:helper-2-noedge} and \autoref{lem:one-neighbour} and \ref{lem:components}. We have only made small efficiency enhancements that are clearly correct and are argued in the definition of the algorithm.
+    This follows from \autoref{lem:one-neighbour}, \ref{lem:components} and \ref{lem:helper-general} through \ref{lem:helper-2-noedge}. We have only made small efficiency enhancements that are clearly correct and are argued in the definition of the algorithm.
 \end{thmproof}
 
 \begin{thmproof}[ms2-terminates]{theorem}{\autoref{alg:ms2} terminates for any input, if $\ms$ and $\ms^1$ terminate with a smaller input.}
@@ -231,26 +235,27 @@ We will write $s_1,s_2,\dots$ for the elements of $S$.
 
 \bigskip
 
-As the observant reader may have noticed, we use $\ms^1$ in the definition of $\ms^2$. We therefore also need to write an efficient algorithm to apply this function. Of course, \autoref{lem:helper-general} and \ref{lem:helper-1} apply to $\ms^1$ as well. Note, that we always call $\ms^1(\cdots,S)$ with $|S|=2$. We will therefore not give a complete algorithm $\ms^1$, but one that works in the necessary cases.
+\clearpage
+As the observant reader may have noticed, we use $\ms^1$ in the definition of $\ms^2$. We therefore also need to write an efficient algorithm to apply this function. Of course, \autoref{lem:helper-general} and \ref{lem:helper-1} apply to $\ms^1$ as well. Note, that we always call $\ms^1(\cdots,S)$ with $|S|=2$. We will not give a complete algorithm for $\ms^1$, but one that works in the necessary cases.
 
-\begin{thmproof}[helper-intersection]{lemma}{If $N(s_1)\cap N(s_2)\neq\emptyset$, we know $\ms^1(G,S)=\ms^1(G\ex(N(s_1)\cap N(s_2)), S)$.}
-    This was already used in \autoref{alg:ms2}, in the case of three states. The m.i.s. will contain either $s_1$ or $s_2$, therefore cannot contain the intersection of their neighbourhoods. Removing these vertices allows for early pruning.
+\begin{thmproof}[helper-intersection]{lemma}{If $N(s_1)\cap N(s_2)\neq\emptyset$, we have $\ms^1(G,S)=\ms^1(G\ex(N(s_1)\cap N(s_2)), S)$.}
+    Something similar was already used in \autoref{alg:ms2}. The m.i.s. will contain either $s_1$ or $s_2$, therefore cannot contain the intersection of their neighbourhoods. Removing these vertices allows for early pruning.
 \end{thmproof}
 
 Robson adds further optimisations to this.
 
 \begin{thmproof}[helper-ms1-2-2]{lemma}{If $d(s_1)=d(s_2)=2$ and $\lnot e(s_1,s_2)$, an m.i.s. containing one of $s_1,s_2$ will contain either $s_1$ or $N(s_1)\with\{s_2\}$.}
-    In the case that the m.i.s. contains $s_1$, we are done. If an m.i.s. $ms$ does not contain $s_1$ but $s_2$, it must contain $N(s_1)$, because otherwise $ms\ex N(s_1)\with s_1$ is an independent set of at least the same size.
+    Special case of \autoref{lem:two-neighbours}.
 \end{thmproof}
 
 If the conditions of \autoref{lem:helper-ms1-2-2} are met, write $w_1,w_2$ for the two neighbours of $s_1$.
 
 \begin{thmproof}[helper-ms1-2-2-edge]{lemma}{If the conditions of \autoref{lem:helper-ms1-2-2} are met and $e(w_1,w_2)$, we have $\ms^1(G,S)=1+\ms(G\ex s_1)$.}
-    It cannot be the case that an m.i.s. will contain $N(s_1)$. \autoref{lem:helper-ms1-2-2} leaves this (choosing $s_1$) as only option.
+    It cannot be the case that an m.i.s. will contain $N(s_1)$. \autoref{lem:helper-ms1-2-2} leaves choosing $s_1$ as only option.
 \end{thmproof}
 
 \begin{thmproof}[helper-ms1-2-2-dominance]{lemma}{If the conditions of \autoref{lem:helper-ms1-2-2} are met and $N^2(s_1)\subset N(s_2)$, we have $\ms^1(G,S)=3+\ms(G\ex\iN(s_1)\ex\iN(s_2))$.}
-    Obviously, an m.i.s. $\iN(s_1)+\iN(s_2)$ that contains $s_1$ or $s_2$ cannot be larger than three. Furthermore, $\{w_1,w_2,s_2\}$ is an independent set and dominates every other independent set of the same size.
+    Obviously, an m.i.s. of the induced subgraph $\iN(s_1)+\iN(s_2)$ that contains $s_1$ or $s_2$ cannot be larger than three. Furthermore, $\{w_1,w_2,s_2\}$ is an independent set of that subgraph and dominates every other independent set of the same size.
 \end{thmproof}
 
 This leads us to a slightly adapted version of $\ms^2$ that we can use for $\ms^1$. Pseudocode is given in \autoref{alg:ms1}.
@@ -293,5 +298,7 @@ This leads us to a slightly adapted version of $\ms^2$ that we can use for $\ms^
     Inductively by \autoref{thm:ms-terminates} and \ref{thm:ms2-terminates}.
 \end{thmproof}
 
-If we assume to have implementations of the more obvious graph algorithms such as the neighbours of a vertex, we now have by \autoref{thm:ms-correct} a correct implementation of the maximum independent set problem.
+\begin{thmproof}[everything-correct]{theorem}{\autoref{alg:ms}, \ref{alg:ms2} and \ref{alg:ms1} form a correct and total algorithm for the maximum independent set problem.}
+    The algorithm is total by \autoref{thm:ms-terminates}, \ref{thm:ms2-terminates} and \ref{thm:ms1-terminates}. It is correct by \autoref{thm:ms-correct}, \ref{thm:ms2-correct} and \ref{thm:ms1-correct}.
+\end{thmproof}