Theory Oblivious_2_Tape

section ‹Existence of two-tape oblivious Turing machines\label{s:oblivious-two-tape}›

theory Oblivious_2_Tape
  imports Oblivious_Polynomial NP
begin


text ‹
In this section we show that for every polynomial-time multi-tape Turing machine
there is a polynomial-time two-tape oblivious Turing machine that computes the
same function and halts with its output tape head in cell number~1.

Consider a $k$-tape Turing machine $M$ with polynomially bounded running time
$T$. We construct a two-tape oblivious Turing machine $S$ simulating $M$ as
follows.

Lemma @{thm [source] polystructor} from the previous section provides us with a
polynomial-time two-tape oblivious TM and a function $f(n) \geq T(n)$ such that
the TM outputs $\mathbf{1}^{f(n)}$ for all inputs of length $n$.

Executing this TM is the first thing our simulator does. The $f(n)$
symbols~@{text 𝟭} mark the space $S$ is going to use. Every cell $i=0, \dots,
f(n) - 1$ of this space is to store a symbol that encodes a $(2k + 2)$-tuple
consisting of:

\begin{itemize}
\item $k$ symbols from $M$'s alphabet representing the contents of all the
  $i$-th cells on the $k$ tapes of $M$;
\item $k$ flags (called ``head flags'') signalling which of the $k$ tape heads
  of $M$ is in cell $i$;
\item a flag (called ``counter flag'') initialized with 0;
\item a flag (called ``start flag'') signalling whether $i = 0$.
\end{itemize}

Together the counter flags are a unary counter from 0 to $f(n)$. They are
toggled from left to right. The start flags never change. The symbols and the
head flags represent the $k$ tapes of $M$ at some step of the execution.  By
choice of $f$ the TM $M$ cannot use more than $f(n)$ cells on any tape. So the
space marked with @{text 𝟭} symbols on the simulator's output tape suffices.

Next the simulator initializes the space of @{text 𝟭} symbols with code symbols
representing the start configuration of $M$ for the input given to the
simulator.

Then the main loop of the simulation performs $f(n)$ iterations. In each
iteration $S$ performs one step of $M$'s computation. In order to do this it
performs several left-to-right and right-to-left sweeps over all the $f(n)$
cells in the formatted section of the output tape.  A sweep will move the output
tape head one cell right (respectively left) in each step.  In this way the
simulator's head positions at any time will only depend on $f(n)$, and hence
on $n$. Thus the machine will be oblivious. Moreover $f(n) \ge T(n)$, and so $M$
will be in the halting state after $f(n)$ iterations of the simulation. Counting
the iterations to $f(n)$ is achieved via the counter flags. 

Finally the simulator extracts from each code symbol the symbol corresponding to
$M$'s output tape, thus reconstructing the output of $M$ on the simulator's
output tape. Thanks to the start flags, the simulator can easily locate the
leftmost cell and put the output tape head one to the right of it, as required.

The construction heavily uses the memorization-in-states technique (see
Chapter~\ref{s:tm-memorizing}). At first the machine features $2k + 1$
memorization tapes in addition to the input tape and output tape. The purpose of
those tapes is to store $M$'s state and the symbols under the tape heads of $M$
in the currently simulated step of $M$'s execution, as well as the $k$ symbols
to be written write and head movements to be executed by the simulator.
›

text ‹
The next predicate expresses that a Turing machine halts within a time bound
depending on the length of the input. We did not have a need for this fairly
basic predicate yet, because so far we were always interested in the halting
configuration, too, and so the predicate @{const computes_in_time} sufficed.

\null
›

definition time_bound :: "machine ⇒ nat ⇒ (nat ⇒ nat) ⇒ bool" where
  "time_bound M k T ≡
    ∀zs. bit_symbols zs ⟶ fst (execute M (start_config k zs) (T (length zs))) = length M"

lemma time_bound_ge:
  assumes "time_bound M k T" and "∀n. fmt n ≥ T n"
  shows "time_bound M k fmt"
  using time_bound_def assms by (metis execute_after_halting_ge)

text ‹
The time bound also bounds the position of all the tape heads.
›

lemma head_pos_le_time_bound:
  assumes "turing_machine k G M"
    and "time_bound M k T"
    and "bit_symbols zs"
    and "j < k"
  shows "execute M (start_config k zs) t <#> j ≤ T (length zs)"
  using assms time_bound_def[of M k T] execute_after_halting_ge head_pos_le_time[OF assms(1,4)]
  by (metis (no_types, lifting) nat_le_linear)

text ‹
The entire construction will take place in a locale that assumes a
polynomial-time $k$-tape Turing machine $M$.
›

locale two_tape =
  fixes M :: machine and k G :: nat and T :: "nat ⇒ nat"
  assumes tm_M: "turing_machine k G M"
    and poly_T: "big_oh_poly T"
    and time_bound_T: "time_bound M k T"
begin

lemma k_ge_2: "k ≥ 2"
  using tm_M turing_machine_def by simp

lemma G_ge_4: "G ≥ 4"
  using tm_M turing_machine_def by simp

text ‹
The construction of the simulator relies on the formatted space on the output
tape to be large enough to hold the input. The size of the formatted space
depends on the time bound $T$, which might be less than the length of the input.
To ensure that the formatted space is large enough we increase the time bound
while keeping it polynomial. The new bound is $T'$:
›

definition T' :: "nat ⇒ nat" where
  "T' n ≡ T n + n"

lemma poly_T': "big_oh_poly T'"
proof -
  have "big_oh_poly (λn. n)"
    using big_oh_poly_poly[of 1] by simp
  then show ?thesis
    using T'_def big_oh_poly_sum[OF poly_T] by presburger
qed

lemma time_bound_T': "time_bound M k T'"
  using T'_def time_bound_ge[OF time_bound_T, of T'] by simp


subsection ‹Encoding multiple tapes into one›

text ‹
The symbols on the output tape of the simulator are supposed to encode a $(2k +
2)$-tuple, where the first $k$ elements assume one of the values in $\{0, \dots,
G - 1\}$, whereas the other $k + 2$ are flags with two possible values only. For
uniformity we define an encoding where all elements range over $G$ values and
that works for tuples of every length.
›

fun encode :: "nat list ⇒ nat" where
  "encode [] = 0" |
  "encode (x # xs) = x + G * encode xs"

text ‹
For every $m \in \nat$, the enocoding is a bijective mapping from $\{0, \dots,
G - 1\}^m$ to $\{0, \dots, G^m - 1\}$.
›

lemma encode_surj:
  assumes "n < G ^ m"
  shows "∃xs. length xs = m ∧ (∀x∈set xs. x < G) ∧ encode xs = n"
  using assms
proof (induction m arbitrary: n)
  case 0
  then show ?case
    by simp
next
  case (Suc m)
  define q where "q = n div G"
  define r where "r = n mod G"
  have "q < G ^ m"
    using Suc q_def
    by (auto simp add: less_mult_imp_div_less power_commutes)
  then obtain xs' where xs': "length xs' = m" "∀x∈set xs'. x < G" "encode xs' = q"
    using Suc by auto
  have "r < G"
    using r_def G_ge_4 by simp
  have "encode (r # xs') = n"
    using xs'(3) q_def r_def G_ge_4 by simp
  moreover have "∀x∈set (r # xs'). x < G"
    using xs'(2) `r < G` by simp
  moreover have "length (r # xs') = Suc m"
    using xs'(1) by simp
  ultimately show ?case
    by blast
qed

lemma encode_inj:
  assumes "∀x∈set xs. x < G"
    and "length xs = m"
    and "∀y∈set ys. y < G"
    and "length ys = m"
    and "encode xs = encode ys"
  shows "xs = ys"
  using assms
proof (induction m arbitrary: xs ys)
  case 0
  then show ?case
    by simp
next
  case (Suc m)
  obtain x xs' y ys' where xy: "xs = x # xs'" "ys = y # ys'"
    using Suc by (metis Suc_length_conv)
  then have len: "length xs' = m" "length ys' = m"
    using Suc by simp_all
  have *: "x + G * encode xs' = y + G * encode ys'"
    using Suc xy by simp
  moreover have "(x + G * encode xs') mod G = x"
    by (simp add: Suc.prems(1) xy(1))
  moreover have "(y + G * encode ys') mod G = y"
    by (simp add: Suc.prems(3) xy(2))
  ultimately have "x = y"
    by simp
  with * have "G * encode xs' = G * encode ys'"
    by simp
  then have "encode xs' = encode ys'"
    using G_ge_4 by simp
  with len Suc xy have "xs' = ys'"
    by simp
  then show ?case
    using `x = y` xy by simp
qed

lemma encode_less:
  assumes "∀x∈set xs. x < G"
  shows "encode xs < G ^ (length xs)"
  using assms
proof (induction xs)
  case Nil
  then show ?case
    by simp
next
  case (Cons x xs)
  then have "x < G"
    by simp
  have "encode (x # xs) = x + G * encode xs"
    by simp
  also have "... ≤ x + G * (G ^ (length xs) - 1)"
    using Cons by simp
  also have "... = x + G * G ^ (length xs) - G"
    by (simp add: right_diff_distrib')
  also have "... < G * G ^ (length xs)"
    using `x < G` less_imp_Suc_add by fastforce
  also have "... = G ^ (Suc (length xs))"
    by simp
  finally have "encode (x # xs) < G ^ (length (x # xs))"
    by simp
  then show ?case .
qed

text ‹
Decoding a number into an $m$-tuple of numbers is then a well-defined operation.
›

definition decode :: "nat ⇒ nat ⇒ nat list" where
  "decode m n ≡ THE xs. encode xs = n ∧ length xs = m ∧ (∀x∈set xs. x < G)"

lemma decode:
  assumes "n < G ^ m"
  shows encode_decode: "encode (decode m n) = n"
    and length_decode: "length (decode m n) = m"
    and decode_less_G: "∀x∈set (decode m n). x < G"
proof -
  have "∃xs. length xs = m ∧ (∀x∈set xs. x < G) ∧ encode xs = n"
    using assms encode_surj by simp
  then have *: "∃!xs. encode xs = n ∧ length xs = m ∧ (∀x∈set xs. x < G)"
    using encode_inj by auto
  let ?xs = "decode m n"
  let ?P = "λxs. encode xs = n ∧ length xs = m ∧ (∀x∈set xs. x < G)"
  have "encode ?xs = n ∧ length ?xs = m ∧ (∀x∈set ?xs. x < G)"
    using * theI'[of ?P] decode_def by simp
  then show "encode (decode m n) = n" and "length (decode m n) = m" and "∀x∈set (decode m n). x < G"
    by simp_all
qed

lemma decode_encode: "∀x∈set xs. x < G ⟹ decode (length xs) (encode xs) = xs"
proof -
  fix xs :: "nat list"
  assume a: "∀x∈set xs. x < G"
  then have "encode xs < G ^ (length xs)"
    using encode_less by simp
  show "decode (length xs) (encode xs) = xs"
    unfolding decode_def
  proof (rule the_equality)
   show "encode xs = encode xs ∧ length xs = length xs ∧ (∀x∈set xs. x < G)"
     using a by simp
   show "⋀ys. encode ys = encode xs ∧ length ys = length xs ∧ (∀x∈set ys. x < G) ⟹ ys = xs"
     using a encode_inj by simp
  qed
qed

text ‹
The simulator will access and update components of the encoded symbol.
›

definition encode_nth :: "nat ⇒ nat ⇒ nat ⇒ nat" where
  "encode_nth m n j ≡ decode m n ! j"

definition encode_upd :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat" where
  "encode_upd m n j x ≡ encode ((decode m n) [j:=x])"

lemma encode_nth_less:
  assumes "n < G ^ m" and "j < m"
  shows "encode_nth m n j < G"
  using assms encode_nth_def decode_less_G length_decode by simp

text ‹
For the symbols the simulator actually uses, we fix $m = 2k + 2$ and reserve the
symbols $\triangleright$ and $\Box$, effectively shifting the symbols by two. We
call the symbols $\{2, \dots, G^{2k+2} + 2\}$ ``code symbols''.
›

definition enc :: "symbol list ⇒ symbol" where
  "enc xs ≡ encode xs + 2"

definition dec :: "symbol ⇒ symbol list" where
  "dec n ≡ decode (2 * k + 2) (n - 2)"

lemma dec:
  assumes "n > 1" and "n < G ^ (2 * k + 2) + 2"
  shows enc_dec: "enc (dec n) = n"
    and length_dec: "length (dec n) = 2 * k + 2"
    and dec_less_G: "∀x∈set (dec n). x < G"
proof -
  show "enc (dec n) = n"
    using enc_def dec_def encode_decode assms by simp
  show "length (dec n) = 2 * k + 2"
    using enc_def dec_def length_decode assms by simp
  show "∀x∈set (dec n). x < G"
    using enc_def dec_def decode_less_G assms
    by (metis Suc_leI less_diff_conv2 one_add_one plus_1_eq_Suc)
qed

lemma dec_enc: "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ dec (enc xs) = xs"
  unfolding enc_def dec_def using decode_encode by fastforce

definition enc_nth :: "nat ⇒ nat ⇒ nat" where
  "enc_nth n j ≡ dec n ! j"

lemma enc_nth: "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ enc_nth (enc xs) j = xs ! j"
  unfolding enc_nth_def by (simp add: dec_enc)

lemma enc_nth_dec:
  assumes "n > 1" and "n < G ^ (2 * k + 2) + 2"
  shows "enc_nth n j = (dec n) ! j"
  using assms enc_nth dec by metis

abbreviation is_code :: "nat ⇒ bool" where
  "is_code n ≡ n < G ^ (2 * k + 2) + 2 ∧ 1 < n"

lemma enc_nth_less:
  assumes "is_code n" and "j < 2 * k + 2"
  shows "enc_nth n j < G"
  using assms enc_nth_def by (metis dec_less_G in_set_conv_nth length_dec)

lemma enc_less: "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ enc xs < G ^ (2 * k + 2) + 2"
  using encode_less enc_def by fastforce

definition enc_upd :: "nat ⇒ nat ⇒ nat ⇒ nat" where
  "enc_upd n j x ≡ enc ((dec n) [j:=x])"

lemma enc_upd_is_code:
  assumes "is_code n" and "j < 2 * k + 2" and "x < G"
  shows "is_code (enc_upd n j x)"
proof -
  let ?ys = "(dec n) [j:=x]"
  have "∀h∈set (dec n). h < G"
    using assms(1,2) dec_less_G by auto
  then have "∀h∈set ?ys. h < G"
    using assms(3)
    by (metis in_set_conv_nth length_list_update nth_list_update_eq nth_list_update_neq)
  moreover have "length ?ys = 2 * k + 2"
    using assms length_dec by simp
  ultimately have "enc ?ys < G ^ (2 * k + 2) + 2"
    using enc_less by simp
  then show ?thesis
    using enc_upd_def enc_def by simp
qed

text ‹
The code symbols require the simulator to have an alphabet of at least size
$G^{2k + 2} + 2$. On top of that we want to store on a memorization tape the
state that $M$ is in. So the alphabet must have at least @{term "length M + 1"}
symbols. Both conditions are met by the simulator having an alphabet of size
$G'$:
›

definition G' :: nat where
  "G' ≡ G ^ (2 * k + 2) + 2 + length M"

lemma G'_ge_6: "G' ≥ 6"
proof -
  have "4 ^ 2 > (5::nat)"
    by simp
  then have "G ^ 2 > (5::nat)"
    using G_ge_4 less_le_trans power2_nat_le_eq_le by blast
  then have "G ^ (2 * k + 2) > (5::nat)"
    using k_ge_2 G_ge_4
    by (metis (no_types, opaque_lifting) dec_induct le_add2 order_less_le_subst1 pow_mono zero_less_Suc zero_less_numeral)
  then show ?thesis
    using G'_def by simp
qed

corollary G'_ge: "G' ≥ 4" "G' ≥ 5"
  using G'_ge_6 by simp_all

lemma G'_ge_G: "G' ≥ G"
proof -
  have "G ^ 2 ≥ G"
    by (simp add: power2_nat_le_imp_le)
  then have "G ^ (2 * k + 2) ≥ G"
    by simp
  then show ?thesis using G'_def
    by linarith
qed

corollary enc_less_G': "∀x∈set xs. x < G ⟹ length xs = 2 * k + 2 ⟹ enc xs < G'"
  using enc_less G'_def by fastforce

lemma enc_greater: "enc xs > 1"
  using enc_def by simp


subsection ‹Construction of the simulator Turing machine›

text ‹
The simulator is a sequence of three Turing machines: The ``formatter'', which
initializes the output tape; the loop, which simulates the TM $M$ for
polynomially many steps; and a cleanup TM, which makes the output tape look like
the output tape of $M$. All these machines are discussed in order in the
following subsections.

The simulator will start with $2k + 1$ memorization tapes for a total of $2k +
3$ tapes. The simulation action will take place on the output tape.
›


subsubsection ‹Initializing the simulator's tapes›

text ‹
The function @{const T'} is polynomially bounded and therefore there is a
polynomial-time two-tape oblivious Turing machine that outputs at least $T'(n)$
symbols~@{text 𝟭} on an input of length $n$, as we have proven in the previous
section (lemma~@{thm [source] polystructor}). We now obtain such a Turing
machine together with its running time bound and trace. This TM will be one of
our blocks for building the simulator TM. We will call it the ``formatter''.

\null
›

definition fmt_es_pM :: "(nat ⇒ nat) × (nat ⇒ (nat × nat) list) × machine" where
  "fmt_es_pM ≡ SOME tec.
    turing_machine 2 G' (snd (snd tec)) ∧
    big_oh_poly (λn. length ((fst (snd tec)) n)) ∧
    big_oh_poly (fst tec) ∧
    (∀n. T' n ≤ (fst tec) n) ∧
    (∀zs. proper_symbols zs ⟶ traces (snd (snd tec)) (start_tapes_2 zs) ((fst (snd tec)) (length zs)) (one_tapes_2 zs ((fst tec) (length zs))))"

lemma polystructor':
  fixes GG :: nat and g :: "nat ⇒ nat"
  assumes "big_oh_poly g" and "GG ≥ 5"
  shows "∃f_es_M.
    turing_machine 2 GG (snd (snd f_es_M)) ∧
    big_oh_poly (λn. length ((fst (snd f_es_M)) n)) ∧
    big_oh_poly (fst f_es_M) ∧
    (∀n. g n ≤ (fst f_es_M) n) ∧
    (∀zs. proper_symbols zs ⟶ traces (snd (snd f_es_M)) (start_tapes_2 zs) ((fst (snd f_es_M)) (length zs)) (one_tapes_2 zs ((fst f_es_M) (length zs))))"
  using polystructor[OF assms] by auto

lemma fmt_es_pM: "turing_machine 2 G' (snd (snd fmt_es_pM)) ∧
    big_oh_poly (λn. length ((fst (snd fmt_es_pM)) n)) ∧
    big_oh_poly (fst fmt_es_pM) ∧
    (∀n. T' n ≤ (fst fmt_es_pM) n) ∧
    (∀zs. proper_symbols zs ⟶ traces (snd (snd fmt_es_pM)) (start_tapes_2 zs) ((fst (snd fmt_es_pM)) (length zs)) (one_tapes_2 zs ((fst fmt_es_pM) (length zs))))"
  using fmt_es_pM_def polystructor'[OF poly_T' G'_ge(2)]
    someI_ex[of "λtec.
      turing_machine 2 G' (snd (snd tec)) ∧
      big_oh_poly (λn. length ((fst (snd tec)) n)) ∧
      big_oh_poly (fst tec) ∧
      (∀n. T' n ≤ (fst tec) n) ∧
      (∀zs. proper_symbols zs ⟶ traces (snd (snd tec)) (start_tapes_2 zs) ((fst (snd tec)) (length zs)) (one_tapes_2 zs ((fst tec) (length zs))))"]
  by simp

definition fmt :: "nat ⇒ nat" where
  "fmt ≡ fst fmt_es_pM"

definition es_fmt :: "nat ⇒ (nat × nat) list" where
  "es_fmt ≡ fst (snd fmt_es_pM)"

definition tm_fmt :: "machine" where
  "tm_fmt ≡ snd (snd fmt_es_pM)"

text ‹
The formatter TM is @{const tm_fmt}, the number of @{text 𝟭} symbols written to
the output tape on input of length $n$ is @{term "fmt n"}, and the trace on
inputs of length $n$ is @{term "es_fmt n"}.
›

lemma fmt:
  "turing_machine 2 G' tm_fmt"
  "big_oh_poly (λn. length (es_fmt n))"
  "big_oh_poly fmt"
  "⋀n. T' n ≤ fmt n"
  "⋀zs. proper_symbols zs ⟹
    traces tm_fmt (start_tapes_2 zs) (es_fmt (length zs)) (one_tapes_2 zs (fmt (length zs)))"
  unfolding fmt_def es_fmt_def tm_fmt_def using fmt_es_pM by simp_all

lemma fmt_ge_n: "fmt n ≥ n"
  using fmt(4) T'_def by (metis dual_order.strict_trans2 le_less_linear not_add_less2)

text ‹
The formatter is a two-tape TM. The first incarnation of the simulator will have
two tapes and $2k + 1$ memorization tapes.  So for now we formally need to
extend the formatter to $2k + 3$ tapes:
›

definition "tm1 ≡ append_tapes 2 (2 * k + 3) tm_fmt"

lemma tm1_tm: "turing_machine (2 * k + 3) G' tm1"
  unfolding tm1_def using append_tapes_tm by (simp add: fmt(1))

text ‹
Next we replace all non-blank symbols on the output tape by code symbols
representing the tuple of $2k + 2$ zeros.
›

definition "tm1_2 ≡ tm_const_until 1 1 {□} (enc (replicate k 0 @ replicate k 0 @ [0, 0]))"

lemma tm1_2_tm: "turing_machine (2 * k + 3) G' tm1_2"
  unfolding tm1_2_def
  using G'_ge
proof (intro tm_const_until_tm, auto)
  show "enc (replicate k 0 @ replicate k 0 @ [0, 0]) < G'"
    using G_ge_4 by (intro enc_less_G', auto)
qed

definition "tm2 ≡ tm1 ;; tm1_2"

lemma tm2_tm: "turing_machine (2 * k + 3) G' tm2"
  unfolding tm2_def using tm1_tm tm1_2_tm by simp

definition "tm3 ≡ tm2 ;; tm_start 1"

lemma tm3_tm: "turing_machine (2 * k + 3) G' tm3"
  unfolding tm3_def using tm2_tm tm_start_tm G'_ge by simp

text ‹
Back at the start symbol of the output tape, we replace it by the code symbol
for the tuple $1^k1^k01$. The first $k$ ones represent that initially the $k$
tapes of $M$ have the start symbol (numerically 1) in the leftmost cell.  The
second run of $k$ ones represent that initially all $k$ tapes have their tape
heads in the leftmost cell. The following 0 is the first bit of the unary
counter, currently set to zero. The final flag~1  signals that this is the
leftmost cell. Unlike the start symbols this signal flag cannot be overwritten
by $M$.
›

definition "tm4 ≡ tm3 ;; tm_write 1 (enc (replicate k 1 @ replicate k 1 @ [0, 1]))"

lemma tm3_4_tm: "turing_machine (2 * k + 3) G' (tm_write 1 (enc (replicate k 1 @ replicate k 1 @ [0, 1])))"
  using G'_ge enc_less_G' G_ge_4 tm_write_tm by simp

lemma tm4_tm: "turing_machine (2 * k + 3) G' tm4"
  unfolding tm4_def using tm3_tm tm3_4_tm by simp

definition "tm5 ≡ tm4 ;; tm_right 1"

lemma tm5_tm: "turing_machine (2 * k + 3) G' tm5"
  unfolding tm5_def using tm4_tm by (simp add: G'_ge(1) tm_right_tm)

text ‹
So far the simulator's output tape encodes $k$ tapes that are empty but for the
start symbols. To represent the start configuration of $M$, we need to copy the
contents of the input tape to the output tape. The following TM moves the work
head to the first blank while copying the input tape content. Here we exploit
$T'(n) \geq n$, which implies that the formatted section is long enough to hold
the input.
›

definition "tm5_6 ≡ tm_trans_until 0 1 {0} (λh. enc (h mod G # replicate (k - 1) 0 @ replicate k 0 @ [0, 0]))"

definition "tm6 ≡ tm5 ;; tm5_6"

lemma tm5_6_tm: "turing_machine (2 * k + 3) G' tm5_6"
  unfolding tm5_6_def
proof (rule tm_trans_until_tm, auto simp add: G'_ge(1) G_ge_4 k_ge_2 enc_less_G')
  show "⋀h. h < G' ⟹ enc (h mod G # replicate (k - Suc 0) 0 @ replicate k 0 @ [0, 0]) < G'"
    using G_ge_4 k_ge_2 enc_less_G' by simp
qed

lemma tm6_tm: "turing_machine (2 * k + 3) G' tm6"
  unfolding tm6_def using tm5_tm tm5_6_tm by simp

text ‹
Since we have overwritten the leftmost cell of the output tape with some code
symbol, we cannot return to it using @{const tm_start}. But we can use @{const
tm_left_until} with a special set of symbols:
›

abbreviation StartSym :: "symbol set" where
  "StartSym ≡ {y. y < G ^ (2 * k + 2) + 2 ∧ y > 1 ∧ dec y ! (2 * k + 1) = 1}"

abbreviation "tm_left_until1 ≡ tm_left_until StartSym 1"

lemma tm_left_until1_tm: "turing_machine (2 * k + 3) G' tm_left_until1"
  using tm_left_until_tm G'_ge(1) k_ge_2 by simp

definition "tm7 ≡ tm6 ;; tm_left_until1"

lemma tm7_tm: "turing_machine (2 * k + 3) G' tm7"
  unfolding tm7_def using tm6_tm tm_left_until1_tm by simp

text ‹
Tape number $2$ is meant to memorize $M$'s state during the simulation.
Initially the state is the start state, that is, zero.
›

definition "tm8 ≡ tm7 ;; tm_write 2 0"

lemma tm8_tm: "turing_machine (2 * k + 3) G' tm8"
  unfolding tm8_def using tm7_tm tm_write_tm k_ge_2 G'_ge(1) by simp

text ‹
We also initialize memorization tapes $3, \dots, 2k + 2$ to zero. This concludes
the initialization of the simulator's tapes.
›

definition "tm9 ≡ tm8 ;; tm_write_many {3..<2 * k + 3} 0"

lemma tm9_tm: "turing_machine (2 * k + 3) G' tm9"
  unfolding tm9_def using tm8_tm tm_write_many_tm k_ge_2 G'_ge(1) by simp


subsubsection ‹The loop›

text ‹
The core of the simulator is a loop whose body is executed @{term "fmt n"} many
times. Each iteration simulates one step of the Turing machine $M$.  For the
analysis of the loop we describe the $2k + 3$ tapes in the form @{term "[a, b,
c] @ map f1 [0..<k] @ map f2 [0..<k]"}.
›

lemma threeplus2k_2:
  assumes "3 ≤ j ∧ j < k + 3"
  shows "([a, b, c] @ map f1 [0..<k] @ map f2 [0..<k]) ! j = f1 (j - 3)"
  using assms by (simp add: nth_append less_diff_conv2 numeral_3_eq_3)

lemma threeplus2k_3:
  assumes "k + 3 ≤ j ∧ j < 2 * k + 3"
  shows "([a, b, c] @ map f1 [0..<k] @ map f2 [0..<k]) ! j = f2 (j - k - 3)"
  using assms by (simp add: nth_append less_diff_conv2 numeral_3_eq_3)

text ‹
To ensure the loop runs for @{term "fmt n"} iterations we increment the unary
counter in the code symbols in each iteration. The loop terminates when there
are no more code symbols with an unset counter flag. The TM that prepares the
loop condition sweeps the output tape left-to-right searching for the first symbol
that is either blank or has an unset counter flag. The condition then checks for
which of the two cases occurred. This is the condition TM: ›

definition "tmC ≡ tm_right_until 1 {y. y < G ^ (2 * k + 2) + 2 ∧ (y = 0 ∨ dec y ! (2 * k) = 0)}"

lemma tmC_tm: "turing_machine (2 * k + 3) G' tmC"
  using tmC_def tm_right_until_tm using G'_ge(1) by simp

text ‹
At the start of the iteration, the memorization tape~2 has the state of $M$, and
all other memorization tapes contain $0$. The output tape head is at the leftmost
code symbol with unset counter flag. The first order of business is to move back
to the beginning of the output tape.
›

definition "tmL1 ≡ tm_left_until1"

lemma tmL1_tm: "turing_machine (2 * k + 3) G' tmL1"
  unfolding tmL1_def using tm6_tm tm_left_until1_tm by simp

text ‹
Then the output tape head sweeps right until it encounters a blank. During the
sweep the Turing machine checks for any set head flags, and if it finds the one
for tape $j$ set, it memorizes the symbol for tape $j$ on tape $3 + k + j$.  The
next command performs this operation:
›

definition cmdL2 :: command where
  "cmdL2 rs ≡
    (if rs ! 1 = □
     then (1, zip rs (replicate (2*k+3) Stay))
     else
      (0,
       [(rs!0, Stay), (rs!1, Right), (rs!2, Stay)] @
       (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @
       (map (λj. (if 1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2 ∧ enc_nth (rs!1) (k+j) = 1 then enc_nth (rs!1) j else rs!(3+k+j), Stay)) [0..<k])))"

lemma cmdL2_at_eq_0:
  assumes "rs ! 1 = 0" and "j < 2 * k + 3" and "length rs = 2 * k + 3"
  shows "snd (cmdL2 rs) ! j = (rs ! j, Stay)"
  using assms by (simp add: cmdL2_def)

lemma cmdL2_at_3:
  assumes "rs ! 1 ≠ □" and "3 ≤ j ∧ j < k + 3"
  shows "cmdL2 rs [!] j = (rs ! j, Stay)"
  using cmdL2_def assms threeplus2k_2
  by (metis (no_types, lifting) le_add_diff_inverse2 snd_conv)

lemma cmdL2_at_4:
  assumes "rs ! 1 ≠ □" and "k + 3 ≤ j ∧ j < 2 * k + 3"
  shows "cmdL2 rs [!] j =
     (if 1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2 ∧ enc_nth (rs ! 1) (j-3) = 1
      then enc_nth (rs ! 1) (j-k-3)
      else rs ! j, Stay)"
  unfolding cmdL2_def using assms threeplus2k_3[OF assms(2), of "(rs ! 0, Stay)"] by simp

lemma cmdL2_at_4'':
  assumes "rs ! 1 ≠ □"
    and "k + 3 ≤ j ∧ j < 2 * k + 3"
    and "¬ (1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2)"
  shows "cmdL2 rs [!] j = (rs ! j, Stay)"
proof -
  have "cmdL2 rs [!] j =
      (if 1 < rs ! 1 ∧ rs ! 1 < G^(2*k+2)+2 ∧ enc_nth (rs!1) (j-3) = 1 then enc_nth (rs!1) (j-k-3) else rs!j, Stay)"
    using assms cmdL2_at_4 by blast
  then show ?thesis
    using assms(3) by auto
qed

lemma turing_command_cmdL2: "turing_command (2 * k + 3) 1 G' cmdL2"
proof
  show "⋀gs. length gs = 2 * k + 3 ⟹ length ([!!] cmdL2 gs) = length gs"
    unfolding cmdL2_def by simp
  show "⋀gs. length gs = 2 * k + 3 ⟹ 0 < 2 * k + 3 ⟹ cmdL2 gs [.] 0 = gs ! 0"
    unfolding cmdL2_def by simp
  show "cmdL2 gs [.] j < G'"
      if "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" "j < length gs"
      for gs j
  proof (cases "gs ! 1 = 0")
    case True
    then have "cmdL2 gs = (1, zip gs (replicate (2*k+3) Stay))"
      unfolding cmdL2_def by simp
    have "cmdL2 gs [.] j = gs ! j"
      using that(1,3) by (simp add: ‹cmdL2 gs = (1, zip gs (replicate (2 * k + 3) Stay))›)
    then show ?thesis
      using that(2,3) by simp
  next
    case False
    consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
      using ‹j < length gs› ‹length gs = 2 * k + 3› by linarith
    then show ?thesis
    proof (cases)
      case 1
      then show ?thesis
        by (simp add: cmdL2_def that(1) that(2))
    next
      case 2
      then show ?thesis
        unfolding cmdL2_def using False that by auto
    next
      case 3
      then show ?thesis
        unfolding cmdL2_def using False that by auto
    next
      case 4
      then have "snd (cmdL2 gs) ! j = (gs ! j, Stay)"
        unfolding cmdL2_def using False that threeplus2k_2[OF 4, of "(gs ! 0, Stay)"] by simp
      then show ?thesis
        using that by (simp add: ‹snd (cmdL2 gs) ! j = (gs ! j, Stay)›)
    next
      case 5
      show ?thesis
      proof (cases "1 < gs ! 1 ∧ gs ! 1 < G ^ (2*k+2) + 2")
        case True
        then have *: "cmdL2 gs [.] j = (if enc_nth (gs ! 1) (j-3) = 1 then enc_nth (gs ! 1) (j-k-3) else gs ! j)"
          using 5 False by (simp add: cmdL2_at_4)
        let ?n = "gs ! 1"
        have len: "length (dec ?n) = 2 * k + 2" and less_G: "∀x∈set (dec ?n). x < G"
          using True length_dec dec_less_G by (simp, blast)
        have **: "enc_nth ?n (j-k-3) = dec ?n ! (j-k-3)"
          using enc_nth_dec True by simp
        then have "dec ?n ! (j-k-3) < G"
          using less_G 5 len by auto
        then have "dec ?n ! (j-k-3) < G'"
          using G'_ge_G by simp
        moreover have "gs ! j < G'"
          using that by simp
        ultimately show ?thesis
          using * ** by simp
      next
        case 6: False
        have "cmdL2 gs [!] j = (gs ! j, Stay)"
          using cmdL2_at_4''[OF False 5 6] by simp
        then show ?thesis
          using that by (simp add: ‹snd (cmdL2 gs) ! j = (gs ! j, Stay)›)
      qed
    qed
  qed
  show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL2 gs) ≤ 1"
    using cmdL2_def by simp
qed

definition "tmL1_2 ≡ [cmdL2]"

lemma tmL1_2_tm: "turing_machine (2 * k + 3) G' tmL1_2"
  using tmL1_2_def using turing_command_cmdL2 G'_ge by auto

definition "tmL2 ≡ tmL1 ;; tmL1_2"

lemma tmL2_tm: "turing_machine (2 * k + 3) G' tmL2"
  by (simp add: tmL1_2_tm tmL1_tm tmL2_def)

text ‹
The memorization tapes $3, \dots, 2 + k$ will store the head movements for
tapes $0, \dots, k - 1$ of $M$. The directions are encoded as symbols thus:
›

definition direction_to_symbol :: "direction ⇒ symbol" where
  "direction_to_symbol m ≡ (case m of Left ⇒ □ | Stay ⇒ ▹ | Right ⇒ 𝟬)"

lemma direction_to_symbol_less: "direction_to_symbol m < 3"
  using direction_to_symbol_def by (cases m) simp_all

text ‹
At this point in the iteration the memorization tapes $k + 3, \dots, 2k+2$
contain the symbols under the $k$ tape heads of $M$, and tape $2$ contains the
state $M$ is in. Therefore all information is available to determine the actions
$M$ is taking in the step currently simulated.  The next command has the entire
behavior of $M$ ``hard-coded'' and causes the actions to be stored on
memorization tapes $3, \dots, 2k+2$: the output symbols on the tapes $k + 3,
\dots, 2k + 2$, and the $k$ head movements on the tapes $3, \dots, k + 2$. The
follow-up state will again be memorized on tape $2$. All this happens in one
step of the simulator machine.
›

definition cmdL3 :: command where
  "cmdL3 rs ≡
   (1,
    [(rs ! 0, Stay),
     (rs ! 1, Stay),
     (if rs ! 2 < length M ∧ (∀h∈set (drop (k + 3) rs). h < G)
      then fst ((M ! (rs ! 2)) (drop (k + 3) rs))
      else rs ! 2, Stay)] @
    map
      (λj. (if rs ! 2 < length M ∧ (∀h∈set (drop (k + 3) rs). h < G) then direction_to_symbol ((M ! (rs ! 2)) (drop (k + 3) rs) [~] j) else 1, Stay))
      [0..<k] @
    map (λj. (if rs ! 2 < length M ∧ (∀h∈set (drop (k + 3) rs). h < G) then ((M ! (rs ! 2)) (drop (k + 3) rs) [.] j) else rs ! (k + 3 + j), Stay)) [0..<k])"

lemma cmdL3_at_2a:
  assumes "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)"
  shows "cmdL3 gs [!] 2 = (fst ((M ! (gs ! 2)) (drop (k + 3) gs)), Stay)"
  using cmdL3_def assms by simp

lemma cmdL3_at_2b:
  assumes "¬ (gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G))"
  shows "cmdL3 gs [!] 2 = (gs ! 2, Stay)"
  using cmdL3_def assms by auto

lemma cmdL3_at_3a:
  assumes "3 ≤ j ∧ j < k + 3"
    and "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)"
  shows "cmdL3 gs [!] j = (direction_to_symbol ((M ! (gs ! 2)) (drop (k + 3) gs) [~] (j - 3)), Stay)"
  using cmdL3_def assms(2) threeplus2k_2[OF assms(1), of "(gs ! 0, Stay)"] by simp

lemma cmdL3_at_3b:
  assumes "3 ≤ j ∧ j < k + 3"
    and "¬ (gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G))"
  shows "cmdL3 gs [!] j = (1, Stay)"
  using cmdL3_def assms(2) threeplus2k_2[OF assms(1), of "(gs ! 0, Stay)"] by auto

lemma cmdL3_at_4a:
  assumes "k + 3 ≤ j ∧ j < 2 * k + 3"
    and "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)"
  shows "cmdL3 gs [!] j = ((M ! (gs ! 2)) (drop (k + 3) gs) [.] (j - k - 3), Stay)"
  using cmdL3_def assms(2) threeplus2k_3[OF assms(1), of "(gs ! 0, Stay)"] by simp

lemma cmdL3_at_4b:
  assumes "k + 3 ≤ j ∧ j < 2 * k + 3"
    and "¬ (gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G))"
  shows "cmdL3 gs [!] j = (gs ! j, Stay)"
  using assms cmdL3_def threeplus2k_3[OF assms(1), of "(gs ! 0, Stay)"] by auto

lemma cmdL3_if_comm:
  assumes "length gs = 2 * k + 3" and "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)"
  shows "length ([!!] (M ! (gs ! 2)) (drop (k + 3) gs)) = k"
    and "⋀j. j < k ⟹ (M ! (gs ! 2)) (drop (k + 3) gs) [.] j < G"
proof -
  let ?rs = "drop (k + 3) gs"
  let ?cmd = "M ! (gs ! 2)"
  have *: "turing_command k (length M) G ?cmd"
    using assms(2) tm_M turing_machineD(3) by simp
  then show "length ([!!] ?cmd ?rs) = k"
    using turing_commandD(1) assms(1) by simp
  have "⋀i. i < length ?rs ⟹ ?rs ! i < G"
    using assms(2) nth_mem by blast
  then show "⋀j. j < k ⟹ (M ! (gs ! 2)) (drop (k + 3) gs) [.] j < G"
    using * turing_commandD(2) assms by simp
qed

lemma turing_command_cmdL3: "turing_command (2 * k + 3) 1 G' cmdL3"
proof
  show "⋀gs. length gs = 2 * k + 3 ⟹ length ([!!] cmdL3 gs) = length gs"
    using cmdL3_def by simp
  show "⋀gs. length gs = 2 * k + 3 ⟹ 0 < 2 * k + 3 ⟹ cmdL3 gs [.] 0 = gs ! 0"
    using cmdL3_def by simp
  show "cmdL3 gs [.] j < G'"
    if "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" "j < length gs"
    for gs j
  proof -
    consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
      using ‹j < length gs› ‹length gs = 2 * k + 3› by linarith
    then show ?thesis
    proof (cases)
      case 1
      then show ?thesis
        using that cmdL3_def by simp
    next
      case 2
      then show ?thesis
        using that cmdL3_def by simp
    next
      case 3
      then show ?thesis
      proof (cases "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)")
        case True
        have "length (drop (k + 3) gs) = k"
          using that(1) by simp
        then have "fst ((M ! (gs ! 2)) (drop (k + 3) gs)) ≤ length M"
          using True turing_commandD(4) tm_M turing_machineD(3) by blast
        moreover have "cmdL3 gs [.] j = fst ((M ! (gs ! 2)) (drop (k + 3) gs))"
          using cmdL3_def True 3 by simp
        ultimately show ?thesis
          using G'_def by simp
      next
        case False
        then have "cmdL3 gs [.] j = gs ! 2"
          using cmdL3_def 3 by auto
        then show ?thesis
          using 3 that(2,3) by simp
      qed
    next
      case 4
      then show ?thesis
      proof (cases "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)")
        case True
        then have "cmdL3 gs [.] j = direction_to_symbol ((M ! (gs ! 2)) (drop (k + 3) gs) [~] (j - 3))"
          using cmdL3_at_3a 4 by simp
        then have "cmdL3 gs [.] j < 3"
          using direction_to_symbol_less by simp
        then show ?thesis
          using G'_ge by simp
      next
        case False
        then show ?thesis
          using cmdL3_at_3b[OF 4] G'_ge by simp
      qed
    next
      case 5
      then show ?thesis
      proof (cases "gs ! 2 < length M ∧ (∀h∈set (drop (k + 3) gs). h < G)")
        case True
        then have "cmdL3 gs [.] j = (M ! (gs ! 2)) (drop (k + 3) gs) [.] (j - k - 3)"
          using cmdL3_at_4a[OF 5] by simp
        then have "cmdL3 gs [.] j < G"
          using cmdL3_if_comm True 5 that(1) by auto
        then show ?thesis
          using G'_ge_G by simp
      next
        case False
        then have "cmdL3 gs [.] j = gs ! j"
          using cmdL3_at_4b[OF 5] by simp
        then show ?thesis
          using that by simp
      qed
    qed
  qed
  show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL3 gs) ≤ 1"
    using cmdL3_def by simp
qed

definition "tmL2_3 ≡ [cmdL3]"

lemma tmL2_3_tm: "turing_machine (2 * k + 3) G' tmL2_3"
  unfolding tmL2_3_def using G'_ge(1) turing_command_cmdL3 by auto

definition "tmL3 ≡ tmL2 ;; tmL2_3"

lemma tmL3_tm: "turing_machine (2 * k + 3) G' tmL3"
  by (simp add: tmL2_3_tm tmL2_tm tmL3_def)

text ‹
Next the output tape head sweeps left to the beginning of the tape, otherwise
doing nothing.
›

definition "tmL4 ≡ tmL3 ;; tm_left_until1"

lemma tmL4_tm: "turing_machine (2 * k + 3) G' tmL4"
  using tmL3_tm tmL4_def tmL1_def tm_left_until1_tm by simp

text ‹
The next four commands @{term cmdL4}, @{term cmdL5}, @{term cmdL6}, @{term
cmdL7} are parameterized by $jj = 0, \dots, k - 1$. Their job is applying the
write operation and head movement for tape $jj$ of $M$. The entire block of
commands will then be executed $k$ times, once for each $jj$.

The first of these commands sweeps right again and applies the write operation
for tape $jj$, which is memorized on tape $3 + k + jj$. To this end it checks for head flags and
updates the code symbol component $jj$ with the contents of tape $3+k+jj$ when
the head flag for tape $jj$ is set.
›

definition "cmdL5 jj rs ≡
  if rs ! 1 = □
  then (1, zip rs (replicate (2*k+3) Stay))
  else
   (0,
    [(rs ! 0, Stay),
     (if is_code (rs ! 1) ∧ rs ! (3+k+jj) < G ∧ enc_nth (rs ! 1) (k+jj) = 1
      then enc_upd (rs ! 1) jj (rs ! (3+k+jj))
      else rs ! 1,
      Right),
     (rs ! 2, Stay)] @
     (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @
     (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]))"

lemma cmdL5_eq_0:
  assumes "j < 2 * k + 3" and "length gs = 2 * k + 3" and "gs ! 1 = 0"
  shows "cmdL5 jj gs [!] j = (gs ! j, Stay)"
  unfolding cmdL5_def using assms by simp

lemma cmdL5_at_0:
  assumes "gs ! 1 ≠ 0"
  shows "cmdL5 jj gs [!] 0 = (gs ! 0, Stay)"
  unfolding cmdL5_def using assms by simp

lemma cmdL5_at_1:
  assumes "gs ! 1 ≠ 0"
    and "is_code (gs ! 1) ∧ gs ! (3+k+jj) < G ∧ enc_nth (gs!1) (k+jj) = 1"
  shows "cmdL5 jj gs [!] 1 = (enc_upd (gs!1) jj (gs!(3+k+jj)), Right)"
  unfolding cmdL5_def using assms by simp

lemma cmdL5_at_1_else:
  assumes "gs ! 1 ≠ 0"
    and "¬ (is_code (gs ! 1) ∧ gs ! (3+k+jj) < G ∧ enc_nth (gs!1) (k+jj) = 1)"
  shows "cmdL5 jj gs [!] 1 = (gs ! 1, Right)"
  unfolding cmdL5_def using assms by auto

lemma cmdL5_at_2:
  assumes "gs ! 1 ≠ 0"
  shows "cmdL5 jj gs [!] 2 = (gs ! 2, Stay)"
  unfolding cmdL5_def using assms by simp

lemma cmdL5_at_3:
  assumes "gs ! 1 ≠ 0" and "3 ≤ j ∧ j < 3 + k"
  shows "cmdL5 jj gs [!] j = (gs ! j, Stay)"
  unfolding cmdL5_def using assms threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp

lemma cmdL5_at_4:
  assumes "gs ! 1 ≠ 0" and "3 + k ≤ j ∧ j < 2 * k + 3"
  shows "cmdL5 jj gs [!] j = (gs ! j, Stay)"
  unfolding cmdL5_def using assms threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp

lemma turing_command_cmdL5:
  assumes "jj < k"
  shows "turing_command (2 * k + 3) 1 G' (cmdL5 jj)"
proof
  show "length gs = 2 * k + 3 ⟹ length ([!!] cmdL5 jj gs) = length gs" for gs
    unfolding cmdL5_def by (cases "gs!1=0") simp_all
  show goal2: "length gs = 2 * k + 3 ⟹ 0 < 2 * k + 3 ⟹ cmdL5 jj gs [.] 0 = gs ! 0" for gs
    unfolding cmdL5_def by (cases "gs ! 1=0") simp_all
  show "cmdL5 jj gs [.] j < G'"
    if "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'" "j < length gs"
    for gs j
  proof (cases "gs ! 1 = 0")
    case True
    then show ?thesis
      using that cmdL5_eq_0 by simp
  next
    case False
    consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
      using `length gs = 2 * k + 3` `j < length gs` by linarith
    then show ?thesis
    proof (cases)
      case 1
      then show ?thesis
        using that goal2 by simp
    next
      case 2
      show ?thesis
      proof (cases "1 < gs ! 1 ∧ gs ! 1 < G^(2*k+2)+2 ∧ gs ! (3+k+jj) < G ∧ enc_nth (gs ! 1) (k+jj) = 1")
        case True
        then have *: "cmdL5 jj gs [.] j = enc_upd (gs ! 1) jj (gs ! (3+k+jj))"
          using 2 cmdL5_at_1[OF False] by simp
        let ?n = "gs ! 1"
        let ?xs = "dec ?n"
        let ?ys = "(dec ?n) [jj:=gs!(3+k+jj)]"
        have "gs ! (3+k+jj) < G"
          using True by simp
        moreover have "∀h∈set (dec ?n). h < G"
          using True dec_less_G by auto
        ultimately have "∀h∈set ?ys. h < G"
          by (metis in_set_conv_nth length_list_update nth_list_update_eq nth_list_update_neq)
        moreover have "length ?ys = 2 * k + 2"
          using True length_dec by simp
        ultimately have "enc ?ys < G ^ (2 * k + 2) + 2"
          using enc_less by simp
        then show ?thesis
          using * by (simp add: enc_upd_def G'_def)
      next
        case b: False
        then show ?thesis
          using that cmdL5_at_1_else[OF False] 2 by simp
      qed
    next
      case 3
      then show ?thesis
        using that cmdL5_at_2[OF False] by simp
    next
      case 4
      then show ?thesis
        using that cmdL5_at_3[OF False] by simp
    next
      case 5
      then show ?thesis
        using that cmdL5_at_4[OF False] by simp
    qed
  qed
  show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL5 jj gs) ≤ 1"
    using cmdL5_def by (metis (no_types, lifting) One_nat_def fst_conv le_eq_less_or_eq plus_1_eq_Suc trans_le_add2)

qed

definition tmL45 :: "nat ⇒ machine" where
  "tmL45 jj ≡ [cmdL5 jj]"

lemma tmL45_tm:
  assumes "jj < k"
  shows "turing_machine (2 * k + 3) G' (tmL45 jj)"
  using assms G'_ge turing_command_cmdL5 tmL45_def by auto

text ‹
We move the output tape head one cell to the left.
›

definition "tmL46 jj ≡ tmL45 jj ;; tm_left 1"

lemma tmL46_tm:
  assumes "jj < k"
  shows "turing_machine (2 * k + 3) G' (tmL46 jj)"
  using assms G'_ge tm_left_tm tmL45_tm tmL46_def tmL45_def by simp

text ‹
The next command sweeps left and applies the head movement for tape $jj$ if this
is a movement to the left. To this end it checks for a set head flag in
component $k + jj$ of the code symbol and clears it. It also memorizes that it
just cleared the head flag by changing the symbol on memorization tape $3 + jj$
to the number $3$, which is not used to encode any actual head movement. In the
next step of the sweep it will recognize this $3$ and set the head flag in
component $k + jj$ of the code symbol. The net result is that the head flag for
tape $jj$ has moved one cell to the left.
›

abbreviation is_beginning :: "symbol ⇒ bool" where
  "is_beginning y ≡ is_code y ∧ dec y ! (2 * k + 1) = 1"

definition cmdL7 :: "nat ⇒ command" where
  "cmdL7 jj rs ≡
 (if is_beginning (rs ! 1) then 1 else 0,
  if rs ! (3 + jj) = □ ∧ enc_nth (rs ! 1) (k + jj) = 1 ∧ is_code (rs ! 1) ∧ ¬ is_beginning (rs ! 1) then
   [(rs ! 0, Stay),
    (enc_upd (rs ! 1) (k + jj) 0, Left),
    (rs ! 2, Stay)] @
    (map (λj. (if j = jj then 3 else rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k])
  else if rs ! (3 + jj) = 3 ∧ is_code (rs ! 1) then
   [(rs ! 0, Stay),
    (enc_upd (rs ! 1) (k + jj) 1, Left),
    (rs ! 2, Stay)] @
    (map (λj. (if j = jj then 0 else rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k])
  else
   [(rs ! 0, Stay),
    (rs ! 1, Left),
    (rs ! 2, Stay)] @
    (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]))"

abbreviation "condition7a gs jj ≡
  gs ! (3 + jj) = 0 ∧ enc_nth (gs ! 1) (k + jj) = 1 ∧ is_code (gs ! 1) ∧ ¬ is_beginning (gs ! 1)"
abbreviation "condition7b gs jj ≡
  ¬ condition7a gs jj ∧ gs ! (3 + jj) = 3 ∧ is_code (gs ! 1)"
abbreviation "condition7c gs jj ≡
  ¬ condition7a gs jj ∧ ¬ condition7b gs jj"

lemma turing_command_cmdL7:
  assumes "jj < k"
  shows "turing_command (2 * k + 3) 1 G' (cmdL7 jj)"
proof
  show "length ([!!] cmdL7 jj gs) = length gs" if "length gs = 2 * k + 3" for gs
  proof -
    consider "condition7a gs jj" | "condition7b gs jj" | "condition7c gs jj"
      by blast
    then show ?thesis
      unfolding cmdL7_def using that by (cases) simp_all
  qed
  show goal2: "0 < 2 * k + 3 ⟹ cmdL7 jj gs [.] 0 = gs ! 0" if "length gs = 2 * k + 3" for gs
  proof -
    consider "condition7a gs jj" | "condition7b gs jj" | "condition7c gs jj"
      by blast
    then show ?thesis
      unfolding cmdL7_def using that by (cases) simp_all
  qed
  show "cmdL7 jj gs [.] j < G'"
    if gs: "j < length gs" "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'"
    for gs j
  proof -
    consider "condition7a gs jj" | "condition7b gs jj" | "condition7c gs jj"
      by blast
    then show ?thesis
    proof (cases)
      case 1
      then have *: "snd (cmdL7 jj gs) =
        [(gs ! 0, Stay),
         (enc_upd (gs ! 1) (k + jj) 0, Left),
         (gs ! 2, Stay)] @
         (map (λj. (if j = jj then 3 else gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL7_def by simp
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using that by (simp add: goal2)
      next
        case 2
        then have "is_code (gs ! 1)"
          using 1 by blast
        moreover have "k + jj < 2 * k + 2"
          using assms by simp
        moreover have "0 < G"
          using G_ge_4 by simp
        ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 0)"
          using enc_upd_is_code by simp
        then have "is_code (cmdL7 jj gs [.] j)"
          using * 2 by simp
        then show ?thesis
          using G'_ge_G G'_def by simp
      next
        case 3
        then show ?thesis
          using * gs by simp
      next
        case 4
        then show ?thesis
          using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp
      next
        case 5
        then show ?thesis
          using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp
      qed
    next
      case case2: 2
      then have *: "snd (cmdL7 jj gs) =
        [(gs ! 0, Stay),
         (enc_upd (gs ! 1) (k + jj) 1, Left),
         (gs ! 2, Stay)] @
         (map (λj. (if j = jj then 0 else gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL7_def by simp
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using that by (simp add: goal2)
      next
        case 2
        then have "is_code (gs ! 1)"
          using case2 by simp
        moreover have "k + jj < 2 * k + 2"
          using assms by simp
        moreover have "1 < G"
          using G_ge_4 by simp
        ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 1)"
          using enc_upd_is_code by simp
        then have "is_code (cmdL7 jj gs [.] j)"
          using * 2 by simp
        then show ?thesis
          using G'_ge_G G'_def by simp
      next
        case 3
        then show ?thesis
          using * gs by simp
      next
        case 4
        then show ?thesis
          using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp
      next
        case 5
        then show ?thesis
          using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp
      qed
    next
      case case3: 3
      then have *: "snd (cmdL7 jj gs) =
        [(gs ! 0, Stay),
         (gs ! 1, Left),
         (gs ! 2, Stay)] @
         (map (λj. (gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL7_def by auto
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
        using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] threeplus2k_3[where ?a="(gs ! 0, Stay)"]
        by (cases) simp_all
    qed
  qed
  show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL7 jj gs) ≤ 1"
    using cmdL7_def by simp
qed

definition tmL67 :: "nat ⇒ machine" where
  "tmL67 jj ≡ [cmdL7 jj]"

lemma tmL67_tm:
  assumes "jj < k"
  shows "turing_machine (2 * k + 3) G' (tmL67 jj)"
  using assms G'_ge tmL67_def turing_command_cmdL7 by auto

definition "tmL47 jj ≡ tmL46 jj ;; tmL67 jj"

lemma tmL47_tm:
  assumes "jj < k"
  shows "turing_machine (2 * k + 3) G' (tmL47 jj)"
  using assms G'_ge tm_left_tm tmL46_tm tmL47_def tmL67_tm by simp

text ‹
Next we are sweeping right again and perform the head movement for tape $jj$
if this is a movement to the right. This works the same as the left movements
in @{const cmdL7}.
›

definition cmdL8 :: "nat ⇒ command" where
  "cmdL8 jj rs ≡
 (if rs ! 1 = □ then 1 else 0,
  if rs ! (3 + jj) = 2 ∧ enc_nth (rs ! 1) (k + jj) = 1 ∧ is_code (rs ! 1) then
   [(rs ! 0, Stay),
    (enc_upd (rs ! 1) (k + jj) 0, Right),
    (rs ! 2, Stay)] @
    (map (λj. (if j = jj then 3 else rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k])
  else if rs ! (3 + jj) = 3 ∧ is_code (rs ! 1) then
   [(rs ! 0, Stay),
    (enc_upd (rs ! 1) (k + jj) 1, Right),
    (rs ! 2, Stay)] @
    (map (λj. (if j = jj then 2 else rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k])
  else if rs ! 1 = 0 then
   [(rs ! 0, Stay),
    (rs ! 1, Stay),
    (rs ! 2, Stay)] @
    (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k])
  else
   [(rs ! 0, Stay),
    (rs ! 1, Right),
    (rs ! 2, Stay)] @
    (map (λj. (rs ! (j + 3), Stay)) [0..<k]) @
    (map (λj. (rs ! (3 + k + j), Stay)) [0..<k]))"

abbreviation "condition8a gs jj ≡
  gs ! (3 + jj) = 2 ∧ enc_nth (gs ! 1) (k + jj) = 1 ∧ is_code (gs ! 1)"
abbreviation "condition8b gs jj ≡
  ¬ condition8a gs jj ∧ gs ! (3 + jj) = 3 ∧ is_code (gs ! 1)"
abbreviation "condition8c gs jj ≡
  ¬ condition8a gs jj ∧ ¬ condition8b gs jj ∧ gs ! 1 = 0"
abbreviation "condition8d gs jj ≡
  ¬ condition8a gs jj ∧ ¬ condition8b gs jj ∧ ¬ condition8c gs jj"

lemma turing_command_cmdL8:
  assumes "jj < k"
  shows "turing_command (2 * k + 3) 1 G' (cmdL8 jj)"
proof
  show "length ([!!] cmdL8 jj gs) = length gs" if "length gs = 2 * k + 3" for gs
  proof -
    consider "condition8a gs jj" | "condition8b gs jj" | "condition8c gs jj" | "condition8d gs jj"
      by blast
    then show ?thesis
      unfolding cmdL8_def using that by (cases) simp_all
  qed
  show goal2: "0 < 2 * k + 3 ⟹ cmdL8 jj gs [.] 0 = gs ! 0" if "length gs = 2 * k + 3" for gs
  proof -
    consider "condition8a gs jj" | "condition8b gs jj" | "condition8c gs jj" | "condition8d gs jj"
      by blast
    then show ?thesis
      unfolding cmdL8_def using that by (cases) simp_all
  qed
  show "cmdL8 jj gs [.] j < G'"
    if gs: "j < length gs" "length gs = 2 * k + 3" "⋀i. i < length gs ⟹ gs ! i < G'"
    for gs j
  proof -
    consider "condition8a gs jj" | "condition8b gs jj" | "condition8c gs jj" | "condition8d gs jj"
      by blast
    then show ?thesis
    proof (cases)
      case 1
      then have *: "snd (cmdL8 jj gs) =
        [(gs ! 0, Stay),
         (enc_upd (gs ! 1) (k + jj) 0, Right),
         (gs ! 2, Stay)] @
         (map (λj. (if j = jj then 3 else gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL8_def by simp
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using that by (simp add: goal2)
      next
        case 2
        then have "is_code (gs ! 1)"
          using 1 by blast
        moreover have "k + jj < 2 * k + 2"
          using assms by simp
        moreover have "0 < G"
          using G_ge_4 by simp
        ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 0)"
          using enc_upd_is_code by simp
        then have "is_code (cmdL8 jj gs [.] j)"
          using * 2 by simp
        then show ?thesis
          using G'_ge_G G'_def by simp
      next
        case 3
        then show ?thesis
          using * gs by simp
      next
        case 4
        then show ?thesis
          using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp
      next
        case 5
        then show ?thesis
          using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp
      qed
    next
      case case2: 2
      then have *: "snd (cmdL8 jj gs) =
        [(gs ! 0, Stay),
         (enc_upd (gs ! 1) (k + jj) 1, Right),
         (gs ! 2, Stay)] @
         (map (λj. (if j = jj then 2 else gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL8_def by simp
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
      proof (cases)
        case 1
        then show ?thesis
          using that by (simp add: goal2)
      next
        case 2
        then have "is_code (gs ! 1)"
          using case2 by simp
        moreover have "k + jj < 2 * k + 2"
          using assms by simp
        moreover have "1 < G"
          using G_ge_4 by simp
        ultimately have "is_code (enc_upd (gs ! 1) (k + jj) 1)"
          using enc_upd_is_code by simp
        then have "is_code (cmdL8 jj gs [.] j)"
          using * 2 by simp
        then show ?thesis
          using G'_ge_G G'_def by simp
      next
        case 3
        then show ?thesis
          using * gs by simp
      next
        case 4
        then show ?thesis
          using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] by simp
      next
        case 5
        then show ?thesis
          using * gs G'_ge threeplus2k_3[where ?a="(gs ! 0, Stay)"] by simp
      qed
    next
      case 3
      then have *: "snd (cmdL8 jj gs) =
        [(gs ! 0, Stay),
         (gs ! 1, Stay),
         (gs ! 2, Stay)] @
         (map (λj. (gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL8_def by auto
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
        using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] threeplus2k_3[where ?a="(gs ! 0, Stay)"]
        by (cases) simp_all
    next
      case 4
      then have *: "snd (cmdL8 jj gs) =
        [(gs ! 0, Stay),
         (gs ! 1, Right),
         (gs ! 2, Stay)] @
         (map (λj. (gs ! (j + 3), Stay)) [0..<k]) @
         (map (λj. (gs ! (3 + k + j), Stay)) [0..<k])"
        unfolding cmdL8_def by auto
      consider "j = 0" | "j = 1" | "j = 2" | "3 ≤ j ∧ j < k + 3" | "k + 3 ≤ j ∧ j < 2 * k + 3"
        using gs by linarith
      then show ?thesis
        using * gs G'_ge threeplus2k_2[where ?a="(gs ! 0, Stay)"] threeplus2k_3[where ?a="(gs ! 0, Stay)"]
        by (cases) simp_all
    qed
  qed
  show "⋀gs. length gs = 2 * k + 3 ⟹ [*] (cmdL8 jj gs) ≤ 1"
    using cmdL8_def by simp
qed

definition tmL78 :: "nat ⇒ machine" where
  "tmL78 jj ≡ [cmdL8 jj]"

lemma tmL78_tm:
  assumes "jj < k"
  shows "turing_machine (2 * k + 3) G' (tmL78 jj)"
  using assms G'_ge tmL78_def turing_command_cmdL8 by auto

definition "tmL48 jj ≡ tmL47 jj ;; tmL78 jj"

lemma tmL48_tm:
  assumes "jj < k"
  shows "turing_machine (2 * k + 3) G' (tmL48 jj)"
  using assms G'_ge tm_left_tm tmL47_tm tmL48_def tmL78_tm by simp

text ‹
The last command in the command sequence is moving back to the beginning of the
output tape.
›

definition "tmL49 jj ≡ tmL48 jj ;; tm_left_until1"

text ‹
The Turing machine @{term "tmL49 jj"} is then repeated for the parameters $jj =
0, \dots, k - 1$ in order to simulate the actions of $M$ on all tapes.
›

lemma tmL49_tm: "jj < k ⟹ turing_machine (2 * k + 3) G' (tmL49 jj)"
  using tmL48_tm tmL49_def tmL1_def tm_left_until1_tm by simp

fun tmL49_upt :: "nat ⇒ machine" where
  "tmL49_upt 0 = []" |
  "tmL49_upt (Suc j) = tmL49_upt j ;; tmL49 j"

lemma tmL49_upt_tm:
  assumes "j ≤ k"
  shows "turing_machine (2 * k + 3) G' (tmL49_upt j)"
  using assms
proof (induction j)
  case 0
  then show ?case
    using G'_ge(1) turing_machine_def by simp
next
  case (Suc j)
  then