## 4 Boolean Quantifiers Evaluation  
Let \(\phi(x_{1},\ldots,x_{n})\) be an arbitrary CNF formula of the variables \(x_{1},\ldots,x_{n}\). For arbitrary taken quantifiers \(\mathrm{Q}_{l}\in\{\exists,\forall\}\), let \(\phi_{l}(x_{1},\ldots x_{i})\): = \(\mathrm{Q}_{i+1}x_{i+1}\mathrm{Q}_{i+2}x_{i+2}\ldots\mathrm{Q}_{n}x_{n}\mathbf{\phi} (x_{1},\ldots,x_{n})\). In particular, \(\phi_{n}(x_{1},\ldots,x_{n})=\phi(x_{1},\ldots,x_{n})\). Let \(\mathrm{EVAL}_{n}\coloneqq\mathrm{EVAL}_{\mathbf{\phi}}\) built in the previous section. We have already defined \(INIT_{n,a}\): \(=INIT_{a}\) as a coloring of \(\mathrm{EVAL}_{n}\) for every \(a\in\{\mathrm{FALSE},\mathrm{TRUE}\}^{n}\). In the following, for each \(i=n,\,n-1,\ldots,0\), we define inductively an \(\mathrm{EVAL}_{i}\) gadget and its coloring \(INIT_{i,\,a}\) for every \(a\in\{\mathrm{FALSE},\mathrm{TRUE}\}^{i}\). Figure 12 depicts our construction of an \(\mathrm{EVAL}_{i}\) gadget when \(\mathrm{Q}_{i+1}=\forall\), containing an already constructed \(\mathrm{EVAL}_{i+1}\) gadget. We describe the coloring of \(\mathrm{EVAL}_{i}\) by those of the (S&T, S&P, \(\mathrm{CONJ},\mathrm{EVAL}_{i+1}\)) gadgets therein. For \(a\in\{\mathrm{FALSE},\mathrm{TRUE}\}^{i}\) and \(b\in\{\mathrm{FALSE},\mathrm{TRUE}\}\), let \((a,b)=(a_{1},\ldots,a_{i},b)\in\{\mathrm{FALSE},\mathrm{TRUE}\}^{i+1}\). Let \(INIT_{i,\,a}\) be the coloring of \(\mathrm{EVAL}_{i}\) that sets the coloring of the (S&T, S&P, \(\mathrm{CONJ},\mathrm{EVAL}_{i+1}\)) gadgets as \(\left(\mathit{UOFF},\,OFF,\,INIT,\,INIT_{i+1,\,(a,\,\mathrm{FALSE})}\right)\) ; the coloring of the other gadgets are set to be initialized. Then, we denote by \(USED_{i,\,a}\) the coloring derived from \(INIT_{i,\,a}\) by the ant's walking course from the entrance to an exit of \(\mathrm{EVAL}_{i}\). We have already defined \(USED_{n,\,a}\): \(=USED_{a}\). In the following lemma, \(USED_{i,\,a}\) are inductively defined, too. **Lemma 2. ** For every a \(\in\{\mathrm{FALSE},\mathrm{TRUE}\}^{i}\), if the coloring of \(\mathrm{EVAL}_{i}\) is \(INIT_{i,\,a}\) and \(\mathbf{\phi}_{i}(\mathbf{a_{1}},\ldots,\!\!\mathbf{a_{i}})=\mathrm{FALSE}\) (TRUE) then the ant entering to the \(\mathrm{EVAL}_{i}\) gadget at \(IN_{i}\) exits at \(OUT_{i,\,\mathrm{FALSE}}\) (\(OUT_{i,\mathrm{TRUE}}\)). **Proof. ** Lemma 1 proves the \(i=n\) case of Lemma 2. Let \(a\in\{\text{FALSE},\,\text{TRUE}\}^{i}\). By the backward induction hypothesis, Lemma 2 is assumed to hold for both \(\phi_{i+1}(a,\text{FALSE})\) and \(\phi_{i+1}(a,\,\text{TRUE})\). In the following proof, we prove Lemma 2 for \(\phi_{i}(a)\) when \(Q_{i}=Q_{\psi}\). Case 1. Suppose that \(\phi_{i+1}(a,\,\text{FALSE})=\text{FALSE}\). The ant walks as follows (Figure 12-1): \(\mathit{IN}_{i}\to\text{S\&T}\to\mathit{CONJ}\to\mathit{IN}_{i+1}\), changing the coloring of (S\(\&\)T, CONJ) from (\(\mathit{UOFF},\mathit{INIT}\)) to (\(\mathit{OFF},\mathit{USED}_{1}\)) ; next, since the coloring of \(\text{EVAL}_{i+1}\) is \(\mathit{INIT}_{i+1,(a,\,\text{FALSE})}\), by Lemma 2 for \(\phi_{i+1}(a,\,\text{FALSE})\), the ant starting from \(\mathit{IN}_{i+1}\) reaches to \(\mathit{OUT}_{i+1,\text{FALSE}}\), which changes the coloring of \(\text{EVAL}_{i+1}\) from \(\mathit{INIT}_{i+1,\,(a,\,\text{FALSE})}\) to \(\mathit{USED}_{i+1,\,(a,\,\text{FALSE})}\); finally, the ant walks from \(\mathit{OUT}_{i+1,\,\text{FALSE}}\) to \(\mathit{OUT}_{i,\,\text{FALSE}}\). Case 2. Suppose \(\phi_{i+1}(a,\,\text{FALSE})=\text{TRUE}\) and \(\phi_{i+1}(a,\,\text{TRUE})=\text{FALSE}\).