diff git a/graphoptimization.pdf b/graphoptimization.pdf
index 2f7642488cf5e0c58eeff95a8f74840cfb43e8c8..4fa384004bcc98ab2995ee9ad03e2316dede1a71 100644
Binary files a/graphoptimization.pdf and b/graphoptimization.pdf differ
diff git a/graphoptimization.tex b/graphoptimization.tex
index d4828297c563f56e252485e512aae9af3c3b44c9..be28a6e809ddae4f20b18bda2213979ffd2a2da7 100644
 a/graphoptimization.tex
+++ b/graphoptimization.tex
@@ 18,7 +18,7 @@
\usepackage{listings}
\usepackage{stmaryrd}
\usepackage{tikz}
\usetikzlibrary{mmt}
+\usetikzlibrary{mmt, positioning}
\usepackage[pdftex,
pdfauthor={Michael Banken},
pdftitle={TGStyler},
diff git a/src/algorithm.tex b/src/algorithm.tex
index bb1a49821cc4694189eda47799ef01f5807ee9b2..92aaabf0a04b010c248c9eeaaf6ebeb206f49e6a 100644
 a/src/algorithm.tex
+++ b/src/algorithm.tex
@@ 58,18 +58,18 @@ This runtime is especially problematic, since we need to update the the informat
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=2cm]\footnotesize
+\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
\textsf{bottom}\\\hline
X\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
+\node[thy, right of = bottom] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
Y\\\hline
not X
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
+\node[thy, right of = middle] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
X, but not Y
@@ 85,18 +85,18 @@ As we can immediately see in \autoref{fig:changeablefuture}, it is possible to r
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=2cm]\footnotesize
+\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
\textsf{bottom}\\\hline
X\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
+\node[thy, right of = bottom] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
Y\\\hline
not X
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
+\node[thy, right of = middle] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
X, but not Y
diff git a/src/candidates.tex b/src/candidates.tex
index d08b419e02bf565c26ad224743bbe119e64faf78..d57f9424800be989a77c0fc871e31fef144d0436 100644
 a/src/candidates.tex
+++ b/src/candidates.tex
@@ 8,8 +8,7 @@ For something to be declared a candidates we will only require that the theory i
Notably optimization candidates will not necessarily preserve the flattened graph. This is only the case for simply redundant inclusions(see below).
\section{Types of optimization candidates}
\subsection{Simply redundant inclusion}
+\section{Simply redundant inclusion}
\label{sec:redinc}
An inclusion of a theory $A\hookrightarrow{}C$ is \underline{simply redundant}, if $C$ includes a theory $B$, such that $B\hookrightarrow{}C$ (see \autoref{fig:redundantbasic}).
@@ 74,7 +73,7 @@ where $Includes(I)$ are the transitively included theories in I and $DirectInclu
It is immediately obvious that removing a simply redundant inclusion I from a theory T also removes it from the above set via the intersection with $DirectIncludes(T)$.\\
Slightly less obvious is that doing so neither adds nor removes any other inclusions. This is because by design the set $\bigcup_{I \in DirectIncludes(T)}Includes(I))$ still includes I and any of its children and thus remains unchanged.
\subsection{Superfluous Inclusion}
+\section{Superfluous Inclusion}
\label{sec:superinc}
An inclusion of a theory $A\hookrightarrow{}B$ is \underline{superfluous}, if $B$ uses none of the constants declared in $A$. Such an inclusion can be \underline{purely superfluous} (\autoref{sec:puresi}) if it can be entirely removed, or \underline{partially superfluous} if it can be reduced to a subset of the theory inclusions in $A$ \autoref{sec:partiallysi}.\\
In both of these cases the inclusion can be replaced or removed entirely, while still yielding a well formed theory. However this changes the resulting flattened theory graph and can invalidate theories that include the optimized theory.\\
@@ 82,9 +81,9 @@ In both of these cases the inclusion can be replaced or removed entirely, while
The superfluous inclusions in a theory T are the set $I_{S}(T) =$\\ $ \{ I \in DirectInludes(T)  I \notin UsedTheories(T) \}$,\\
where $DirectIncludes(T)$ are the theories included directly in the theory T and UsedTheories(T) are those theories whose terms are used in T.
\subsubsection{Purely Superfluous Inclusion}
An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}, if $B$ uses none of the constants in $A$, not even if they were declared in a theory $C$ such that $C\hookrightarrow{}A$.\\
+\subsection{Purely Superfluous Inclusion}
\label{sec:puresi}
+An inclusion of a theory $A\hookrightarrow{}B$ is \underline{purely superfluous}, if $B$ uses none of the constants in $A$, not even if they were declared in a theory $C$ such that $C\hookrightarrow{}A$.\\
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=3cm]\footnotesize
@@ 126,29 +125,31 @@ Purely superfluous inclusions can be removed while still retaining a valid theor
The purely superfluous inclusions in a theory T are the set $I_{PuS}(T) =$\\ $ \{ I \in DirectInludes(T)  I \notin UsedTheories(T) \land Includes(I) \cap UsedTheories(T) \setminus Includes(UsedTheories(T)\setminus \{ T \}) = \emptyset \}$,\\
where $Includes(I)$ are the transitively included theories in I, $DirectIncludes(T)$ are the theories included directly in the theory T and $UsedTheories(T)$ are those theories whose terms are used in T.
\subsubsection{Partially Superfluous Inclusion}
+\subsection{Partially Superfluous Inclusion}
\label{sec:partiallysi}
An inclusion of a theory $A\hookrightarrow{}B$ is \underline{partially superfluous}, if $B$ uses none of the constants in $A$, but uses some declarations that were declared in one or more theory $C$ such that C is (transitively) included in A. We describe theories that have declarations being used in a theory A, which includes them, as \underline{theories used by A}.\\
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=3cm]\footnotesize
+\begin{tikzpicture}[node distance=2cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
\textsf{bottom}\\\hline
$X_1$\\\hline
...
\end{tabular}};
\node[right of = bottom] (dots) {...};
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
+\node[below = 0.2cm of bottom] (dots) {\begin{tabular}{l}
+ .\\.\\.\\
+ \end{tabular}};
+\node[thy, below = 0.2cm of dots] (bottomn) {\begin{tabular}{l}
\textsf{$bottom_n$}\\\hline
$X_n$\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
+\node[thy, right = 1.5cm of dots] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
Y\\\hline
...
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
+\node[thy, right = 1.2cm of middle, node distance=4.3cm ] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
$X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
@@ 165,24 +166,26 @@ Partially superfluous inclusions can be optimized by identifying the used subset
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=3cm]\footnotesize
+\begin{tikzpicture}[node distance=2cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
\textsf{bottom}\\\hline
$X_1$\\\hline
...
\end{tabular}};
\node[right of = bottom] (dots) {...};
\node[thy, right of = dots] (bottomn) {\begin{tabular}{l}
+\node[below = 0.2cm of bottom] (dots) {\begin{tabular}{l}
+ .\\.\\.\\
+ \end{tabular}};
+\node[thy, below = 0.2cm of dots] (bottomn) {\begin{tabular}{l}
\textsf{$bottom_n$}\\\hline
$X_n$\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
+\node[thy, right = 1.5cm of dots] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
Y\\\hline
...
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
+\node[thy, right = 1.2 of middle, node distance=4.3cm ] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
$X\subseteq\bigcup{}\{X_1,...,X_n\}$, but not Y
@@ 190,7 +193,7 @@ Partially superfluous inclusions can be optimized by identifying the used subset
\draw[include] (bottom)  (middle);
\draw[include] (bottomn)  (middle);
\draw[include] (bottomn)  (top);
\draw[include, bend left] (bottom) edge (top);
+\draw[include] (bottom)  (top);
\end{tikzpicture}
\caption{Example of partially superfluous inclusion optimized}
\label{fig:partiallysuperfluousoptimized}
@@ 208,18 +211,18 @@ The danger of performing the proposed optimizations varies between the type of c
As noted in \autoref{sec:puresi} there is very little that speaks against removing simply redundant inclusions, since the flattened graph is preserved. However there are some cases where they might do more harm than good, particularly when they overlap with superfluous inclusions, as seen in \autoref{fig:redundantoverlap}.\\ Removing the redundant edge will not change the flattened graph, but it will complicate the changes needed to remove the superfluous edge between middle and top. A simple solution to avoiding this problem is to relegate the removal of simple redundancies until after other optimizations have been performed on the theory.\\
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=2cm]\footnotesize
+\begin{tikzpicture}[node distance=3cm]\footnotesize
\node[thy] (bottom) {\begin{tabular}{l}
\textsf{bottom}\\\hline
X\\\hline
...
\end{tabular}};
\node[thy, above of = bottom] (middle) {\begin{tabular}{l}
+\node[thy, right of = bottom] (middle) {\begin{tabular}{l}
\textsf{middle}\\\hline
Y\\\hline
...
\end{tabular}};
\node[thy, above of = middle] (top) {\begin{tabular}{l}
+\node[thy, right of = middle] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
X, but not Y
@@ 244,14 +247,14 @@ Removing purely superfluous includes from a theory union will leave behind an en
\node[thy] (union) {\begin{tabular}{l}
\textsf{union}\\\hline
\\\hline

+ \hfill
\end{tabular}};
\node[thy, below left of = union] (A) {\begin{tabular}{l}
+\node[thy, above left = 0.2cm and 1.2cm of union] (A) {\begin{tabular}{l}
\textsf{A}\\\hline
...\\\hline
...
\end{tabular}};
\node[thy, below right of = union] (B) {\begin{tabular}{l}
+\node[thy, below left = 0.2cm and 1.2cm of union] (B) {\begin{tabular}{l}
\textsf{B}\\\hline
...\\\hline
...
@@ 277,17 +280,17 @@ Another problem arises were inclusion paths branch of before eventually meeting
X\\\hline
...
\end{tabular}};
\node[thy, above right of = bottom] (right) {\begin{tabular}{l}
+\node[thy, below right = 0cm and 1 cm of bottom] (right) {\begin{tabular}{l}
\textsf{right}\\\hline
Y\\\hline
not X
\end{tabular}};
\node[thy, above left of = bottom] (left) {\begin{tabular}{l}
+\node[thy, above right = 0cm and 1 cm of bottom] (left) {\begin{tabular}{l}
\textsf{left}\\\hline
Z\\\hline
not X
\end{tabular}};
\node[thy, above left of = right] (top) {\begin{tabular}{l}
+\node[thy, above right = 0cm and 1 cm of right] (top) {\begin{tabular}{l}
\textsf{top}\\\hline
...\\\hline
X, Y, Z
@@ 311,18 +314,18 @@ Let us consider the following example from elementary Algebra (\autoref{fig:elal
\begin{figure}[!htb]
\centering
\begin{tikzpicture}[node distance=2cm]\myfontsize
+\begin{tikzpicture}[node distance=3cm]\myfontsize
\node[thy] (magma) {\begin{tabular}{l}
\textsf{Magma}\\\hline
$G,\circ$\\\hline
$\scriptstyle x\circ y\in G$
\end{tabular}};
\node[thy, above of=magma] (sg) {\begin{tabular}{l}
+\node[thy, right of=magma] (sg) {\begin{tabular}{l}
\textsf{SemiGrp}\\\hline
\\\hline
$\scriptstyle (x\circ y)\circ z=x\circ (y\circ z)$
\end{tabular}};
\node[thy, above of=sg] (m) {\begin{tabular}{l}
+\node[thy, right of=sg] (m) {\begin{tabular}{l}
\textsf{Monoid}\\\hline
$e$\\\hline
$\scriptstyle e\circ x=x\circ e=x$
diff git a/src/introduction.tex b/src/introduction.tex
index 92fbb3cdbf38e52e9cf3449474ea1d870aede2cc..8a77fbdcd4fde1b51a22e09236dae8b025824798 100644
 a/src/introduction.tex
+++ b/src/introduction.tex
@@ 5,7 +5,7 @@ Knowledge is complicated and so is its representation, especially when trying to
\begin{figure}[!htb]
\centering
\includegraphics[width=\textwidth/2]{tgview}
+\includegraphics[width=\textwidth]{tgview}
\caption{Picture of the LATIN archive\cite{latin} graph using TGView\cite{rupprecht2017flexible}}
\label{fig:tgview}
\end{figure}
diff git a/src/titlepage.tex b/src/titlepage.tex
index 5af471aceeafbd089bb65f079c576caae15e940e..18b5841053422120951f7be808632725dc9806ed 100644
 a/src/titlepage.tex
+++ b/src/titlepage.tex
@@ 16,7 +16,7 @@ ErlangenNürnberg%
\rule{\textwidth}{1pt}\par
\vspace{0.5\baselineskip}
{% maybe \itshape?
\Huge\bfseries Styler
+\Huge\bfseries TGStyler
\\[1cm]
\large\bfseries
A static analysis tool for optimizing theory graphs