Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
using_automata_to_decide_msol_over_finite_strings [2007/05/16 03:50] vkuncak |
using_automata_to_decide_msol_over_finite_strings [2007/05/16 10:44] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Compare this to [[Using automata to decide Presburger arithmetic]]. | Compare this to [[Using automata to decide Presburger arithmetic]]. | ||
| - | We will define $A(G)$ such that for every $G$ and for all $k \ge k_0$, for every matrix $a_{ij} \in \{0,1\}$ where for $1 \leq i \leq n$ and $1 \leq j \leq k$, | + | We will define $A(G)$ such that for every $G$ and for all $k$, for every matrix $a_{ij} \in \{0,1\}$ where for $1 \leq i \leq n$ and $1 \leq j \leq k$, |
| \begin{equation*} | \begin{equation*} | ||
| [\![G]\!] [v_i \mapsto \{j \mid a_{ij}=1 \}]_{i=1}^n = \mbox{true} | [\![G]\!] [v_i \mapsto \{j \mid a_{ij}=1 \}]_{i=1}^n = \mbox{true} | ||