Specify trees as binary

1 files changed, 8 insertions, 8 deletions

diff --git a/mgr.tex b/mgr.tex
index 8ecbc83..5f8e6ab 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -285,11 +285,11 @@ with elements of $Q$ such that
 \end{itemize}
 
 A run is \definedterm{accepting} if $T$'s root gets relabeled to an accepting
-state, that is a state $q \in F$. The set of all trees accepted by an automaton
-$A$ is called the \definedterm{language recognized by $A$}, notated $L(A)$. We
-call the class of all languages recognized by tree automata \definedterm{regular
-tree languages}, analogously to regular languages recognized by finite state
-automata.
+state, that is a state $q \in F$. The set of all binary trees accepted by an
+automaton $A$ is called the \definedterm{language recognized by $A$}, notated
+$L(A)$. We call the class of all languages recognized by tree automata
+\definedterm{regular tree languages}, analogously to regular languages
+recognized by finite state automata.
 
 We note that the expressive power of deterministic bottom-up tree automata is
 the same as that of nondeterministic (either bottom-up or top-down) tree
@@ -316,9 +316,9 @@ $E$.
 We make use of a fundamental theorem tying MSO logic on trees and tree automata:
 
 \begin{theorem}\label{mso-to-automaton}
-    For every MSO formula $\varphi$ over trees, there exists a tree automaton
-    $A$ such that for every tree $T$, $T \models \varphi$ if, and only if $T \in
-    L(A)$.
+    For every MSO formula $\varphi$ over binary trees, there exists a tree
+    automaton $A$ such that for every binary tree $T$, $T \models \varphi$ if,
+    and only if $T \in L(A)$.
 \end{theorem}
 
 We note that the converse of this theorem is also true (i.e. that for every tree