Organize with theorems

1 files changed, 31 insertions, 5 deletions

diff --git a/mgr.tex b/mgr.tex
index 1054211..47c1013 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -647,11 +647,26 @@ infix regular queries in constant time.
 
 \chapter{MSO Query Answering on Trees}\label{mso-query-answering}
 
-We now have all the pieces necessary to present our \qptime{$O(n)$}{$O(m \log
-m)$} algorithm for MSO query answering on trees. We fix an MSO formula
-$\varphi(\vec{X})$ and take a tree $T$ of size $n$. We proceed with several
-reductions so that we end up with needing to solve the relabel regular queries
-problem, which we solve in the remainder of this chapter.
+Now we have all the pieces necessary to present our main result, which we
+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(n)$}{$O(m \log m)$}.
+\end{theorem}
+
+First, let's reduce Problem \ref{mso-query-answering-problem} to Problem
+\ref{relabel-regular-queries}:
+
+\begin{lemma}
+    If Problem \ref{relabel-regular-queries} has an \qptime{$O(n)$}{$O(m \log
+    m)$} solution, then so does Problem \ref{mso-query-answering-problem}.
+\end{lemma}
+
+Proof: We proceed with several standard linear reductions that transform Problem
+\ref{mso-query-answering-problem}, which speaks about MSO formulae with free
+variables, to Problem \ref{relabel-regular-queries}, which talks about tree
+automata over binary trees.
 
 First of all, if $T$ is not binary, we can use a standard encoding to encode it
 inside of a binary tree $T'$, modifying $\varphi$ to $\varphi'$, such that $T
@@ -689,6 +704,17 @@ selecting a specific valuation $\vec{W}$ of $\vec{X}$, thus answering whether or
 not $A$ accepts the relabeled tree is equivalent to answering whether or not $T
 \models \varphi(\vec{W})$.
 
+This concludes the proof of the lemma, and Theorem
+\ref{mso-query-answering-theorem} will be proved if we prove:
+
+\begin{theorem}\label{relabel-regular-queries-theorem}
+    Problem \ref{relabel-regular-queries} can be solved in time
+    \qptime{$O(n)$}{$O(m \log m)$}
+\end{theorem}
+
+The rest of this chapter is dedicated to proving Theorem
+\ref{relabel-regular-queries-theorem}.
+
 \section{Relabel Regular Queries on Trees}
 
 Fix a tree automaton $A$ and take a $\Sigma$-labeled binary tree $T$.