From 29f5d0b9c55179a60590d34953127cf8e0f19059 Mon Sep 17 00:00:00 2001 From: Marcin Chrzanowski Date: Thu, 16 Dec 2021 17:35:39 +0100 Subject: Style --- mgr.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/mgr.tex b/mgr.tex index 86b8a54..15fe64b 100644 --- a/mgr.tex +++ b/mgr.tex @@ -722,10 +722,10 @@ $y$ consider the vertex $y.q$, the unique vertex here of color $c$. If it is in the same connected component as $x'.q_0$ (which we check by comparing $\componenttable[x'.q_0]$ with $\componenttable[y.q]$), we can immediately answer whether or not $A$ will accept the word on this path based on whether -this state is accepting. Indeed, if that is the case then we have not changed -connected components, thus there is a single-color path from $x'.q_0$ down to -$y.q$ and $q$ is indeed the state $A$ would have ended in after running on the -word given by the labels from $x$ down to $y$. +this state is accepting. Indeed, if the two vertices are in the same component +then there is a single-color path from $x'.q_0$ down to $y.q$ and $q$ is indeed +the state $A$ would have ended in after running on the word given by the labels +from $x$ down to $y$. Otherwise, we need to jump down to a lower copy of $Q$. We can find the first such copy where the color on our path changes from $c$ to something lower by @@ -783,7 +783,7 @@ variable $X$ is set to $W$. Now by Theorem \ref{mso-to-automaton}, there is a tree automaton $A$ for binary trees over the alphabet $\{ 0, 1 \}^{\vec{X}}$ which accepts a tree if and only if its labeling corresponds to a model satisfying $\varphi''$. Here a label -$a_1 \ldots a_k$ (where $k = |\vec{X}|$ and each $a_i \in \{ 0, 1 \}$) should be +$b_1 \ldots b_k$ (where $k = |\vec{X}|$ and each $b_i \in \{ 0, 1 \}$) should be interpreted as a bit vector signifying which unary relations $U_X$ a vertex is assigned to. -- cgit v1.2.3