chapter ‹Reducing $\NP$ languages to \SAT{}\label{s:Reducing}› theory Reducing imports Satisfiability Oblivious begin text ‹ We have already shown that \SAT{} is in $\NP$. It remains to show that \SAT{} is $\NP$-hard, that is, that every language $L \in \NP$ can be polynomial-time reduced to \SAT{}. This, in turn, can be split in two parts. First, showing that for every $x$ there is a CNF formula $\Phi$ such that $x\in L$ iff.\ $\Phi$ is satisfiable. Second, that $\Phi$ can be computed from $x$ in polynomial time. This chapter is devoted to the first part, which is the core of the proof. In the subsequent two chapters we painstakingly construct a polynomial-time Turing machine computing $\Phi$ from $x$ in order to show something that is usually considered ``obvious''. The proof corresponds to lemma~2.11 from the textbook~\cite{ccama}. Of course we have to be much more explicit than the textbook, and the first section describes in some detail how we derive the formula $\Phi$. › section ‹Introduction› text ‹ Let $L \in \NP$. In order to reduce $L$ to \SAT{}, we need to construct for every string $x\in\bbOI^*$ a CNF formula $\Phi$ such that $x\in L$ iff.\ $\Phi$ is satisfiable. In this section we describe how $\Phi$ looks like. \subsection{Preliminaries} We denote the length of a string $s\in\bbOI^*$ by $|s|$. We define \[ num(s) = \left\{\begin{array}{ll} k & \text{if } s = \bbbI^k\bbbO^{|s|-k},\\ |s| + 1 & \text{otherwise.} \end{array}\right. \] Essentially $num$ interprets some strings as unary codes of numbers. All other strings are interpreted as an ``error value''. For a string $s$ and a sequence $w\in\nat^n$ of numbers we write $s(w)$ for $num(s_{w_0}\dots s_{w_{n-1}})$. Likewise for an assignment $\alpha\colon \nat \to \bbOI$ we write $\alpha(w) = num(\alpha(w_0)\dots\alpha(w_{n-1}))$. We define two families of CNF formulas. Variables are written $v_0, v_1, v_2, \dots$, and negated variables are written $\bar v_0, \bar v_1, \bar v_2, \dots$ Let $w\in\nat^n$ be a list of numbers. For $k \leq n$ define \[ \Psi(w, k) = \bigwedge_{i=0}^{k-1} v_{w_i} \land \bigwedge_{i=k}^{n - 1} \bar v_{w_i}. \] This formula is satisfied by an assignment $\alpha$ iff.\ $\alpha(w) = k$. In a similar fashion we define for $n > 2$, \[ \Upsilon(w) = v_{w_0} \land v_{w_1} \land \bigwedge_{i=3}^{n - 1} \bar v_{w_i}, \] which is satisfied by an assignment $\alpha$ iff.\ $\alpha(w) \in \{2, 3\} = \{\mathbf{0}, \mathbf{1}\}$, where as usual the boldface $\mathbf{0}$ and $\mathbf{1}$ refer to the symbols represented by the numbers~2 and~3. For $a \leq b$ we write $[a:b]$ for the interval $[a, \dots, b - 1] \in \nat^{b - a}$. For intervals the CNF formulas become: \[ \Psi([a:b], k) = \bigwedge_{i=a}^{a+k-1} v_i \land \bigwedge_{i=a+k}^{b - 1} \bar v_i \qquad \text{and} \qquad \Upsilon([a:b]) = v_a \land v_{a+1} \land \bigwedge_{i=a+3}^{b - 1} \bar v_i. \] Let $\phi$ be a CNF formula and let $\sigma\in\nat^*$ be a sequence of variable indices such that for all variables $v_i$ occurring in $\phi$ we have $i < |\sigma|$. Then we define the CNF formula $\sigma(\phi)$ as the formula resulting from replacing every variable $v_i$ in $\phi$ by the variable $v_{\sigma_i}$. This corresponds to our function @{const relabel}. \subsection{Construction of the CNF formula} Let $M$ be the two-tape oblivious verifier Turing machine for $L$ from lemma~@{text NP_imp_oblivious_2tape}. Let $p$ be the polynomial function for the length of the certificates, and let $T\colon \nat \to \nat$ be the polynomial running-time bound. Let $G$ be $M$'s alphabet size. Let $x\in\bbOI^n$ be fixed thoughout the rest of this section. We seek a CNF formula $\Phi$ that is satisfiable iff.\ $x\in L$. We are going to transform ``$x\in L$'' via several equivalent statements to the statement ``$\Phi$ is satisfiable'' for a suitable $\Phi$ defined along the way. The Isabelle formalization later in this chapter does not prove these equivalences explicitly. They are only meant to explain the shape of $\Phi$. \subsubsection{1st equivalence} From lemma~@{text NP_imp_oblivious_2tape} about $M$ we get the first equivalent statement: There exists a certificate $u \in \bbOI^{p(n)}$ such that $M$ on input $\langle x, u\rangle$ halts with the symbol \textbf{1} under its output tape head. The running time of $M$ is bounded by $T(|\langle x, u\rangle|) = T(2n+2+2p(n))$. We abbreviate $|\langle x, u\rangle| = 2n+2+2p(n)$ by $m$. \subsubsection{2nd equivalence} For the second equivalent statement, we define what the textbook calls ``snapshots''. For every $u\in\{\bbbO,\bbbI\}^{p(n)}$ let $z_0^u(t)$ be the symbol under the input tape head of $M$ on input $\langle x, u\rangle$ at step $t$. Similarly we define $z_1^u(t)$ as the symbol under the output tape head of $M$ at step $t$ and $z_2^u(t)$ as the state $M$ is in at step $t$. A triple $z^u(t) = (z^u_0(t), z^u_1(t), z^u_2(t))$ is called a snapshot. For the initial snapshot we have: \begin{equation} z_0^u(0) = z_1^u(0) = \triangleright\qquad\text{and}\qquad z_2^u(0) = 0. \tag{Z0} \end{equation} The crucial idea is that the snapshots for $t > 0$ can be characterized recursively using two auxiliary functions $\inputpos$ and $\prev$. Since $M$ is oblivious, the positions of the tape heads on input $\langle x, u\rangle$ after $t$ steps are the same for all $u$ of length $p(n)$. We denote the input head positions by $\inputpos(t)$. For every $t$ we denote by $\prev(t)$ the last step before $t$ in which the output tape head of $M$ was in the same cell as in step $t$. Due to $M$'s obliviousness this is again the same for all $u$ of length $p(n)$. If there is no such previous step, because $t$ is the first time the cell is reached, we set $\prev(t) = t$. (This deviates from the textbook, which sets $\prev(t) = 1$.) In the other case we have $\prev(t) < t$. Also due to $M$'s obliviousness, the halting time on input $\langle x, u\rangle$ is the same for all $u$ of length $p(n)$, and we denote it by $T' \le T(|\langle x, u\rangle|)$. Thus we have $\inputpos(t) \le T'$ for all $t$. If we define the symbol sequence $y(u) = \triangleright \langle x, u\rangle \Box^{T'}$, the first component of the snapshots is, for arbitrary $t$: \begin{equation} z_0^u(t) = y(u)_{\inputpos(t)}. \tag{Z1} \end{equation} Next we consider the snapshot components $z_1^u(t)$ for $t > 0$. First consider the case $\prev(t) < t$; that is, the last time before $t$ when $M$'s output tape head was in the same cell as in step $t$ was in step $\prev(t)$. The snapshot for step $\prev(t)$ has exactly the information needed to calculate the actions of $M$ at step $t$: the symbols read from both tapes and the state which $M$ is in. In some sort of hybrid notation: \begin{equation} z_1^u(t) = (M\ !\ z_2^u(\prev(t)))\ [z_0^u(\prev(t)), z_1^u(\prev(t))]\ [.]\ 1. \tag{Z2} \end{equation} In the other case, $\prev(t) = t$, the output tape head has not been in this cell before and is thus reading a blank. It cannot be reading the start symbol because the output tape head was in cell zero at step $t = 0$ already. Formally: \begin{equation} z_1^u(t) = \Box. \tag{Z3} \end{equation} The state $z_2^u(t)$ for $t > 0$ can be computed from the state $z_2^u(t-1)$ in the previous step and the symbols $z_0^u(t-1)$ and $z_1^u(t-1)$ read in the previous step: \begin{equation} z_2^u(t) = \mathit{fst}\ ((M\ !\ z_2^u(t - 1))\ [z_0^u(t - 1), z_1^u(t - 1)]). \tag{Z4} \end{equation} For a string $u\in\bbOI^{p(n)}$ the equations (Z0) -- (Z4) uniquely determine all the $z^u(0), \dots, z^u(T')$. Conversely, the snapshots for $u$ satisfy all the equations. Therefore the equations characterize the sequence of snapshots. The condition that $M$ halts with the output tape head on \textbf{1} can be expressed with snapshots: \begin{equation} z_1^{u}(T') = \mathbf{1}. \tag{Z5} \end{equation} This yields our second equivalent statement: $x\in L$ iff.\ there is a $u\in\{\bbbO,\bbbI\}^{p(n)}$ and a sequence $z^u(0), \dots, z^u(T')$ satisfying the equations (Z0) -- (Z5). \subsubsection{3rd equivalence} The length of $y(u)$ is $m' := m + 1 + T' = 3 + 2n + 2p(n) + T'$ because $|\langle x, u\rangle| = m$ plus the start symbol plus the $T'$ blanks. For the next equivalence we observe that the strings $y(u)$ for $u\in\{\bbbO,\bbbI\}^{p(n)}$ can be characterized as follows. Consider a predicate on strings $y$: \begin{itemize} \item[(Y0)] $|y| = m'$; \item[(Y1)] $y_0 = \triangleright$ (the start symbol); \item[(Y2)] $y_{2n+1} = y_{2n+2} = \mathbf{1}$ (the separator in the pair encoding); \item[(Y3)] $y_{2i+1} = \mathbf{0}$ for $i=0,\dots,n-1$ (the zeros before $x$); \item[(Y4)] $y_{2n+2+2i+1} = \mathbf{0}$ for $i=0, \dots, p(n)-1$ (the zeros before $u$); \item[(Y5)] $y_{2n+2p(n)+3+i} = \Box$ for $i=0, \dots, T' - 1$ (the blanks after the input proper); \item[(Y6)] $y_{2i+2} = \left\{\begin{array}{ll} \mathbf{0} & \text{if } x_i = \bbbO,\\ \mathbf{1} & \text{otherwise} \end{array}\right.$ for $i = 0, \dots, n - 1$ (the bits of $x$); \item[(Y7)] $y_{2n+4+2i} \in \{\mathbf{0}, \mathbf{1}\}$ for $i=0,\dots,p(n)-1$ (the bits of $u$). \end{itemize} Every $y(u)$ for some $u$ of length $p(n)$ satisfies this predicate. Conversely, from a $y$ satisfying the predicate, a $u$ of length $p(n)$ can be extracted such that $y = y(u)$. From that we get the third equivalent statement: $x \in L$ iff.\ there is a $y \in \{0, \dots, G - 1\}^{m'}$ with (Y0) -- (Y7) and a sequence $z^u(0), \dots, z^u(T')$ with (Z0) -- (Z5). \subsubsection{4th equivalence} Each element of $y$ is a symbol from $M$'s alphabet, that is, a number less than $G$. The same goes for the first two elements of each snapshot, $z_0^u(t)$ and $z_1^u(t)$. The third element, $z_2^u(t)$, is a number less than or equal to the number of states of $M$. Let $H$ be the maximum of $G$ and the number of states. Every element of $y$ and of the snapshots can then be represented by a bit string of length $H$ using $num$ (the textbook uses binary, but unary is simpler for us). So we use $3H$ bits to represent one snapshot. There are $T' + 1$ snapshots until $M$ halts. Thus all elements of all snapshots can be represented by a string of length $3H\cdot(T'+1)$. Together with the string of length $N := H\cdot m'$ for the input tape contents $y$, we have a total length of $N + 3H\cdot(T'+1)$. The equivalence can thus be stated as $x \in L$ iff.\ there is a string $s\in \{\bbbO,\bbbI\}^{N + 3H\cdot(T'+1)}$ with certain properties. To write these properties we introduce some intervals: \begin{itemize} \item $\gamma_i = [iH : (i+1)H]$ for $i < m'$, \item $\zeta_0(t) = [N + 3Ht : N+3Ht + H]$ for $t \leq T'$, \item $\zeta_1(t) = [N + 3Ht + H : N+3Ht + 2H]$ for $t \leq T'$, \item $\zeta_2(t) = [N + 3Ht + 2H : N+3H(t + 1)]$ for $t \leq T'$. \end{itemize} These intervals slice the string $s$ in intervals of length $H$. The string $s$ must satisfy properties analogous to (Y0) -- (Y7), which we express using the intervals $\gamma_i$: \begin{itemize} \item[(Y0)] $|s| = N + 3H(T' + 1)$ \item[(Y1)] $s(\gamma_0) = \triangleright$ (the start symbol); \item[(Y2)] $s(\gamma_{2n+1}) = s(\gamma_{2n+2}) = \mathbf{1}$ (the separator in the pair encoding); \item[(Y3)] $s(\gamma_{2i+1}) = \mathbf{0}$ for $i=0,\dots,n-1$ (the zeros before $x$); \item[(Y4)] $s(\gamma_{2n+2+2i+1}) = \mathbf{0}$ for $i=0,\dots,p(n)-1$ (the zeros before $u$); \item[(Y5)] $s(\gamma_{2n+2p(n)+3+i}) = \Box$ for $i=0,\dots,T' - 1$ (the blanks after the input proper); \item[(Y6)] $s(\gamma_{2i+2}) = \left\{\begin{array}{ll} \mathbf{0} & \text{if } x_i = \bbbO,\\ \mathbf{1} & \text{otherwise} \end{array}\right.$ for $i = 0, \dots, n - 1$ (the bits of $x$); \item[(Y7)] $s(\gamma_{2n+4+2i}) \in \{\mathbf{0}, \mathbf{1}\}$ for $i=0,\dots,p(n)-1$ (the bits of $u$). \end{itemize} Moreover the string $s$ must satisfy (Z0) -- (Z5). For these properties we use the $\zeta$ intervals. \begin{itemize} \item[(Z0)] $s(\zeta_0(0)) = s(\zeta_1(0)) = \triangleright$ and $s(\zeta_2(0)) = 0$, \item[(Z1)] $s(\zeta_0(t)) = s(\gamma_{\inputpos(t)})$ for $t = 1, \dots, T'$, \item[(Z2)] $s(\zeta_1(t)) = (M\ !\ s(\zeta_2(\prev(t)))\ [s(\zeta_0(\prev(t))), s(\zeta_1(\prev(t)))]\ [.]\ 1$ for $t = 1, \dots, T'$ with $\prev(t) < t$, \item[(Z3)] $s(\zeta_1(t)) = \Box$ for $t = 1, \dots, T'$ with $\prev(t) = t$, \item[(Z4)] $s(\zeta_2(t)) = \mathit{fst}\ ((M\ !\ s(\zeta_2(t - 1))\ [s(\zeta_0(t - 1), s(\zeta_1(t - 1)])$ for $t = 1, \dots, T'$, \item[(Z5)] $s(\zeta_1(T')) = \mathbf{1}$. \end{itemize} \subsubsection{5th equivalence} An assignment is an infinite bit string. For formulas over variables with indices in the interval $[0 : N+3H(T'+1)]$, only the initial $N+3H(T'+1)$ bits of the assignment are relevant. If we had a CNF formula $\Phi$ over these variables that is satisfied exactly by the assignments $\alpha$ for which there is an $s$ with the above properties and $\alpha(i) = s_i$ for all $i < |s|$, then the existence of such an $s$ would be equivalent to $\Phi$ being satisfiable. Next we construct such a CNF formula. Most properties are easy to translate using the formulas $\Psi$ and $\Upsilon$. For example, $s(\gamma_0) = \triangleright$ corresponds to $\alpha(\gamma_0) = \triangleright$. A formula that is satisfied exactly by assignments with this property is $\Psi(\gamma_0, 1)$. Likewise the property $s(\gamma_{2n+4+2i})\in\{\mathbf{0}, \mathbf{1}\}$ corresponds to the CNF formula $\Upsilon(\gamma_{2n+4+2i})$. Property (Y0) corresponds to $\Phi$ having only variables $0, \dots, N+3H(T'+1) - 1$. The other (Y$\cdot$) properties become: \begin{itemize} \item[(Y1)] $\Phi_1 := \Psi(\gamma_0, 1)$, \item[(Y2)] $\Phi_2 := \Psi(\gamma_{2n+1}, 3) \land \Psi(\gamma_{2n+2}, 3)$, \item[(Y3)] $\Phi_3 := \bigwedge_{i=0}^{n-1}\Psi(\gamma_{2i+1}, 2)$, \item[(Y4)] $\Phi_4 := \bigwedge_{i=0}^{p(n) - 1}\Psi(\gamma_{2n+2+2i+1}, 2)$, \item[(Y5)] $\Phi_5 := \bigwedge_{i=0}^{T' - 1}\Psi(\gamma_{2n+2p(n)+3+i}, 0)$, \item[(Y6)] $\Phi_6 := \bigwedge_{i=0}^{n - 1}\Psi(\gamma_{2i+2}, x_i + 2)$, \item[(Y7)] $\Phi_7 := \bigwedge_{i=0}^{p(n) - 1}\Upsilon(\gamma_{2n+4+2i})$. \end{itemize} Property~(Z0) and property~(Z5) become these formulas: \begin{itemize} \item[(Z0)] $\Phi_0 := \Psi(\zeta_0(0), 1) \land \Psi(\zeta_1(0), 1) \land \Psi(\zeta_2(0), 0)$, \item[(Z5)] $\Phi_8 := \Psi(\zeta_1(T'), 3)$. \end{itemize} The remaining properties (Z1) -- (Z4) are more complex. They apply to $t = 1, \dots T'$. Let us first consider the case $\prev(t) < t$. With $\alpha$ for $s$ the properties become: \begin{itemize} \item[(Z1)] $\alpha(\zeta_0(t)) = \alpha(\gamma_{\inputpos(t)})$, \item[(Z2)] $\alpha(\zeta_1(t)) = ((M\ !\ \alpha(\zeta_2(\prev(t))))\ [\alpha(\zeta_0(\prev(t))), \alpha(\zeta_1(\prev(t)))])\ [.]\ 1$, \item[(Z4)] $\alpha(\zeta_2(t)) = \mathit{fst}\ ((M\ !\ \alpha(\zeta_2(t-1)))\ [\alpha(\zeta_0(t-1)), \alpha(\zeta_1(t-1))])$. \end{itemize} For any $t$ the properties (Z1), (Z2), (Z4) use at most $10H$ variable indices, namely all the variable indices in the nine $\zeta$'s and in $\gamma_{\inputpos(t)}$, each of which have $H$ indices. Now if the set of all these variable indices was $\{0, \dots, 10H - 1\}$ we could apply lemma~@{thm [source] depon_ex_formula} to get a CNF formula $\psi$ over these variables that ``captures the spirit'' of the properties. We would then merely have to relabel the formula with the actual variable indices we need for each $t$. More precisely, let $w_i = [iH : (i+1)H]$ for $i = 0, \dots, 9$ and consider the following criterion for $\alpha$ on the variable indices $\{0, \dots 10H - 1\}$: \begin{itemize} \item[($\mathrm{F}_1$)] $\alpha(w_6) = \alpha(w_9)$, \item[($\mathrm{F}_2$)] $\alpha(w_7) = ((M\ !\ \alpha(w_5))\ [\alpha(w_3), \alpha(w_4)])\ [.]\ 1,$ \item[($\mathrm{F}_3$)] $\alpha(w_8) = \mathit{fst}\ ((M\ !\ \alpha(w_2))\ [\alpha(w_0), \alpha(w_1)]).$ \end{itemize} Lemma~@{thm [source] depon_ex_formula} gives us a formula $\psi$ satisfied exactly by those assignments $\alpha$ that meet the conditions ($\mathrm{F}_1$), ($\mathrm{F}_2$), ($\mathrm{F}_3$). From this $\psi$ we can create all the formulas we need for representing the properties~(Z1), (Z2), (Z4) by substituting (``relabeling'' in our terminology) the variables $[0,10H)$ appropriately. The substitution for step $t$ is \[ \rho_t = \zeta_0(t-1) \circ \zeta_1(t-1) \circ \zeta_2(t-1) \circ \zeta_0(\prev(t)) \circ \zeta_1(\prev(t)) \circ \zeta_2(\prev(t)) \circ \zeta_0(t) \circ \zeta_1(t) \circ \zeta_2(t) \circ \gamma_{\inputpos(t)}, \] where $\circ$ denotes the concatenation of lists. Then $\rho_t(\psi)$ is CNF formula satisfied exactly by the assignments $\alpha$ satisfying (Z1), (Z2), (Z4). For the case $\prev(t) = t$ we have a criterion on the variable indices $\{0, \dots, 7H - 1\}$: \begin{itemize} \item[($\mathrm{F}_1'$)] $\alpha(w_3) = \alpha(w_6)$, \item[($\mathrm{F}_2'$)] $\alpha(w_4) = \Box$, \item[($\mathrm{F}_3'$)] $\alpha(w_5) = \mathit{fst}\ ((M\ !\ \alpha(w_2))\ [\alpha(w_0), \alpha(w_1)])$, \end{itemize} whence lemma~@{thm [source] depon_ex_formula} supplies us with a formula $\psi'$. With appropriate substitutions \[ \rho'_t = \zeta_0(t-1) \circ \zeta_1(t-1) \circ \zeta_2(t-1) \circ \zeta_0(t) \circ \zeta_1(t) \circ \zeta_2(t) \circ \gamma_{\inputpos(t)}, \] we then define CNF formulas $\chi_t$ for all $t = 1, \dots, T'$: \[ \chi_t = \left\{\begin{array}{ll} \rho_t(\psi) &\text{if }\prev(t) < t,\\ \rho'_t(\psi') &\text{if }\prev(t) = t. \end{array}\right. \] The point of all that is that we can hard-code $\psi$ and $\psi'$ in the TM performing the reduction (to be built in the final chapter) and for each $t$ the TM only needs to construct the substitution $\rho_t$ or $\rho_t'$ and perform the relabeling. Turing machines that perform these operations will be constructed in the next chapter. Since all $\chi_t$ are in CNF, so is the conjunction \[ \Phi_9 := \bigwedge_{t=1}^{T'}\chi_t\ . \] Finally the complete CNF formula is: \[ \Phi := \Phi_0 \land \Phi_1 \land \Phi_2 \land \Phi_3 \land \Phi_4 \land \Phi_5 \land \Phi_6 \land \Phi_7 \land \Phi_8 \land \Phi_9\ . \] › section ‹Auxiliary CNF formulas› text ‹ In this section we define the CNF formula families $\Psi$ and $\Upsilon$. In the introduction both families were parameterized by intervals of natural numbers. Here we generalize the definition to allow arbitrary sequences of numbers although we will not need this generalization. › text ‹ The number of variables set to true in a list of variables: › definition numtrue :: "assignment ⇒ nat list ⇒ nat" where "numtrue α vs ≡ length (filter α vs)" text ‹ Checking whether the list of bits assigned to a list @{term vs} of variables has the form $\bbbI\dots\bbbI\bbbO\dots\bbbO$: › definition blocky :: "assignment ⇒ nat list ⇒ nat ⇒ bool" where "blocky α vs k ≡ ∀i<length vs. α (vs ! i) ⟷ i < k" text ‹ The next function represents the notation $\alpha(\gamma)$ from the introduction, albeit generalized to lists that are not intervals $\gamma$. › definition unary :: "assignment ⇒ nat list ⇒ nat" where "unary α vs ≡ if (∃k. blocky α vs k) then numtrue α vs else Suc (length vs)" lemma numtrue_remap: assumes "∀s∈set seq. s < length σ" shows "numtrue (remap σ α) seq = numtrue α (reseq σ seq)" proof - have *: "length (filter f xs) = length (filter (f ∘ ((!) xs)) [0..<length xs])" for f and xs :: "'a list" using length_filter_map map_nth by metis let ?s_alpha = "remap σ α" let ?s_seq = "reseq σ seq" have "numtrue ?s_alpha seq = length (filter ?s_alpha seq)" using numtrue_def by simp then have lhs: "numtrue ?s_alpha seq = length (filter (?s_alpha ∘ ((!) seq)) [0..<length seq])" using * by auto have "numtrue α ?s_seq = length (filter α ?s_seq)" using numtrue_def by simp then have "numtrue α ?s_seq = length (filter (α ∘ ((!) ?s_seq)) [0..<length ?s_seq])" using * by metis then have rhs: "numtrue α ?s_seq = length (filter (α ∘ ((!) ?s_seq)) [0..<length seq])" using reseq_def by simp have "(?s_alpha ∘ ((!) seq)) i = (α ∘ ((!) ?s_seq)) i" if "i < length seq" for i using assms remap_def reseq_def that by simp then show ?thesis using lhs rhs by (metis atLeastLessThan_iff filter_cong set_upt) qed lemma unary_remap: assumes "∀s∈set seq. s < length σ" shows "unary (remap σ α) seq = unary α (reseq σ seq)" proof - have *: "blocky (remap σ α) seq k = blocky α (reseq σ seq) k" for k using blocky_def remap_def reseq_def assms by simp let ?alpha = "remap σ α" and ?seq = "reseq σ seq" show ?thesis proof (cases "∃k. blocky ?alpha seq k") case True then show ?thesis using * unary_def numtrue_remap assms by simp next case False then have "unary ?alpha seq = Suc (length seq)" using unary_def by simp moreover have "¬ (∃k. blocky α ?seq k)" using False * assms by simp ultimately show ?thesis using unary_def by simp qed qed text ‹ Now we define the family $\Psi$ of CNF formulas. It is parameterized by a list @{term vs} of variable indices and a number $k \leq |\mathit{vs}|$. The formula is satisfied exactly by those assignments that set to true the first $k$ variables in $vs$ and to false the other variables. This is more general than we need, because for us $vs$ will always be an interval. › definition Psi :: "nat list ⇒ nat ⇒ formula" ("Ψ") where "Ψ vs k ≡ map (λs. [Pos s]) (take k vs) @ map (λs. [Neg s]) (drop k vs)" lemma Psi_unary: assumes "k ≤ length vs" and "α ⊨ Ψ vs k" shows "unary α vs = k" proof - have "α ⊨ map (λs. [Pos s]) (take k vs)" using satisfies_def assms Psi_def by simp then have "satisfies_clause α [Pos v]" if "v ∈ set (take k vs)" for v using satisfies_def that by simp then have "satisfies_literal α (Pos v)" if "v ∈ set (take k vs)" for v using satisfies_clause_def that by simp then have pos: "α v" if "v ∈ set (take k vs)" for v using that by simp have "α ⊨ map (λs. [Neg s]) (drop k vs)" using satisfies_def assms Psi_def by simp then have "satisfies_clause α [Neg v]" if "v ∈ set (drop k vs)" for v using satisfies_def that by simp then have "satisfies_literal α (Neg v)" if "v ∈ set (drop k vs)" for v using satisfies_clause_def that by simp then have neg: "¬ α v" if "v ∈ set (drop k vs)" for v using that by simp have "blocky α vs k" proof - have "α (vs ! i)" if "i < k" for i using pos that assms(1) by (metis in_set_conv_nth length_take min_absorb2 nth_take) moreover have "¬ α (vs ! i)" if "i ≥ k" "i < length vs" for i using that assms(1) neg by (metis Cons_nth_drop_Suc list.set_intros(1) set_drop_subset_set_drop subsetD) ultimately show ?thesis using blocky_def by (metis linorder_not_le) qed moreover have "numtrue α vs = k" proof - have "filter α vs = take k vs" using pos neg by (metis (mono_tags, lifting) append.right_neutral append_take_drop_id filter_True filter_append filter_empty_conv) then show ?thesis using numtrue_def assms(1) by simp qed ultimately show ?thesis using unary_def by auto qed text ‹ We will only ever consider cases where $k \leq |vs|$. So we can use $blocky$ to show that an assignment satisfies a $\Psi$ formula. › lemma satisfies_Psi: assumes "k ≤ length vs" and "blocky α vs k" shows "α ⊨ Ψ vs k" proof - have "α ⊨ map (λs. [Pos s]) (take k vs)" (is "α ⊨ ?phi") proof - { fix c :: clause assume c: "c ∈ set ?phi" then obtain s where "c = [Pos s]" and "s ∈ set (take k vs)" by auto then obtain i where "i < k" and "s = vs ! i" using assms(1) by (smt (verit, best) in_set_conv_nth le_antisym le_trans nat_le_linear nat_less_le nth_take nth_take_lemma take_all_iff) then have "c = [Pos (vs ! i)]" using `c = [Pos s]` by simp moreover have "i < length vs" using assms(1) `i < k` by simp ultimately have "α (vs ! i)" using assms(2) blocky_def ‹i < k› by blast then have "satisfies_clause α c" using satisfies_clause_def by (simp add: ‹c = [Pos (vs ! i)]›) } then show ?thesis using satisfies_def by simp qed moreover have "α ⊨ map (λs. [Neg s]) (drop k vs)" (is "α ⊨ ?phi") proof - { fix c :: clause assume c: "c ∈ set ?phi" then obtain s where "c = [Neg s]" and "s ∈ set (drop k vs)" by auto then obtain j where "j < length vs - k" and "s = drop k vs ! j" by (metis in_set_conv_nth length_drop) define i where "i = j + k" then have "i ≥ k" and "s = vs ! i" by (auto simp add: ‹s = drop k vs ! j› add.commute assms(1) i_def) then have "c = [Neg (vs ! i)]" using `c = [Neg s]` by simp moreover have "i < length vs" using assms(1) using ‹j < length vs - k› i_def by simp ultimately have "¬ α (vs ! i)" using assms(2) blocky_def[of α vs k] i_def by simp then have "satisfies_clause α c" using satisfies_clause_def by (simp add: ‹c = [Neg (vs ! i)]›) } then show ?thesis using satisfies_def by simp qed ultimately show ?thesis using satisfies_def Psi_def by auto qed lemma blocky_imp_unary: assumes "k ≤ length vs" and "blocky α vs k" shows "unary α vs = k" using assms satisfies_Psi Psi_unary by simp text ‹ The family $\Upsilon$ of CNF formulas also takes as parameter a list of variable indices. › definition Upsilon :: "nat list ⇒ formula" ("Υ") where "Υ vs ≡ map (λs. [Pos s]) (take 2 vs) @ map (λs. [Neg s]) (drop 3 vs)" text ‹ For $|\mathit{vs}| > 2$, an assignment satisfies $\Upsilon(\mathit{vs})$ iff.\ it satisfies $\Psi(\mathit{vs}, 2)$ or $\Psi(\mathit{vs}, 3)$. › lemma Psi_2_imp_Upsilon: fixes α :: assignment assumes "α ⊨ Ψ vs 2" and "length vs > 2" shows "α ⊨ Υ vs" proof - have "α ⊨ map (λs. [Pos s]) (take 2 vs)" using assms Psi_def satisfies_def by simp moreover have "α ⊨ map (λs. [Neg s]) (drop 3 vs)" using assms Psi_def satisfies_def by (smt (z3) Cons_nth_drop_Suc One_nat_def Suc_1 Un_iff insert_iff list.set(2) list.simps(9) numeral_3_eq_3 set_append) ultimately show ?thesis using Upsilon_def satisfies_def by auto qed lemma Psi_3_imp_Upsilon: assumes "α ⊨ Ψ vs 3" and "length vs > 2" shows "α ⊨ Υ vs" proof - have "α ⊨ map (λs. [Pos s]) (take 2 vs)" using assms Psi_def satisfies_def by (metis eval_nat_numeral(3) map_append satisfies_append(1) take_Suc_conv_app_nth) moreover have "α ⊨ map (λs. [Neg s]) (drop 3 vs)" using assms Psi_def satisfies_def by simp ultimately show ?thesis using Upsilon_def satisfies_def by auto qed lemma Upsilon_imp_Psi_2_or_3: assumes "α ⊨ Υ vs" and "length vs > 2" shows "α ⊨ Ψ vs 2 ∨ α ⊨ Ψ vs 3" proof - have "α ⊨ map (λs. [Pos s]) (take 2 vs)" using satisfies_def assms Upsilon_def by simp then have "satisfies_clause α [Pos v]" if "v ∈ set (take 2 vs)" for v using satisfies_def that by simp then have "satisfies_literal α (Pos v)" if "v ∈ set (take 2 vs)" for v using satisfies_clause_def that by simp then have 1: "α v" if "v ∈ set (take 2 vs)" for v using that by simp then have 2: "satisfies_clause α [Pos v]" if "v ∈ set (take 2 vs)" for v using that satisfies_clause_def by simp have "α ⊨ map (λs. [Neg s]) (drop 3 vs)" using satisfies_def assms Upsilon_def by simp then have "satisfies_clause α [Neg v]" if "v ∈ set (drop 3 vs)" for v using satisfies_def that by simp then have "satisfies_literal α (Neg v)" if "v ∈ set (drop 3 vs)" for v using satisfies_clause_def that by simp then have 3: "¬ α v" if "v ∈ set (drop 3 vs)" for v using that by simp then have 4: "satisfies_clause α [Neg v]" if "v ∈ set (drop 3 vs)" for v using that satisfies_clause_def by simp show ?thesis proof (cases "α (vs ! 2)") case True then have "α v" if "v ∈ set (take 3 vs)" for v using that 1 assms(2) by (metis (no_types, lifting) in_set_conv_nth le_simps(3) length_take less_imp_le_nat linorder_neqE_nat min_absorb2 not_less_eq nth_take numeral_One numeral_plus_numeral plus_1_eq_Suc semiring_norm(3)) then have "satisfies_clause α [Pos v]" if "v ∈ set (take 3 vs)" for v using that satisfies_clause_def by simp then have "α ⊨ Ψ vs 3" using 4 Psi_def satisfies_def by auto then show ?thesis by simp next case False then have "¬ α v" if "v ∈ set (drop 2 vs)" for v using that 3 assms(2) by (metis Cons_nth_drop_Suc numeral_plus_numeral numerals(1) plus_1_eq_Suc semiring_norm(3) set_ConsD) then have "satisfies_clause α [Neg v]" if "v ∈ set (drop 2 vs)" for v using that satisfies_clause_def by simp then have "α ⊨ Ψ vs 2" using 2 Psi_def satisfies_def by auto then show ?thesis by simp qed qed lemma Upsilon_unary: assumes "α ⊨ Υ vs" and "length vs > 2" shows "unary α vs = 2 ∨ unary α vs = 3" using assms Upsilon_imp_Psi_2_or_3 Psi_unary by fastforce section ‹The functions $\inputpos$ and $\prev$› text ‹ Sequences of the symbol~\textbf{0}: › definition zeros :: "nat ⇒ symbol list" where "zeros n ≡ string_to_symbols (replicate n 𝕆)" lemma length_zeros [simp]: "length (zeros n) = n" using zeros_def by simp lemma bit_symbols_zeros: "bit_symbols (zeros n)" using zeros_def by simp lemma zeros: "zeros n = replicate n 𝟬" using zeros_def by simp text ‹ The assumptions in the following locale are the conditions that according to lemma~@{text NP_imp_oblivious_2tape} hold for all $\NP$ languages. The construction of $\Phi$ will take place inside this locale, which in later chapters will be extended to contain the Turing machine outputting $\Phi$ and the correctness proof for this Turing machine. › locale reduction_sat = fixes L :: language fixes M :: machine and G :: nat and T p :: "nat ⇒ nat" assumes T: "big_oh_poly T" assumes p: "polynomial p" assumes tm_M: "turing_machine 2 G M" and oblivious_M: "oblivious M" and T_halt: "⋀y. bit_symbols y ⟹ fst (execute M (start_config 2 y) (T (length y))) = length M" and cert: "⋀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ execute M (start_config 2 ⟨x; u⟩) (T (length ⟨x; u⟩)) <.> 1 = 𝟭)" begin text ‹ The value $H$ is an upper bound for the number of states of $M$ and the alphabet size of $M$. › definition H :: nat where "H ≡ max G (length M)" lemma H_ge_G: "H ≥ G" using H_def by simp lemma H_gr_2: "H > 2" using H_def tm_M turing_machine_def by auto lemma H_ge_3: "H ≥ 3" using H_gr_2 by simp lemma H_ge_length_M: "H ≥ length M" using H_def by simp text ‹ The number of symbols used for encoding one snapshot is $Z = 3H$: › definition Z :: nat where "Z ≡ 3 * H" text ‹ The configuration after running $M$ on input $y$ for $t$ steps: › abbreviation exc :: "symbol list ⇒ nat ⇒ config" where "exc y t ≡ execute M (start_config 2 y) t" text ‹ The function $T$ is just some polynomial upper bound for the running time. The next function, $TT$, is the actual running time. Since $M$ is oblivious, its running time depends only on the length of the input. The argument @{term "zeros n"} is thus merely a placeholder for an arbitrary symbol sequence of length $n$. › definition TT :: "nat ⇒ nat" where "TT n ≡ LEAST t. fst (exc (zeros n) t) = length M" lemma TT: "fst (exc (zeros n) (TT n)) = length M" proof - let ?P = "λt. fst (exc (zeros n) t) = length M" have "?P (T n)" using T_halt bit_symbols_zeros length_zeros by metis then show ?thesis using wellorder_Least_lemma[of ?P] TT_def by simp qed lemma TT_le: "TT n ≤ T n" using wellorder_Least_lemma length_zeros TT_def T_halt[OF bit_symbols_zeros[of n]] by fastforce lemma less_TT: "t < TT n ⟹ fst (exc (zeros n) t) < length M" proof - assume "t < TT n" then have "fst (exc (zeros n) t) ≠ length M" using TT_def not_less_Least by auto moreover have "fst (exc (zeros n) t) ≤ length M" for t using tm_M start_config_def turing_machine_execute_states by auto ultimately show "fst (exc (zeros n) t) < length M" using less_le by blast qed lemma oblivious_halt_state: assumes "bit_symbols zs" shows "fst (exc zs t) < length M ⟷ fst (exc (zeros (length zs)) t) < length M" proof - obtain e where e: "∀zs. bit_symbols zs ⟶ (∃tps. trace M (start_config 2 zs) (e (length zs)) (length M, tps))" using oblivious_M oblivious_def by auto let ?es = "e (length zs)" have "∀i<length ?es. fst (exc zs i) < length M" using trace_def e assms by simp moreover have "fst (exc zs (length ?es)) = length M" using trace_def e assms by auto moreover have "∀i<length ?es. fst (exc (zeros (length zs)) i) < length M" using length_zeros bit_symbols_zeros trace_def e by simp moreover have "fst (exc (zeros (length zs)) (length ?es)) = length M" using length_zeros bit_symbols_zeros trace_def e assms by (smt (verit, ccfv_SIG) fst_conv) ultimately show ?thesis by (metis (no_types, lifting) execute_after_halting_ge le_less_linear) qed corollary less_TT': assumes "bit_symbols zs" and "t < TT (length zs)" shows "fst (exc zs t) < length M" using assms oblivious_halt_state less_TT by simp corollary TT': assumes "bit_symbols zs" shows "fst (exc zs (TT (length zs))) = length M" using assms TT oblivious_halt_state by (metis (no_types, lifting) fst_conv start_config_def start_config_length less_le tm_M turing_machine_execute_states zero_le zero_less_numeral) lemma exc_TT_eq_exc_T: assumes "bit_symbols zs" shows "exc zs (TT (length zs)) = exc zs (T (length zs))" using execute_after_halting_ge[OF TT'[OF assms] TT_le] by simp text ‹ The position of the input tape head of $M$ depends only on the length $n$ of the input and the step $t$, at least as long as the input is over the alphabet $\{\mathbf{0}, \mathbf{1}\}$. › definition inputpos :: "nat ⇒ nat ⇒ nat" where "inputpos n t ≡ exc (zeros n) t <#> 0" lemma inputpos_oblivious: assumes "bit_symbols zs" shows "exc zs t <#> 0 = inputpos (length zs) t" proof - obtain e where e: "(∀zs. bit_symbols zs ⟶ (∃tps. trace M (start_config 2 zs) (e (length zs)) (length M, tps)))" using oblivious_M oblivious_def by auto let ?es = "e (length zs)" obtain tps where t1: "trace M (start_config 2 zs) ?es (length M, tps)" using e assms by auto let ?zs = "(replicate (length zs) 2)" have "proper_symbols ?zs" by simp moreover have "length ?zs = length zs" by simp ultimately obtain tps0 where t0: "trace M (start_config 2 ?zs) ?es (length M, tps0)" using e by fastforce have le: "exc zs t <#> 0 = inputpos (length zs) t" if "t ≤ length ?es" for t proof (cases "t = 0") case True then show ?thesis by (simp add: start_config_def inputpos_def) next case False then obtain i where i: "Suc i = t" using gr0_implies_Suc by auto then have "exc zs (Suc i) <#> 0 = fst (?es ! i)" using t1 False that Suc_le_lessD trace_def by auto moreover have "exc ?zs (Suc i) <#> 0 = fst (?es ! i)" using t0 False i that Suc_le_lessD trace_def by auto ultimately show ?thesis using i inputpos_def zeros by simp qed moreover have "exc zs t <#> 0 = inputpos (length zs) t" if "t > length ?es" proof - have "exc ?zs (length ?es) = (length M, tps0)" using t0 trace_def by simp then have *: "exc ?zs t = exc ?zs (length ?es)" using that by (metis execute_after_halting_ge fst_eqD less_or_eq_imp_le) have "exc zs (length ?es) = (length M, tps)" using t1 trace_def by simp then have "exc zs t = exc zs (length ?es)" using that by (metis execute_after_halting_ge fst_eqD less_or_eq_imp_le) then show ?thesis using * le[of "length ?es"] by (simp add: inputpos_def zeros) qed ultimately show ?thesis by fastforce qed text ‹ The position of the tape head on the output tape of $M$ also depends only on the length $n$ of the input and the step $t$. › lemma oblivious_headpos_1: assumes "bit_symbols zs" shows "exc zs t <#> 1 = exc (zeros (length zs)) t <#> 1" proof - obtain e where e: "(∀zs. bit_symbols zs ⟶ (∃tps. trace M (start_config 2 zs) (e (length zs)) (length M, tps)))" using oblivious_M oblivious_def by auto let ?es = "e (length zs)" obtain tps where t1: "trace M (start_config 2 zs) ?es (length M, tps)" using e assms by auto let ?zs = "(replicate (length zs) 2)" have "proper_symbols ?zs" by simp moreover have "length ?zs = length zs" by simp ultimately obtain tps0 where t0: "trace M (start_config 2 ?zs) ?es (length M, tps0)" using e by fastforce have le: "exc zs t <#> 1 = exc (zeros (length zs)) t <#> 1" if "t ≤ length ?es" for t proof (cases "t = 0") case True then show ?thesis by (simp add: start_config_def inputpos_def) next case False then obtain i where i: "Suc i = t" using gr0_implies_Suc by auto then have "exc zs (Suc i) <#> 1 = snd (?es ! i)" using t1 False that Suc_le_lessD trace_def by auto moreover have "exc ?zs (Suc i) <#> 1 = snd (?es ! i)" using t0 False i that Suc_le_lessD trace_def by auto ultimately show ?thesis using i inputpos_def zeros by simp qed moreover have "exc zs t <#> 1 = exc (zeros (length zs)) t <#> 1" if "t > length ?es" proof - have "exc ?zs (length ?es) = (length M, tps0)" using t0 trace_def by simp then have *: "exc ?zs t = exc ?zs (length ?es)" using that by (metis execute_after_halting_ge fst_eqD less_or_eq_imp_le) have "exc zs (length ?es) = (length M, tps)" using t1 trace_def by simp then have "exc zs t = exc zs (length ?es)" using that by (metis execute_after_halting_ge fst_eqD less_or_eq_imp_le) then show ?thesis using * le[of "length ?es"] by (simp add: inputpos_def zeros) qed ultimately show ?thesis using le_less_linear by blast qed text ‹ The value $\prev(t)$ is the most recent step in which $M$'s output tape head was in the same position as in step $t$. If no such step exists, $\prev(t)$ is set to $t$. Again due to $M$ being oblivious, $\prev$ depends only on the length $n$ of the input (and on $t$, of course). › definition prev :: "nat ⇒ nat ⇒ nat" where "prev n t ≡ if ∃t'<t. exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1 then GREATEST t'. t' < t ∧ exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1 else t" lemma oblivious_prev: assumes "bit_symbols zs" shows "prev (length zs) t = (if ∃t'<t. exc zs t' <#> 1 = exc zs t <#> 1 then GREATEST t'. t' < t ∧ exc zs t' <#> 1 = exc zs t <#> 1 else t)" using prev_def assms oblivious_headpos_1 by auto lemma prev_less: assumes "∃t'<t. exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1" shows "prev n t < t ∧ exc (zeros n) (prev n t) <#> 1 = exc (zeros n) t <#> 1" proof - let ?P = "λt'. t' < t ∧ exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1" have "prev n t = (GREATEST t'. t' < t ∧ exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1)" using assms prev_def by simp moreover have "∀y. ?P y ⟶ y ≤ t" by simp ultimately show ?thesis using GreatestI_ex_nat[OF assms, of t] by simp qed corollary prev_less': assumes "bit_symbols zs" assumes "∃t'<t. exc zs t' <#> 1 = exc zs t <#> 1" shows "prev (length zs) t < t ∧ exc zs (prev (length zs) t) <#> 1 = exc zs t <#> 1" using prev_less oblivious_headpos_1 assms by simp lemma prev_greatest: assumes "t' < t" and "exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1" shows "t' ≤ prev n t" proof - let ?P = "λt'. t' < t ∧ exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1" have "prev n t = (GREATEST t'. t' < t ∧ exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1)" using assms prev_def by auto moreover have "?P t'" using assms by simp moreover have "∀y. ?P y ⟶ y ≤ t" by simp ultimately show ?thesis using Greatest_le_nat[of ?P t' t] by simp qed corollary prev_greatest': assumes "bit_symbols zs" assumes "t' < t" and "exc zs t' <#> 1 = exc zs t <#> 1" shows "t' ≤ prev (length zs) t" using prev_greatest oblivious_headpos_1 assms by simp lemma prev_eq: "prev n t = t ⟷ ¬ (∃t'<t. exc (zeros n) t' <#> 1 = exc (zeros n) t <#> 1)" using prev_def nat_less_le prev_less by simp lemma prev_le: "prev n t ≤ t" using prev_eq prev_less by (metis less_or_eq_imp_le) corollary prev_eq': assumes "bit_symbols zs" shows "prev (length zs) t = t ⟷ ¬ (∃t'<t. exc zs t' <#> 1 = exc zs t <#> 1)" using prev_eq oblivious_headpos_1 assms by simp lemma prev_between: assumes "prev n t < t'" and "t' < t" shows "exc (zeros n) t' <#> 1 ≠ exc (zeros n) (prev n t) <#> 1" using assms by (metis (no_types, lifting) leD prev_eq prev_greatest prev_less) lemma prev_write_read: assumes "bit_symbols zs" and "n = length zs" and "prev n t < t" and "cfg = exc zs (prev n t)" and "t ≤ TT n" shows "exc zs t <.> 1 = (M ! (fst cfg)) [cfg <.> 0, cfg <.> 1] [.] 1" proof - let ?cfg = "exc zs (Suc (prev n t))" let ?sas = "(M ! (fst cfg)) [cfg <.> 0, cfg <.> 1]" let ?i = "cfg <#> 1" have 1: "fst cfg < length M" using assms less_TT' by simp have 2: "||cfg|| = 2" using assms execute_num_tapes start_config_length tm_M by auto then have 3: "read (snd cfg) = [cfg <.> 0, cfg <.> 1]" using read_def by (smt (z3) Cons_eq_map_conv Suc_1 length_0_conv length_Suc_conv list.simps(8) nth_Cons_0 nth_Cons_Suc numeral_1_eq_Suc_0 numeral_One) have *: "(?cfg <:> 1) ?i = (M ! (fst cfg)) [cfg <.> 0, cfg <.> 1] [.] 1" proof - have "?cfg <!> 1 = exe M cfg <!> 1" by (simp add: assms) also have "... = sem (M ! (fst cfg)) cfg <!> 1" using 1 exe_lt_length by simp also have "... = act (snd ((M ! (fst cfg)) (read (snd cfg))) ! 1) (snd cfg ! 1)" using sem_snd_tm tm_M 1 2 by (metis Suc_1 lessI prod.collapse) also have "... = act (?sas [!] 1) (cfg <!> 1)" using 3 by simp finally have *: "?cfg <!> 1 = act (?sas [!] 1) (cfg <!> 1)" . have "(?cfg <:> 1) ?i = fst (?cfg <!> 1) ?i" by simp also have ***: "... = ((fst (cfg <!> 1))(?i := (?sas [.] 1))) ?i" using * act by simp also have "... = ?sas [.] 1" by simp finally show "(?cfg <:> 1) ?i = ?sas [.] 1" using *** by simp qed have "((exc zs t') <:> 1) ?i = (M ! (fst cfg)) [cfg <.> 0, cfg <.> 1] [.] 1" if "Suc (prev n t) ≤ t'" and "t' ≤ t" for t' using that proof (induction t' rule: nat_induct_at_least) case base then show ?case using * by simp next case (Suc m) let ?cfg_m = "exc zs m" from Suc have between: "prev n t < m" "m < t" by simp_all then have *: "?cfg_m <#> 1 ≠ ?i" using prev_between assms oblivious_headpos_1 by simp have "m < TT n" using Suc assms by simp then have 1: "fst ?cfg_m < length M" using assms less_TT' by simp have 2: "||?cfg_m|| = 2" using execute_num_tapes start_config_length tm_M by auto have "exc zs (Suc m) <!> 1 = exe M ?cfg_m <!> 1" by simp also have "... = sem (M ! (fst ?cfg_m)) ?cfg_m <!> 1" using 1 exe_lt_length by simp also have "... = act (snd ((M ! (fst ?cfg_m)) (read (snd ?cfg_m))) ! 1) (snd ?cfg_m ! 1)" using sem_snd_tm tm_M 1 2 by (metis Suc_1 lessI prod.collapse) finally have "exc zs (Suc m) <!> 1 = act (snd ((M ! (fst ?cfg_m)) (read (snd ?cfg_m))) ! 1) (snd ?cfg_m ! 1)" . then have "(exc zs (Suc m) <:> 1) ?i = fst (snd ?cfg_m ! 1) ?i" using * act_changes_at_most_pos' by simp then show ?case using Suc by simp qed then have "((exc zs t) <:> 1) ?i = (M ! (fst cfg)) [cfg <.> 0, cfg <.> 1] [.] 1" using Suc_leI assms by simp moreover have "?i = exc zs t <#> 1" using assms(1,2,4) oblivious_headpos_1 prev_eq prev_less by (smt (z3)) ultimately show ?thesis by simp qed lemma prev_no_write: assumes "bit_symbols zs" and "n = length zs" and "prev n t = t" and "t ≤ TT n" and "t > 0" shows "exc zs t <.> 1 = □" proof - let ?i = "exc zs t <#> 1" have 1: "¬ (∃t'<t. exc zs t' <#> 1 = ?i)" using prev_eq' assms(1,2,3) by simp have 2: "?i > 0" proof (rule ccontr) assume "¬ 0 < ?i" then have eq0: "?i = 0" by simp moreover have "exc zs 0 <#> 1 = 0" by (simp add: start_config_pos) ultimately show False using 1 assms(5) by auto qed have 3: "(exc zs (Suc t') <:> 1) i = (exc zs t' <:> 1) i" if "i ≠ exc zs t' <#> 1" for i t' proof (cases "fst (exc zs t') < length M") case True let ?cfg = "exc zs t'" have len2: "||?cfg|| = 2" using execute_num_tapes start_config_length tm_M by auto have "exc zs (Suc t') <!> 1 = exe M ?cfg <!> 1" by simp also have "... = sem (M ! (fst ?cfg)) ?cfg <!> 1" using True exe_lt_length by simp also have "... = act (snd ((M ! (fst ?cfg)) (read (snd ?cfg))) ! 1) (snd ?cfg ! 1)" using sem_snd_tm tm_M True len2 by (metis Suc_1 lessI prod.collapse) finally have "exc zs (Suc t') <!> 1 = act (snd ((M ! (fst ?cfg)) (read (snd ?cfg))) ! 1) (snd ?cfg ! 1)" . then have "(exc zs (Suc t') <:> 1) i = fst (snd ?cfg ! 1) i" using that act_changes_at_most_pos' by simp then show ?thesis by simp next case False then show ?thesis using that by (simp add: exe_def) qed have "(exc zs t' <:> 1) ?i = (exc zs 0 <:> 1) ?i" if "t' ≤ t" for t' using that proof (induction t') case 0 then show ?case by simp next case (Suc t') then show ?case by (metis 1 3 Suc_leD Suc_le_lessD) qed then have "exc zs t <.> 1 = (exc zs 0 <:> 1) ?i" by simp then show ?thesis using 2 One_nat_def execute.simps(1) start_config1 less_2_cases_iff less_one by presburger qed text ‹ The intervals $\gamma_i$ and $w_0, \dots, w_9$ do not depend on $x$, and so can be defined here already. › definition gamma :: "nat ⇒ nat list" ("γ") where "γ i ≡ [i * H..<Suc i * H]" lemma length_gamma [simp]: "length (γ i) = H" using gamma_def by simp abbreviation "w⇩_{0}≡ [0..<H]" abbreviation "w⇩_{1}≡ [H..<2*H]" abbreviation "w⇩_{2}≡ [2*H..<Z]" abbreviation "w⇩_{3}≡ [Z..<Z+H]" abbreviation "w⇩_{4}≡ [Z+H..<Z+2*H]" abbreviation "w⇩_{5}≡ [Z+2*H..<2*Z]" abbreviation "w⇩_{6}≡ [2*Z..<2*Z+H]" abbreviation "w⇩_{7}≡ [2*Z+H..<2*Z+2*H]" abbreviation "w⇩_{8}≡ [2*Z+2*H..<3*Z]" abbreviation "w⇩_{9}≡ [3*Z..<3*Z+H]" lemma unary_upt_eq: fixes α⇩_{1}α⇩_{2}:: assignment and lower upper k :: nat assumes "∀i<k. α⇩_{1}i = α⇩_{2}i" and "upper ≤ k" shows "unary α⇩_{1}[lower..<upper] = unary α⇩_{2}[lower..<upper]" proof - have "numtrue α⇩_{1}[lower..<upper] = numtrue α⇩_{2}[lower..<upper]" proof - let ?vs = "[lower..<upper]" have "filter α⇩_{1}?vs = filter α⇩_{2}?vs" using assms by (metis atLeastLessThan_iff filter_cong less_le_trans set_upt) then show ?thesis using numtrue_def by simp qed moreover have "blocky α⇩_{1}[lower..<upper] = blocky α⇩_{2}[lower..<upper]" using blocky_def assms by auto ultimately show ?thesis using assms unary_def by simp qed text ‹ For the case @{term "prev m t < t"}, we have the following predicate on assignments, which corresponds to ($\mathrm{F}_1$), ($\mathrm{F}_2$), ($\mathrm{F}_3$) from the introduction: › definition F :: "assignment ⇒ bool" where "F α ≡ unary α w⇩_{6}= unary α w⇩_{9}∧ unary α w⇩_{7}= (M ! (unary α w⇩_{5})) [unary α w⇩_{3}, unary α w⇩_{4}] [.] 1 ∧ unary α w⇩_{8}= fst ((M ! (unary α w⇩_{2})) [unary α w⇩_{0}, unary α w⇩_{1}])" lemma depon_F: "depon (3 * Z + H) F" using depon_def F_def Z_def unary_upt_eq by simp text ‹ There is a CNF formula $\psi$ that contains the first $3Z + H$ variables and is satisfied by exactly the assignments specified by $F$. › definition psi :: formula ("ψ") where "ψ ≡ SOME φ. fsize φ ≤ (3 * Z + H) * 2 ^ (3 * Z + H) ∧ length φ ≤ 2 ^ (3 * Z + H) ∧ variables φ ⊆ {..<3 * Z + H} ∧ (∀α. F α = α ⊨ φ)" lemma psi: "fsize ψ ≤ (3 * Z + H) * 2 ^ (3*Z + H) ∧ length ψ ≤ 2 ^ (3 * Z + H) ∧ variables ψ ⊆ {..<3 * Z + H} ∧ (∀α. F α = α ⊨ ψ)" using psi_def someI_ex[OF depon_ex_formula[OF depon_F]] by metis lemma satisfies_psi: assumes "length σ = 3 * Z + H" shows "α ⊨ relabel σ ψ = remap σ α ⊨ ψ" using assms psi satisfies_sigma by simp lemma psi_F: "remap σ α ⊨ ψ = F (remap σ α)" using psi by simp corollary satisfies_F: assumes "length σ = 3 * Z + H" shows "α ⊨ relabel σ ψ = F (remap σ α)" using assms satisfies_psi psi_F by simp text ‹ For the case @{term "prev m t = t"}, the following predicate corresponds to ($\mathrm{F}_1'$), ($\mathrm{F}_2'$), ($\mathrm{F}_3'$) from the introduction: › definition F' :: "assignment ⇒ bool" where "F' α ≡ unary α w⇩_{3}= unary α w⇩_{6}∧ unary α w⇩_{4}= 0 ∧ unary α w⇩_{5}= fst ((M ! (unary α w⇩_{2})) [unary α w⇩_{0}, unary α w⇩_{1}])" lemma depon_F': "depon (2 * Z + H) F'" using depon_def F'_def Z_def unary_upt_eq by simp text ‹ The CNF formula $\psi'$ is analogous to $\psi$ from the previous case. › definition psi' :: formula ("ψ''") where "ψ' ≡ SOME φ. fsize φ ≤ (2*Z+H) * 2 ^ (2*Z+H) ∧ length φ ≤ 2 ^ (2*Z+H) ∧ variables φ ⊆ {..<2*Z+H} ∧ (∀α. F' α = α ⊨ φ)" lemma psi': "fsize ψ' ≤ (2*Z+H) * 2 ^ (2*Z+H) ∧ length ψ' ≤ 2 ^ (2*Z+H) ∧ variables ψ' ⊆ {..<2*Z+H} ∧ (∀α. F' α = α ⊨ ψ')" using psi'_def someI_ex[OF depon_ex_formula[OF depon_F']] by metis lemma satisfies_psi': assumes "length σ = 2*Z+H" shows "α ⊨ relabel σ ψ' = remap σ α ⊨ ψ'" using assms psi' satisfies_sigma by simp lemma psi'_F': "remap σ α ⊨ ψ' = F' (remap σ α)" using psi' by simp corollary satisfies_F': assumes "length σ = 2*Z+H" shows "α ⊨ relabel σ ψ' = F' (remap σ α)" using assms satisfies_psi' psi'_F' by simp end (* locale reduction_sat *) section ‹Snapshots› text ‹ The snapshots and much of the rest of the construction of $\Phi$ depend on the string $x$. We encapsulate this in a sublocale of @{locale reduction_sat}. › locale reduction_sat_x = reduction_sat + fixes x :: string begin abbreviation n :: nat where "n ≡ length x" text ‹ Turing machines consume the string $x$ as a sequence $xs$ of symbols: › abbreviation xs :: "symbol list" where "xs ≡ string_to_symbols x" lemma bs_xs: "bit_symbols xs" by simp text ‹ For the verifier Turing machine $M$ we are only concerned with inputs of the form $\langle x, u\rangle$ for a string $u$ of length $p(n)$. The pair $\langle x, u\rangle$ has the length $m = 2n + 2p(n) + 2$. › definition m :: nat where "m ≡ 2 * n + 2 * p n + 2" text ‹ On input $\langle x, u\rangle$ the Turing machine $M$ halts after $T' = TT(m)$ steps. › definition T' :: nat where "T' ≡ TT m" text ‹ The positions of both of $M$'s tape heads are bounded by $T'$. › lemma inputpos_less: "inputpos m t ≤ T'" proof - define u :: string where "u = replicate (p n) False" let ?i = "inputpos m t" have y: "bit_symbols ⟨x; u⟩" by simp have len: "length ⟨x; u⟩ = m" using u_def m_def length_pair by simp then have "exc ⟨x; u⟩ t <#> 0 ≤ T'" using TT'[OF y] T'_def head_pos_le_halting_time[OF tm_M, of "⟨x; u⟩" T' 0] by simp then show ?thesis using inputpos_oblivious[OF y] len by simp qed lemma headpos_1_less: "exc (zeros m) t <#> 1 ≤ T'" proof - define u :: string where "u = replicate (p n) False" let ?i = "inputpos m t" have y: "bit_symbols ⟨x; u⟩" by simp have len: "length ⟨x; u⟩ = m" using u_def m_def length_pair by simp then have "exc ⟨x; u⟩ t <#> 1 ≤ T'" using TT'[OF y] T'_def head_pos_le_halting_time[OF tm_M, of "⟨x; u⟩" "T'" 1] by simp then show ?thesis using oblivious_headpos_1[OF y] len by simp qed text ‹ The formula $\Phi$ must contain a condition for every symbol that $M$ is reading from the input tape. While $T'$ is an upper bound for the input tape head position of $M$, it might be that $T'$ is less than the length of the input $\langle x, u\rangle$. So the portion of the input read by $M$ might be a prefix of the input or it might be the input followed by some blanks afterwards. This would make for an awkward case distinction. We do not have to be very precise here and can afford to bound the portion of the input tape read by $M$ by the number $m' = 2n + 2p(n) + 3 + T'$, which is the length of the start symbol followed by the input $\langle x, u\rangle$ followed by $T'$ blanks. This symbol sequence was called $y(u)$ in the introduction. Here we will call it @{term "ysymbols u"}. › definition m' :: nat where "m' ≡ 2 * n + 2 * p n + 3 + T'" definition ysymbols :: "string ⇒ symbol list" where "ysymbols u ≡ 1 # ⟨x; u⟩ @ replicate T' 0" lemma length_ysymbols: "length u = p n ⟹ length (ysymbols u) = m'" using ysymbols_def m'_def m_def length_pair by simp lemma ysymbols_init: assumes "i < length (ysymbols u)" shows "ysymbols u ! i = (start_config 2 ⟨x; u⟩ <:> 0) i" proof - let ?y = "⟨x; u⟩" have init: "start_config 2 ?y <:> 0 = (λi. if i = 0 then 1 else if i ≤ length ?y then ?y ! (i - 1) else 0)" using start_config_def by auto have "i < length ?y + 1 + T'" using assms ysymbols_def by simp then consider "i = 0" | "i > 0 ∧ i ≤ length ?y" | "i > length ?y ∧ i < length ?y + 1 + T'" by linarith then show "ysymbols u ! i = (start_config 2 ?y <:> 0) i" proof (cases) case 1 then show ?thesis using ysymbols_def init by simp next case 2 then have "ysymbols u ! i = ⟨x; u⟩ ! (i - 1)" using ysymbols_def by (smt (z3) One_nat_def Suc_less_eq Suc_pred le_imp_less_Suc neq0_conv nth_Cons' nth_append) then show ?thesis using init 2 by simp next case 3 then have "(start_config 2 ?y <:> 0) i = 0" using init by simp moreover have "ysymbols u ! i = 0" unfolding ysymbols_def using 3 nth_append[of "1#⟨x; u⟩" "replicate T' 0" i] by auto ultimately show ?thesis by simp qed qed lemma ysymbols_at_0: "ysymbols u ! 0 = 1" using ysymbols_def by simp lemma ysymbols_first_at: assumes "j < length x" shows "ysymbols u ! (2*j+1) = 2" and "ysymbols u ! (2*j+2) = (if x ! j then 3 else 2)" proof - have *: "ysymbols u = (1 # ⟨x; u⟩) @ replicate T' 0" using ysymbols_def by simp let ?i = "2 * j + 1" have len: "2*j < length ⟨x, u⟩" using assms length_string_pair by simp have "?i < length (1 # ⟨x; u⟩)" using assms length_pair by simp then have "ysymbols u ! ?i = (1 # ⟨x; u⟩) ! ?i" using * nth_append by metis also have "... = ⟨x; u⟩ ! (2*j)" by simp also have "... = 2" using string_pair_first_nth assms len by simp finally show "ysymbols u ! ?i = 2" . let ?i = "2 * j + 2" have len2: "?i < length (1 # ⟨x; u⟩)" using assms length_pair by simp then have "ysymbols u ! ?i = (1 # ⟨x; u⟩) ! ?i" using * nth_append by metis also have "... = ⟨x; u⟩ ! (2*j+1)" by simp also have "... = (if x ! j then 3 else 2)" using string_pair_first_nth(2) assms len2 by simp finally show "ysymbols u ! ?i = (if x ! j then 3 else 2)" . qed lemma ysymbols_at_2n1: "ysymbols u ! (2*n+1) = 3" proof - let ?i = "2 * n + 1" have "ysymbols u ! ?i = ⟨x; u⟩ ! (2*n)" using ysymbols_def by (metis (no_types, lifting) add.commute add_2_eq_Suc' le_add2 le_imp_less_Suc length_pair less_SucI nth_Cons_Suc nth_append plus_1_eq_Suc) also have "... = (if ⟨x, u⟩ ! (2*n) then 3 else 2)" using length_pair by simp also have "... = 3" using string_pair_sep_nth by simp finally show ?thesis . qed lemma ysymbols_at_2n2: "ysymbols u ! (2*n+2) = 3" proof - let ?i = "2 * n + 2" have "ysymbols u ! ?i = ⟨x; u⟩ ! (2*n+1)" using ysymbols_def by (smt (z3) One_nat_def add.commute add.right_neutral add_2_eq_Suc' add_Suc_right le_add2 le_imp_less_Suc length_pair nth_Cons_Suc nth_append) also have "... = (if ⟨x, u⟩ ! (2*n+1) then 3 else 2)" using length_pair by simp also have "... = 3" using string_pair_sep_nth by simp finally show ?thesis . qed lemma ysymbols_second_at: assumes "j < length u" shows "ysymbols u ! (2*n+2+2*j+1) = 2" and "ysymbols u ! (2*n+2+2*j+2) = (if u ! j then 3 else 2)" proof - have *: "ysymbols u = (1 # ⟨x; u⟩) @ replicate T' 0" using ysymbols_def by simp let ?i = "2 * n + 2 + 2 * j + 1" have len: "2 * n + 2 + 2*j < length ⟨x, u⟩" using assms length_string_pair by simp have "?i < length (1 # ⟨x; u⟩)" using assms length_pair by simp then have "ysymbols u ! ?i = (1 # ⟨x; u⟩) ! ?i" using * nth_append by metis also have "... = ⟨x; u⟩ ! (2*n+2+2*j)" by simp also have "... = 2" using string_pair_second_nth(1) assms len by simp finally show "ysymbols u ! ?i = 2" . let ?i = "2*n+2+2 * j + 2" have len2: "?i < length (1 # ⟨x; u⟩)" using assms length_pair by simp then have "ysymbols u ! ?i = (1 # ⟨x; u⟩) ! ?i" using * nth_append by metis also have "... = ⟨x; u⟩ ! (2*n+2+2*j+1)" by simp also have "... = (if u ! j then 3 else 2)" using string_pair_second_nth(2) assms len2 by simp finally show "ysymbols u ! ?i = (if u ! j then 3 else 2)" . qed lemma ysymbols_last: assumes "length u = p n" and "i > m" and "i < m + 1 + T'" shows "ysymbols u ! i = 0" using assms length_ysymbols m_def m'_def ysymbols_def nth_append[of "1#⟨x; u⟩" "replicate T' 0" i] by simp text ‹ The number of symbols used for unary encoding $m'$ symbols will be called $N$: › definition N :: nat where "N ≡ H * m'" lemma N_eq: "N = H * (2 * n + 2 * p n + 3 + T')" using m'_def N_def by simp lemma m': "m' * H = N " using m'_def N_def by simp lemma inputpos_less': "inputpos m t < m'" using inputpos_less m_def m'_def by (metis Suc_1 add_less_mono1 le_neq_implies_less lessI linorder_neqE_nat not_add_less2 numeral_plus_numeral semiring_norm(3) trans_less_add2) lemma T'_less: "T' < N" proof - have "T' < 2 * n + 2 * p n + 3 + T'" by simp also have "... < H * (2 * n + 2 * p n + 3 + T')" using H_gr_2 by simp also have "... = N" using N_eq by simp finally show ?thesis . qed text ‹The three components of a snapshot:› definition z0 :: "string ⇒ nat ⇒ symbol" where "z0 u t ≡ exc ⟨x; u⟩ t <.> 0" definition z1 :: "string ⇒ nat ⇒ symbol" where "z1 u t ≡ exc ⟨x; u⟩ t <.> 1" definition z2 :: "string ⇒ nat ⇒ state" where "z2 u t ≡ fst (exc ⟨x; u⟩ t)" lemma z0_le: "z0 u t ≤ H" using z0_def H_ge_G tape_alphabet[OF tm_M, where ?j=0 and ?zs="⟨x; u⟩"] symbols_lt_pair[of x u] tm_M turing_machine_def by (metis (no_types, lifting) dual_order.strict_trans1 less_or_eq_imp_le zero_less_numeral) lemma z1_le: "z1 u t ≤ H" using z1_def H_ge_G tape_alphabet[OF tm_M, where ?j=1 and ?zs="⟨x; u⟩"] symbols_lt_pair[of x u] tm_M turing_machine_def by (metis (no_types, lifting) dual_order.strict_trans1 less_or_eq_imp_le one_less_numeral_iff semiring_norm(76)) lemma z2_le: "z2 u t ≤ H" proof - have "z2 u t ≤ length M" using z2_def turing_machine_execute_states[OF tm_M] start_config_def by simp then show ?thesis using H_ge_length_M by simp qed text ‹ The next lemma corresponds to (Z1) from the second equivalence mentioned in the introduction. It expresses the first element of a snapshot in terms of $y(u)$ and $\inputpos$. › lemma z0: assumes "length u = p n" shows "z0 u t = ysymbols u ! (inputpos m t)" proof - let ?i = "inputpos m t" let ?y = "⟨x; u⟩" have "bit_symbols ?y" by simp have len: "length ?y = m" using assms m_def length_pair by simp have "?i < length (ysymbols u)" using inputpos_less' assms length_ysymbols by simp then have *: "ysymbols u ! ?i = (start_config 2 ?y <:> 0) ?i" using ysymbols_init by simp have "z0 u t = exc ?y t <.> 0" using z0_def by simp also have "... = (start_config 2 ?y <:> 0) (exc ?y t <#> 0)" using tm_M input_tape_constant start_config_length by simp also have "... = (start_config 2 ?y <:> 0) ?i" using inputpos_oblivious[OF `bit_symbols ?y`] len by simp also have "... = ysymbols u ! ?i" using * by simp finally show ?thesis . qed text ‹ The next lemma corresponds to (Z2) from the second equivalence mentioned in the introduction. It shows how, in the case $\prev(t) < t$, the second component of a snapshot can be expressed recursively using snapshots for earlier steps. › lemma z1: assumes "length u = p n" and "prev m t < t" and "t ≤ T'" shows "z1 u t = (M ! (z2 u (prev m t))) [z0 u (prev m t), z1 u (prev m t)] [.] 1" proof - let ?y = "⟨x; u⟩" let ?cfg = "exc ?y (prev m t)" have "bit_symbols ?y" by simp moreover have len: "length ?y = m" using assms m_def length_pair by simp ultimately have "exc ?y t <.> 1 = (M ! (fst ?cfg)) [?cfg <.> 0, ?cfg <.> 1] [.] 1" using prev_write_read[of ?y m t ?cfg] assms(2,3) T'_def by fastforce then show ?thesis using z0_def z1_def z2_def by simp qed text ‹ The next lemma corresponds to (Z3) from the second equivalence mentioned in the introduction. It shows that in the case $\prev(t) = t$, the second component of a snapshot equals the blank symbol. › lemma z1': assumes "length u = p n" and "prev m t = t" and "0 < t" and "t ≤ T'" shows "z1 u t = □" proof - let ?y = "⟨x; u⟩" let ?cfg = "exc ?y (prev m t)" have "bit_symbols ?y" by simp moreover have len: "length ?y = m" using assms m_def length_pair by simp ultimately have "exc ?y t <.> 1 = □" using prev_no_write[of ?y m t] assms T'_def by fastforce then show ?thesis using z0_def z1_def z2_def by simp qed text ‹ The next lemma corresponds to (Z4) from the second equivalence mentioned in the introduction. It shows how the third component of a snapshot can be expressed recursively using snapshots for earlier steps. › lemma z2: assumes "length u = p n" and "t < T'" shows "z2 u (Suc t) = fst ((M ! (z2 u t)) [z0 u t, z1 u t])" proof - let ?y = "⟨x; u⟩" have "bit_symbols ?y" by simp moreover have len: "length ?y = m" using assms m_def length_pair by simp ultimately have run: "fst (exc ?y t) < length M" using less_TT' assms(2) T'_def by simp have "||exc ?y t|| = 2" using start_config_length execute_num_tapes tm_M by simp then have "snd (exc ?y t) = [exc ?y t <!> 0, exc ?y t <!> 1]" by auto (smt (z3) Suc_length_conv length_0_conv nth_Cons_0 nth_Cons_Suc numeral_2_eq_2) then have *: "read (snd (exc ?y t)) = [exc ?y t <.> 0, exc ?y t <.> 1]" using read_def by (metis (no_types, lifting) list.simps(8) list.simps(9)) have "z2 u (Suc t) = fst (exc ?y (Suc t))" using z2_def by simp also have "... = fst (exe M (exc ?y t))" by simp also have "... = fst (sem (M ! fst (exc ?y t)) (exc ?y t))" using exe_lt_length run by simp also have "... = fst (sem (M ! (z2 u t)) (exc ?y t))" using z2_def by simp also have "... = fst ((M ! (z2 u t)) (read (snd (exc ?y t))))" using sem_fst by simp also have "... = fst ((M ! (z2 u t)) [exc ?y t <.> 0, exc ?y t <.> 1])" using * by simp also have "... = fst ((M ! (z2 u t)) [z0 u t, z1 u t])" using z0_def z1_def by simp finally show ?thesis . qed corollary z2': assumes "length u = p n" and "t > 0" and "t ≤ T'" shows "z2 u t = fst ((M ! (z2 u (t - 1))) [z0 u (t - 1), z1 u (t - 1)])" using assms z2 by (metis Suc_diff_1 Suc_less_eq le_imp_less_Suc) text ‹ The intervals $\zeta_0$, $\zeta_1$, and $\zeta_2$ are long enough for a unary encoding of the three components of a snapshot: › definition zeta0 :: "nat ⇒ nat list" ("ζ⇩_{0}") where "ζ⇩_{0}t ≡ [N + t * Z..<N + t * Z + H]" definition zeta1 :: "nat ⇒ nat list" ("ζ⇩_{1}") where "ζ⇩_{1}t ≡ [N + t * Z + H..<N + t * Z + 2 * H]" definition zeta2 :: "nat ⇒ nat list" ("ζ⇩_{2}") where "ζ⇩_{2}t ≡ [N + t * Z + 2 * H..<N + (Suc t) * Z]" lemma length_zeta0 [simp]: "length (ζ⇩_{0}t) = H" using zeta0_def by simp lemma length_zeta1 [simp]: "length (ζ⇩_{1}t) = H" using zeta1_def by simp lemma length_zeta2 [simp]: "length (ζ⇩_{2}t) = H" using zeta2_def Z_def by simp text ‹ The substitutions $\rho_t$, which have to be applied to $\psi$ to get the CNF formulas $\chi_t$ for the case $\prev(t) < t$: › definition rho :: "nat ⇒ nat list" ("ρ") where "ρ t ≡ ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1) @ ζ⇩_{2}(t - 1) @ ζ⇩_{0}(prev m t) @ ζ⇩_{1}(prev m t) @ ζ⇩_{2}(prev m t) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t)" lemma length_rho: "length (ρ t) = 3 * Z + H" using rho_def Z_def by simp text ‹ The substitutions $\rho_t'$, which have to be applied to $\psi'$ to get the CNF formulas $\chi_t$ for the case $\prev(t) = t$: › definition rho' :: "nat ⇒ nat list" ("ρ''") where "ρ' t ≡ ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1) @ ζ⇩_{2}(t - 1) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t)" lemma length_rho': "length (ρ' t) = 2 * Z + H" using rho'_def Z_def by simp text ‹ An auxiliary lemma for accessing the $n$-th element of a list sandwiched between two lists. It will be applied to $xs = \rho_t$ or $xs = \rho'_t$: › lemma nth_append3: fixes xs ys zs ws :: "'a list" and n i :: nat assumes "xs = ys @ zs @ ws" and "i < length zs" and "n = length ys" shows "xs ! (n + i) = zs ! i" using assms by (simp add: nth_append) text ‹The formulas $\chi_t$ representing snapshots for $0 < t \leq T'$:› definition chi :: "nat ⇒ formula" ("χ") where "χ t ≡ if prev m t < t then relabel (ρ t) ψ else relabel (ρ' t) ψ'" text ‹ The crucial feature of the formulas $\chi_t$ for $t > 0$ is that they are satisfied by exactly those assignments that represent in their bits $N$ to $N + Z\cdot(T' + 1)$ the $T' + 1$ snapshots of $M$ on input $\langle x, u\rangle$ when the relevant portion of the input tape is encoded in the first $N$ bits of the assignment. This works because the $\chi_t$ constrain the assignment to meet the recursive characterizations (Z1) --- (Z4) for the snapshots. The next two lemmas make this more precise. We first consider the case $\prev(t) < t$. The following lemma says $\alpha$ satisfies $\chi_t$ iff.\ $\alpha$ satisfies the properties (Z1), (Z2), and (Z4). › lemma satisfies_chi_less: fixes α :: assignment assumes "prev m t < t" shows "α ⊨ χ t ⟷ unary α (ζ⇩_{0}t) = unary α (γ (inputpos m t)) ∧ unary α (ζ⇩_{1}t) = (M ! (unary α (ζ⇩_{2}(prev m t)))) [unary α (ζ⇩_{0}(prev m t)), unary α (ζ⇩_{1}(prev m t))] [.] 1 ∧ unary α (ζ⇩_{2}t) = fst ((M ! (unary α (ζ⇩_{2}(t - 1)))) [unary α (ζ⇩_{0}(t - 1)), unary α (ζ⇩_{1}(t - 1))])" proof - let ?sigma = "ρ t" have "α ⊨ χ t = α ⊨ relabel ?sigma psi" using assms chi_def by simp then have "α ⊨ χ t = F (remap ?sigma α)" (is "_ = F ?alpha") by (simp add: length_rho satisfies_F) then have *: "α ⊨ χ t = (unary ?alpha w⇩_{6}= unary ?alpha w⇩_{9}∧ unary ?alpha w⇩_{7}= (M ! (unary ?alpha w⇩_{5})) [unary ?alpha w⇩_{3}, unary ?alpha w⇩_{4}] [.] 1 ∧ unary ?alpha w⇩_{8}= fst ((M ! (unary ?alpha w⇩_{2})) [unary ?alpha w⇩_{0}, unary ?alpha w⇩_{1}]))" using F_def by simp have w_less_len_rho: "∀s∈set w⇩_{0}. s < length (ρ t)" "∀s∈set w⇩_{1}. s < length (ρ t)" "∀s∈set w⇩_{2}. s < length (ρ t)" "∀s∈set w⇩_{3}. s < length (ρ t)" "∀s∈set w⇩_{4}. s < length (ρ t)" "∀s∈set w⇩_{5}. s < length (ρ t)" "∀s∈set w⇩_{6}. s < length (ρ t)" "∀s∈set w⇩_{7}. s < length (ρ t)" "∀s∈set w⇩_{8}. s < length (ρ t)" "∀s∈set w⇩_{9}. s < length (ρ t)" using length_rho Z_def by simp_all have **: "α ⊨ χ t = (unary α (reseq ?sigma w⇩_{6}) = unary α (reseq ?sigma w⇩_{9}) ∧ unary α (reseq ?sigma w⇩_{7}) = (M ! (unary α (reseq ?sigma w⇩_{5}))) [unary α (reseq ?sigma w⇩_{3}), unary α (reseq ?sigma w⇩_{4})] [.] 1 ∧ unary α (reseq ?sigma w⇩_{8}) = fst ((M ! (unary α (reseq ?sigma w⇩_{2}))) [unary α (reseq ?sigma w⇩_{0}), unary α (reseq ?sigma w⇩_{1})]))" using * w_less_len_rho unary_remap[where ?σ="?sigma" and ?α=α] by presburger have 1: "reseq ?sigma w⇩_{0}= ζ⇩_{0}(t - 1)" (is "?l = ?r") proof (rule nth_equalityI) show "length ?l = length ?r" using zeta0_def by simp show "?l ! i = ?r ! i" if "i < length ?l" for i proof - have 1: "?sigma = [] @ ζ⇩_{0}(t - 1) @ (ζ⇩_{1}(t - 1) @ ζ⇩_{2}(t - 1) @ ζ⇩_{0}(prev m t) @ ζ⇩_{1}(prev m t) @ ζ⇩_{2}(prev m t) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t))" using rho_def by simp have "?sigma ! i = ζ⇩_{0}(t - 1) ! i" using nth_append3[OF 1, of i 0] Z_def that by simp then show ?thesis using reseq_def that by simp qed qed have 2: "reseq ?sigma w⇩_{1}= ζ⇩_{1}(t - 1)" (is "?l = ?r") proof (rule nth_equalityI) show "length ?l = length ?r" using zeta1_def by simp show "?l ! i = ?r ! i" if "i < length ?l" for i proof - have 1: "?sigma = ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1) @ ζ⇩_{2}(t - 1) @ ζ⇩_{0}(prev m t) @ ζ⇩_{1}(prev m t) @ ζ⇩_{2}(prev m t) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t)" using rho_def by simp have "?sigma ! (H+i) = ζ⇩_{1}(t - 1) ! i" using that zeta0_def zeta1_def by (intro nth_append3[OF 1]) auto then show ?thesis using reseq_def that by simp qed qed have 3: "reseq ?sigma w⇩_{2}= ζ⇩_{2}(t - 1)" (is "?l = ?r") proof (rule nth_equalityI) show len: "length ?l = length ?r" using zeta2_def by simp show "?l ! i = ?r ! i" if "i < length ?l" for i proof - have 1: "?sigma = (ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1)) @ ζ⇩_{2}(t - 1) @ ζ⇩_{0}(prev m t) @ ζ⇩_{1}(prev m t) @ ζ⇩_{2}(prev m t) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t)" using rho_def by simp have "?sigma ! (2*H+i) = ζ⇩_{2}(t - 1) ! i" using len that zeta0_def zeta1_def by (intro nth_append3[OF 1]) auto then show ?thesis using reseq_def that by simp qed qed have 4: "reseq ?sigma w⇩_{3}= ζ⇩_{0}(prev m t)" (is "?l = ?r") proof (rule nth_equalityI) show "length ?l = length ?r" using zeta0_def by simp show "?l ! i = ?r ! i" if "i < length ?l" for i proof - have 1: "?sigma = (ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1) @ ζ⇩_{2}(t - 1)) @ ζ⇩_{0}(prev m t) @ ζ⇩_{1}(prev m t) @ ζ⇩_{2}(prev m t) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t)" using rho_def by simp have "?sigma ! (Z+i) = ζ⇩_{0}(prev m t) ! i" using that Z_def by (intro nth_append3[OF 1]) auto then show ?thesis using reseq_def that by simp qed qed have 5: "reseq ?sigma w⇩_{4}= ζ⇩_{1}(prev m t)" (is "?l = ?r") proof (rule nth_equalityI) show "length ?l = length ?r" using zeta1_def by simp show "?l ! i = ?r ! i" if "i < length ?l" for i proof - have 1: "?sigma = (ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1) @ ζ⇩_{2}(t - 1) @ ζ⇩_{0}(prev m t)) @ ζ⇩_{1}(prev m t) @ ζ⇩_{2}(prev m t) @ ζ⇩_{0}t @ ζ⇩_{1}t @ ζ⇩_{2}t @ γ (inputpos m t)" using rho_def by simp have "?sigma ! (Z+H+i) = ζ⇩_{1}(prev m t) ! i" using that Z_def by (intro nth_append3[OF 1]) auto then show ?thesis using reseq_def that by simp qed qed have 6: "reseq ?sigma w⇩_{5}= ζ⇩_{2}(prev m t)" (is "?l = ?r") proof (rule nth_equalityI) show "length ?l = length ?r" using zeta2_def by simp show "?l ! i = ?r ! i" if "i < length ?l" for i proof - have 1: "?sigma = (ζ⇩_{0}(t - 1) @ ζ⇩_{1}(t - 1)