Fix and add theorems

1 files changed, 28 insertions, 11 deletions

diff --git a/mgr.tex b/mgr.tex
index 7ba597c..4db589a 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -531,18 +531,24 @@ The question answering problem we will solve is:
 
 \queryproblem[%
     regular language $L$ over alphabet $\Sigma$, given by DFA $A$.
-]{Branch Infix Regular Questions}{%
+]{\label{branch-infix-problem} Branch Infix Regular Questions}{%
     a $\Sigma$-labeled tree $T$.
 }{%
     given a vertex $x$ and its descendant $y$, does the word given by labels on
     the path from $x$ to $y$ belong to $L$?
 }
 
-Let $n$ be the size of $V(T)$. We begin with a similar construction as in the
-word case, i.e. we create a graph of $n+1$ copies of $A$'s states $Q$. The
-vertex set of the graph will be $(V(T) \cup \{ \mathsf{root} \}) \times Q \}$
-and we can refer to a specific vertex as $x.q$ for $x \in V(T) \cup \{
-\mathsf{root} \}, q \in Q$.
+Let $n$ be the size of $V(T)$.
+
+\begin{theorem}\label{branch-infix-theorem}
+    Problem \ref{branch-infix-problem} can be solved in time
+    \qptime{$O_{A}(n)$}{$O_{A}(1)$}.
+\end{theorem}
+
+We begin with a similar construction as in the word case, i.e. we create a graph
+of $n+1$ copies of $A$'s states $Q$. The vertex set of the graph will be $(V(T)
+\cup \{ \mathsf{root} \}) \times Q \}$ and we can refer to a specific vertex as
+$x.q$ for $x \in V(T) \cup \{ \mathsf{root} \}, q \in Q$.
 
 Again, each letter $a \in \Sigma$ defines a function $a : Q \to Q$, and these
 functions induce edges in our ``fattened'' tree: consider a vertex $x$ of $T$,
@@ -607,7 +613,7 @@ subproblem.
 
 Consider the following question answering problem:
 
-\queryproblem{Highest Marked Descendant on Path Questions}{%
+\queryproblem{\label{highest-marked-problem} Highest Marked Descendant on Path Questions}{%
     a tree $T$ with set $M \subseteq V(T)$ of marked vertices.
 }{%
     given a vertex $x$, its descendant $y$, find the node $z \in M$ that
@@ -615,6 +621,11 @@ Consider the following question answering problem:
     exists.
 }
 
+\begin{theorem}\label{highest-marked-theorem}
+    Problem \ref{highest-marked-problem} can be solved in time
+    \qptime{$O(n)$}{$O(1)$}.
+\end{theorem}
+
 We will build an index structure, constructible in linear time, that allows us
 to handle such questions in constant time. The structure is heavily inspired by
 \textcite{bender2000}, where a simple algorithm for answering LCA questions is
@@ -710,6 +721,10 @@ check).
 See Figure \ref{marked-figure} for a visual example of the data structure
 described.
 
+Constructing each of $\posttable$, $\prefixtable$, and $\indextable$ takes linear
+time, RMQ is a \qptime{$O(n)$}{$O(1)$} problem, so we have proved Therom
+\ref{highest-marked-theorem}.
+
 \section{Answering branch infix regular questions}
 
 With the above problem solved, we are ready to finish our algorithm for branch
@@ -757,6 +772,8 @@ another jump down. Handling each jump takes constant time, and the number of
 jumps is bounded by $|Q|$ since we can only jump to a lower color. Thus we can
 answer branch infix regular questions in time constant with respect to $|T|$.
 
+This finishes the proof of Theorem \ref{branch-infix-theorem}.
+
 \chapter{MSO Query Answering on Trees}\label{mso-query-answering}
 
 Now we have all the pieces necessary to present our main result, which we
@@ -764,9 +781,7 @@ can formulate as Theorem \ref{mso-query-answering-theorem}:
 
 \begin{theorem}\label{mso-query-answering-theorem}
     Problem \ref{mso-query-answering-problem} can be solved in time
-    \qptime{$O_{\varphi}(n)$}{$O_{\varphi}(m \log m)$}. Furthermore, time
-    complexity with respect to the size of the tree automaton is exponential in
-    both the preprocessing and question answering phases.
+    \qptime{$O_{\varphi}(n)$}{$O_{\varphi}(m \log m)$}.
 \end{theorem}
 
 First, let's reduce Problem \ref{mso-query-answering-problem} to Problem
@@ -824,7 +839,9 @@ This concludes the proof of the lemma, and Theorem
 
 \begin{theorem}\label{relabel-regular-queries-theorem}
     Problem \ref{relabel-regular-queries} can be solved in time
-    \qptime{$O_A(n)$}{$O_A(m \log m)$}.
+    \qptime{$O_A(n)$}{$O_A(m \log m)$}. Furthermore, time
+    complexity with respect to the size of the tree automaton is exponential in
+    both the preprocessing and question answering phases.
 \end{theorem}
 
 The rest of this chapter is dedicated to proving Theorem