Theory Reduction_TM

chapter ‹Turing machines for reducing $\NP$ languages to \SAT{}\label{s:Red_TM}›

theory Reduction_TM
  imports Sat_TM_CNF Oblivious_2_Tape
begin

text ‹
At long last we are going to create a polynomial-time Turing machine that, for a
fixed language $L\in\NP$, computes for every string $x$ a CNF formula $\Phi$
such that $x\in L$ iff.\ $\Phi$ is satisfiable. This concludes the proof of the
Cook-Levin theorem.

The CNF formula $\Phi$ is a conjunction of formulas $\Phi_0, \dots, \Phi_9$, and
the previous chapter has provided us with Turing machines @{const tm_PHI0},
@{const tm_PHI1}, etc.\ that are supposed to generate these formulas. But only
for $\Phi_9$ has this been proven yet. So our first task is to transfer the
Turing machines @{const tm_PHI0}, $\dots$, @{const tm_PHI8} into the locale
@{locale reduction_sat_x} and show that they really do generate the CNF formulas
$\Phi_0, \dots, \Phi_8$.

The TMs require certain values on their tapes prior to starting. Therefore we
build a Turing machine that computes these values. Then, in a final effort, we
combine all these TMs to create this article's biggest Turing machine.
›


section ‹Turing machines for parts of $\Phi$ revisited›

text ‹
In this section we restate the semantic lemmas @{text "transforms_tm_PHI0"}
etc.\ of the Turing machines @{const tm_PHI0} etc.\ in the context of the locale
@{locale reduction_sat_x}. This means that the lemmas now have terms like @{term
"formula_n Φ⇩₀"} in them instead of more complicated expressions. It also means
that we more clearly see which values the tapes need to contain initially
because they are now expressed in terms of values in the locale, such as $n$,
$p(n)$, or $m'$.

\null
›

context reduction_sat_x
begin

lemma tm_PHI0 [transforms_intros]:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat
  assumes "length tps = k" and "1 < j" and "j + 8 < k"
  assumes
    "tps ! 1 = (⌊[]⌋, 1)"
    "tps ! j = (⌊m'⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊[]⌋, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
    "tps ! (j + 8) = (⌊[]⌋, 1)"
  assumes "tps' = tps
    [j := (⌊Suc (Suc m')⌋⇩_N, 1),
     j + 2 := (⌊0⌋⇩_N, 1),
     j + 6 := (⌊nll_Psi (Suc (Suc m') * H) H 0⌋⇩_N⇩_L⇩_L, 1),
     1 := nlltape (formula_n Φ⇩₀)]"
  assumes "ttt = 5627 * H ^ 4 * (3 + nlength (3 * H + m' * H))⇧²"
  shows "transforms (tm_PHI0 j) tps ttt tps'"
proof -
  have "nll_Psi (m' * H) H 1 = formula_n (Ψ (ζ⇩₀ 0) 1)"
    using nll_Psi zeta0_def m' by simp
  moreover have "nll_Psi (H + m' * H) H 1 = formula_n (Ψ (ζ⇩₁ 0) 1)"
    using nll_Psi zeta1_def m'
    by (smt (verit) ab_semigroup_add_class.add_ac(1) add.commute add_cancel_left_right mult_2 mult_zero_left)
  moreover have "nll_Psi (Suc (Suc m') * H) H 0 = formula_n (Ψ (ζ⇩₂ 0) 0)"
  proof -
    have "Suc (Suc m') * H = N + 2 * H"
      using m' by simp
    moreover have "Suc (Suc m') * H + H = N + (Suc 0) * Z"
      using m' Z_def by simp
    ultimately have "ζ⇩₂ 0 = [Suc (Suc m') * H..<Suc (Suc m') * H + H]"
      using zeta2_def by (metis Nat.add_0_right mult_zero_left)
    then show ?thesis
      using nll_Psi by simp
  qed
  ultimately have "nll_Psi (m' * H) H 1 @ nll_Psi (H + m' * H) H 1 @ nll_Psi (Suc (Suc m') * H) H 0 =
      formula_n Φ⇩₀"
    using formula_n_def PHI0_def by simp
  then show ?thesis
    using transforms_tm_PHI0I[OF assms(1-3) H_ge_3 assms(4-13)] assms(14,15) by simp
qed

lemma tm_PHI1 [transforms_intros]:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 7 < k"
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊0⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊[]⌋, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
  assumes "tps' = tps
    [j + 2 := (⌊1⌋⇩_N, 1),
     j + 6 := (⌊nll_Psi 0 H 1⌋⇩_N⇩_L⇩_L, 1),
     1 := nlltape (nss @ formula_n Φ⇩₁)]"
  assumes "ttt = 1875 * H ^ 4"
  shows "transforms (tm_PHI1 j) tps ttt tps'"
proof -
  have "nll_Psi 0 H 1 = formula_n (Ψ ([0..<H]) 1)"
    using nll_Psi by simp
  then have "nll_Psi 0 H 1 = formula_n (Ψ (γ 0) 1)"
    using gamma_def by simp
  then have "nll_Psi 0 H 1 = formula_n Φ⇩₁"
    using PHI1_def by simp
  then show ?thesis
    using transforms_tm_PHI1I[OF assms(1-3) H_ge_3 assms(4-12)] assms(13,14) by simp
qed

lemma tm_PHI2 [transforms_intros]:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 8 < k"
  assumes "idx = n "
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊idx⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊[]⌋, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
    "tps ! (j + 8) = (⌊[]⌋, 1)"
  assumes "ttt = 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧²"
  assumes "tps' = tps
    [j := (⌊2 * idx + 2⌋⇩_N, 1),
     j + 2 := (⌊3⌋⇩_N, 1),
     j + 6 := (⌊nll_Psi (Suc (Suc (2 * idx)) * H) H 3⌋⇩_N⇩_L⇩_L, 1),
     1 := nlltape (nss @ formula_n Φ⇩₂)]"
  shows "transforms (tm_PHI2 j) tps ttt tps'"
proof -
  have "nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3 = formula_n Φ⇩₂"
  proof -
    have "γ (2 * n + 1) = [H + 2 * idx * H..<H + 2 * idx * H + H]"
      using assms(4) gamma_def by simp
    moreover have "γ (2 * n + 2) = [2 * H + 2 * idx * H..<2 * H + 2 * idx * H + H]"
      using assms(4) gamma_def by simp
    ultimately show "nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3 = formula_n Φ⇩₂"
      using nll_Psi PHI2_def formula_n_def by simp
  qed
  then show ?thesis
    using transforms_tm_PHI2I[OF assms(1-3) H_ge_3 assms(5-14)] assms(15,16) by simp
qed

lemma PHI3_correct: "concat (map (λi. nll_Psi (H * (1 + 2 * i)) H 2) [0..<n]) = formula_n Φ⇩₃"
proof -
  have "nll_Psi (H * (1 + 2 * i)) H 2 = formula_n (Ψ (γ (2*i+1)) 2)" for i
  proof -
    have "γ (2 * i + 1) = [H * (1 + 2 * i)..<H * (1 + 2 * i) + H]"
      using gamma_def by (simp add: mult.commute)
    then show ?thesis
      using nll_Psi by simp
  qed
  then have "concat (map (λi. nll_Psi (H * (1 + 2 * i)) H 2) [0..<n]) =
      concat (map (λi. formula_n (Ψ (γ (2*i+1)) 2)) [0..<n])"
    by simp
  also have "... = formula_n (concat (map (λi. Ψ (γ (2*i+1)) 2) [0..<n]))"
    using concat_formula_n by simp
  also have "... = formula_n Φ⇩₃"
    using PHI3_def by simp
  finally show ?thesis .
qed

lemma tm_PHI3:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 8 < k"
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊1⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊2⌋⇩_N, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
    "tps ! (j + 8) = (⌊1 + 2 * n⌋⇩_N, 1)"
  assumes "ttt = Suc n * (9 + 1897 * (H ^ 4 * (nlength (1 + 2 * n))⇧²))"
  assumes "tps' = tps
    [j := (⌊1 + 2 * n⌋⇩_N, 1),
     1 := nlltape (nss @ formula_n Φ⇩₃),
     j + 3 := (⌊1⌋⇩_N, 1)]"
  shows "transforms (tm_PHI345 2 j) tps ttt tps'"
  using transforms_tm_PHI345I[OF assms(1,2,3) H_ge_3, of 2 2 nss 1 "n "] H_gr_2 assms PHI3_correct
  by fastforce

lemma PHI4_correct:
  assumes "idx = 2 * n + 2 + 1" and "kappa = 2" and "step = 2" and "numiter = p n"
  shows "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) = formula_n Φ⇩₄"
proof -
  have "nll_Psi (H * (idx + step * i)) H kappa = formula_n (Ψ (γ (2 * n + 2 + 2 * i + 1)) 2)" for i
  proof -
    have "γ (2 * n + 2 + 2 * i + 1) = [H * (idx + step * i)..<H * (idx + step * i) + H]"
      using assms gamma_def by (simp add: add.commute mult.commute)
    then show ?thesis
      using nll_Psi assms by simp
  qed
  then have "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) =
      concat (map (λi. formula_n (Ψ (γ (2 * n + 2 + 2 * i + 1)) 2)) [0..<numiter])"
    by simp
  also have "... = formula_n (concat (map (λi. Ψ (γ (2 * n + 2 + 2 * i + 1)) 2) [0..<p n]))"
    using assms concat_formula_n by simp
  also have "... = formula_n Φ⇩₄"
    using PHI4_def by simp
  finally show ?thesis .
qed

lemma tm_PHI4:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt step k :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 8 < k" assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊2 * n + 2 + 1⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊2⌋⇩_N, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
    "tps ! (j + 8) = (⌊2 * n + 2 + 1 + 2 * p n⌋⇩_N, 1)"
  assumes "ttt = Suc (p n) * (9 + 1897 * (H ^ 4 * (nlength (2 * n + 2 + 1 + 2 * p n))⇧²))"
  assumes "tps' = tps
    [j := (⌊2 * n + 2 + 1 + 2 * p n⌋⇩_N, 1),
     1 := nlltape (nss @ formula_n Φ⇩₄),
     j + 3 := (⌊1⌋⇩_N, 1)]"
  shows "transforms (tm_PHI345 2 j) tps ttt tps'"
  using transforms_tm_PHI345I[OF assms(1,2,3) H_ge_3, of 2 2 nss "2 * n + 2 + 1" "p n"] H_gr_2 assms PHI4_correct
  by fastforce

lemma PHI5_correct:
  assumes "idx = 2 * n + 2 * p n + 3" and "kappa = 0" and "step = 1" and "numiter = T' "
  shows "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) = formula_n Φ⇩₅"
proof -
  have "nll_Psi (H * (idx + step * i)) H kappa = formula_n (Ψ (γ (2 * n + 2 * p n + 3 + i)) 0)" for i
  proof -
    have "γ (2 * n + 2 * p n + 3 + i) = [H * (idx + step * i)..<H * (idx + step * i) + H]"
      using assms gamma_def by (simp add: add.commute mult.commute)
    then show ?thesis
      using nll_Psi assms by simp
  qed
  then have "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<numiter]) =
      concat (map (λi. formula_n (Ψ (γ (2 * n + 2 * p n + 3 + i)) 0)) [0..<numiter])"
    by simp
  also have "... = formula_n (concat (map (λi. Ψ (γ (2 * n + 2 * p n + 3 + i)) 0) [0..<T']))"
    using assms concat_formula_n by simp
  also have "... = formula_n Φ⇩₅"
    using PHI5_def by simp
  finally show ?thesis .
qed

lemma tm_PHI5:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 8 < k"
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊2 * n + 2 * p n + 3⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊0⌋⇩_N, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
    "tps ! (j + 8) = (⌊2 * n + 2 * p n + 3 + T'⌋⇩_N, 1)"
  assumes "ttt = Suc T' * (9 + 1891 * (H ^ 4 * (nlength (2 * n + 2 * p n + 3 + T'))⇧²))"
  assumes "tps' = tps
    [j := (⌊2 * n + 2 * p n + 3 + T'⌋⇩_N, 1),
     1 := nlltape (nss @ formula_n Φ⇩₅),
     j + 3 := (⌊1⌋⇩_N, 1)]"
  shows "transforms (tm_PHI345 1 j) tps ttt tps'"
  using transforms_tm_PHI345I[OF assms(1,2,3) H_ge_3, of 0 1, OF _ _ assms(4-12)] H_gr_2 assms(13-) PHI5_correct
  by fastforce

lemma PHI6_correct:
  "concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (xs ! i)) [0..<length xs]) = formula_n Φ⇩₆"
proof -
  have "nll_Psi (H * (2 + 2 * i)) H (xs ! i) = formula_n (Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2))"
    if "i < length xs" for i
  proof -
    have "γ (2 * i + 2) = [H * (2 + 2 * i)..<H * (2 + 2* i) + H]"
      using gamma_def by (simp add: mult.commute)
    then have "nll_Psi (H * (2 + 2 * i)) H (xs ! i) = formula_n (Ψ (γ (2 * i + 2)) (xs ! i))"
      using nll_Psi by simp
    moreover have "xs ! i = (if x ! i then 3 else 2)"
      using that by simp
    ultimately show ?thesis
      by simp
  qed
  then have "map (λi. nll_Psi (H * (2 + 2 * i)) H (xs ! i)) [0..<length xs] =
      map (λi. formula_n (Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2))) [0..<length xs]"
    by simp
  then have "concat (map (λi. nll_Psi (H * (2 + 2 * i)) H (xs ! i)) [0..<length xs]) =
      concat (map (λi. formula_n (Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2))) [0..<length xs])"
    by metis
  also have "... = formula_n (concat (map (λi. Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2)) [0..<length xs]))"
    using concat_formula_n by simp
  also have "... = formula_n (concat (map (λi. Ψ (γ (2 * i + 2)) (if x ! i then 3 else 2)) [0..<n]))"
    by simp
  also have "... = formula_n Φ⇩₆"
    using PHI6_def by simp
  finally show ?thesis .
qed

lemma tm_PHI6 [transforms_intros]:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 7 < k"
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! 0 = (⌊xs⌋, 1)"
    "tps ! j = (⌊2⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊0⌋⇩_N, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
  assumes "tps' = tps
    [0 := (⌊xs⌋, Suc n),
     j := (⌊2 + 2 * n⌋⇩_N, 1),
     1 := nlltape (nss @ formula_n Φ⇩₆)]"
  assumes "ttt = 133650 * H ^ 6 * n ^ 3 + 1"
  shows "transforms (tm_PHI6 j) tps ttt tps'"
  using transforms_tm_PHI6I[OF assms(1,2,3) H_ge_3 bs_xs assms(4-13) _] assms(14,15) PHI6_correct
  by simp

lemma PHI7_correct:
  assumes "idx = 2 * n + 4" and "numiter = p n"
  shows "concat (map (λi. nll_Upsilon (idx + 2 * i) H) [0..<numiter]) = formula_n Φ⇩₇"
proof -
  have "nll_Upsilon (idx + 2 * i) H = formula_n (Υ (γ (2*n + 4 + 2 * i)))" for i
  proof -
    have "nll_Upsilon (idx + 2 * i) H = formula_n (Υ [(idx + 2 * i)*H..<(idx + 2 * i)*H+H])"
      using nll_Upsilon[OF H_ge_3] by simp
    also have "... = formula_n (Υ (γ (2 * n + 4 + 2 * i)))"
      using gamma_def assms(1) by (simp add: add.commute)
    finally show ?thesis .
  qed
  then have "concat (map (λi. nll_Upsilon (idx + 2 * i) H) [0..<numiter]) =
      concat (map (λi. formula_n (Υ (γ (2*n + 4 + 2 * i)))) [0..<numiter])"
    by simp
  also have "... = formula_n (concat (map (λi. Υ (γ (2*n + 4 + 2 * i))) [0..<numiter]))"
    using concat_formula_n by simp
  also have "... = formula_n (concat (map (λi. Υ (γ (2*n + 4 + 2 * i))) [0..<p n]))"
    using assms(2) by simp
  also have "... = formula_n Φ⇩₇"
    using PHI7_def by simp
  finally show ?thesis .
qed

lemma tm_PHI7 [transforms_intros]:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt numiter k idx :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 6 < k"
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊2 * n + 4⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊[]⌋, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊p n⌋⇩_N, 1)"
  assumes "ttt = p n * 257 * H * (nlength (2 * n + 4 + 2 * p n) + nlength H)⇧² + 1"
  assumes "tps' = tps
    [j := (⌊2 * n + 4 + 2 * p n⌋⇩_N, 1),
     j + 6 := (⌊0⌋⇩_N, 1),
     1 := nlltape (nss @ formula_n Φ⇩₇)]"
  shows "transforms (tm_PHI7 j) tps ttt tps'"
  using transforms_tm_PHI7I[OF assms(1,2,3) H_ge_3 assms(4-12)] assms(13) PHI7_correct
  by simp

lemma tm_PHI8 [transforms_intros]:
  fixes tps tps' :: "tape list" and j :: tapeidx and ttt k idx :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 7 < k"
  assumes "idx = 1 + 3 * T' + m' "
  assumes
    "tps ! 1 = nlltape nss"
    "tps ! j = (⌊1 + 3 * T' + m'⌋⇩_N, 1)"
    "tps ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps ! (j + 2) = (⌊[]⌋, 1)"
    "tps ! (j + 3) = (⌊[]⌋, 1)"
    "tps ! (j + 4) = (⌊[]⌋, 1)"
    "tps ! (j + 5) = (⌊[]⌋, 1)"
    "tps ! (j + 6) = (⌊[]⌋, 1)"
    "tps ! (j + 7) = (⌊[]⌋, 1)"
  assumes "tps' = tps
      [1 := nlltape (nss @ formula_n Φ⇩₈),
       j + 2 := (⌊3⌋⇩_N, 1),
       j + 6 := (⌊formula_n Φ⇩₈⌋⇩_N⇩_L⇩_L, 1)]"
  assumes "ttt = 18 + 1861 * H ^ 4 * (nlength (Suc (1 + 3 * T' + m')))⇧²"
  shows "transforms (tm_PHI8 j) tps ttt tps'"
proof -
  let ?idx = "1 + 3 * T' + m' "
  have "m' * H + T' * 3 * H + H = ?idx * H"
    using m' add_mult_distrib by simp
  then have "ζ⇩₁ T' = [?idx * H..<?idx * H + H]"
    using zeta1_def Z_def m' by (metis ab_semigroup_add_class.add_ac(1) mult.assoc mult_2)
  then have "nll_Psi (?idx * H) H 3 = formula_n Φ⇩₈"
    using PHI8_def nll_Psi by simp
  then show ?thesis
    using transforms_tm_PHI8I[OF assms(1-3) H_ge_3 assms(5-13) _ assms(15)] assms(14) by simp
qed

end  (* context reduction_sat_x *)


section ‹A Turing machine for initialization›

text ‹
As we have seen in the previous section, the Turing machines @{const tm_PHI0}
etc.\ expect some tapes to contain certain values that depend on the verifier TM
$M$. In this section we construct the TM @{term tm_PHI_init} that computes
theses values.

The TM expects the string $x$ on the input tape. Then it determines the length
$n$ of $x$ and stores it on tape~11. Then it computes the value $p(n)$ and
stores it on tape~15. Then it computes $m = 2n + 2p(n) + 2$ and stores it on
tape~16. It then writes $\mathbf{0}^m$ to tape~9 and runs @{const
tm_list_headpos}, which writes the sequences of head positions for the input and
work/output tape of the verifier TM $M$ to tapes~4 and~7, respectively.  The
length of these lists determines $T'$, which is written to tape~17. From this
and $m$ the TM computes $m'$ and writes it to tape~18. It then writes $H$, which
is hard-coded, to tape~19 and finally $N = H\cdot m'$ to tape~20.

We assume that the TM starts in a configuration where the input tape head and
the heads on tapes with index greater than 10 are positioned on cell number~1,
whereas all other tapes are on cell number~0 as usual.
The TM has no tape parameters, as all tapes are fixed to work with the final TM
later.

As with other TMs before, we will define and analyze the TM on the theory level
and then transfer the semantics to the locale @{locale reduction_sat_x}.
›

definition tm_PHI_init :: "nat ⇒ machine ⇒ (nat ⇒ nat) ⇒ machine" where
  "tm_PHI_init G M p ≡
     tm_right 9 ;;
     tm_length_input 11 ;;
     tm_polynomial p 11 ;;
     tm_copyn 15 16 ;;
     tm_add 11 16 ;;
     tm_incr 16 ;;
     tm_times2 16 ;;
     tm_copyn 16 17 ;;
     tm_write_replicate 2 17 9 ;;
     tm_left 9 ;;
     tm_list_headpos G M 2 ;;
     tm_count 4 17 4 ;;
     tm_decr 17 ;;
     tm_copyn 16 18 ;;
     tm_incr 18 ;;
     tm_add 17 18 ;;
     tm_setn 19 (max G (length M)) ;;
     tm_mult 18 19 20"

lemma tm_PHI_init_tm:
  fixes H k
  assumes "turing_machine 2 G M" and "k > 20" and "H ≥ Suc (length M)" and "H ≥ G"
  assumes "H ≥ 5"
  shows "turing_machine k H (tm_PHI_init G M p)"
  unfolding tm_PHI_init_def
  using assms turing_machine_sequential_turing_machine tm_right_tm tm_length_input_tm tm_polynomial_tm
    tm_copyn_tm tm_add_tm tm_incr_tm tm_times2_tm tm_write_replicate_tm tm_left_tm tm_list_headpos_tm
    tm_count_tm tm_decr_tm tm_setn_tm tm_mult_tm
  by simp

locale turing_machine_PHI_init =
  fixes G :: nat and M :: machine and p :: "nat ⇒ nat"
begin

definition "tm3 ≡ tm_right 9"
definition "tm4 ≡ tm3 ;; tm_length_input 11"
definition "tm5 ≡ tm4 ;; tm_polynomial p 11"
definition "tm6 ≡ tm5 ;; tm_copyn 15 16"
definition "tm7 ≡ tm6 ;; tm_add 11 16"
definition "tm8 ≡ tm7 ;; tm_incr 16"
definition "tm9 ≡ tm8 ;; tm_times2 16"
definition "tm10 ≡ tm9 ;; tm_copyn 16 17"
definition "tm11 ≡ tm10 ;; tm_write_replicate 2 17 9"
definition "tm12 ≡ tm11 ;; tm_left 9"
definition "tm13 ≡ tm12 ;; tm_list_headpos G M 2"
definition "tm14 ≡ tm13 ;; tm_count 4 17 4"
definition "tm15 ≡ tm14 ;; tm_decr 17"
definition "tm16 ≡ tm15 ;; tm_copyn 16 18"
definition "tm17 ≡ tm16 ;; tm_incr 18"
definition "tm18 ≡ tm17 ;; tm_add 17 18"
definition "tm19 ≡ tm18 ;; tm_setn 19 (max G (length M))"
definition "tm20 ≡ tm19 ;; tm_mult 18 19 20"

lemma tm20_eq_tm_PHI_init: "tm20 = tm_PHI_init G M p"
  unfolding tm20_def tm19_def tm18_def tm17_def tm16_def tm15_def tm14_def tm13_def tm12_def tm11_def
  unfolding tm10_def tm9_def tm8_def tm7_def tm6_def tm5_def tm4_def tm3_def tm_PHI_init_def
  by simp

context
  fixes k H thalt :: nat and tps0 :: "tape list" and xs zs :: "symbol list"
  assumes poly_p: "polynomial p"
    and M_tm: "turing_machine 2 G M"
    and k: "k = length tps0" "20 < k"
    and H: "H = max G (length M)"
    and xs: "bit_symbols xs"
    and zs: "zs = 2 # 2 # replicate (2 * length xs + 2 * p (length xs)) 2"
  assumes thalt:
    "∀t<thalt. fst (execute M (start_config 2 zs) t) < length M"
    "fst (execute M (start_config 2 zs) thalt) = length M"
  assumes tps0:
    "tps0 ! 0 = (⌊xs⌋, 1)"
    "⋀i. 0 < i ⟹ i ≤ 10 ⟹ tps0 ! i = (⌊[]⌋, 0)"
    "⋀i. 10 < i ⟹ i < k ⟹ tps0 ! i = (⌊[]⌋, 1)"
begin

lemma G: "G ≥ 4"
  using M_tm turing_machine_def by simp

lemma H: "H ≥ length M" "H ≥ G"
  using H by simp_all

definition "tps3 ≡ tps0
  [9 := (⌊[]⌋, 1)]"

lemma tm3 [transforms_intros]: "transforms tm3 tps0 1 tps3"
  unfolding tm3_def by (tform tps: tps3_def tps0 k)

abbreviation "n ≡ length xs"

definition "tps4 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1)]"

lemma tm4 [transforms_intros]:
  assumes "ttt = 5 + 11 * (length xs)⇧²"
  shows "transforms tm4 tps0 ttt tps4"
  unfolding tm4_def
proof (tform tps: tps3_def tps4_def tps0 k time: assms)
  show "proper_symbols xs"
    using xs by auto
  show "tps3 ! 11 = (⌊0⌋⇩_N, 1)"
    using canrepr_0 tps3_def tps0 k by simp
qed

definition "tps5 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1)]"

lemma tm5 [transforms_intros]:
  assumes "ttt = 5 + 11 * (length xs)⇧² + (d_polynomial p + d_polynomial p * (nlength (length xs))⇧²)"
  shows "transforms tm5 tps0 ttt tps5"
  unfolding tm5_def by (tform tps: canrepr_0 tps4_def tps5_def tps0 k poly_p time: assms)

definition "tps6 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊p n⌋⇩_N, 1)]"

lemma tm6 [transforms_intros]:
  assumes "ttt = 19 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) + 3 * nlength (p n)"
  shows "transforms tm6 tps0 ttt tps6"
  unfolding tm6_def
proof (tform tps: tps5_def tps6_def tps0 k)
  show "tps5 ! 16 = (⌊0⌋⇩_N, 1)"
    using canrepr_0 k tps0 tps5_def by simp
  show "ttt = 5 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
      (14 + 3 * (nlength (p n) + nlength 0))"
    using assms by simp
qed

definition "tps7 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊n + p n⌋⇩_N, 1)]"

lemma tm7 [transforms_intros]:
  assumes "ttt = 29 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n))"
  shows "transforms tm7 tps0 ttt tps7"
  unfolding tm7_def by (tform tps: tps6_def tps7_def tps0 k assms)

definition "tps8 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊Suc (n + p n)⌋⇩_N, 1)]"

lemma tm8 [transforms_intros]:
  assumes "ttt = 34 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n)"
  shows "transforms tm8 tps0 ttt tps8"
  unfolding tm8_def by (tform tps: tps7_def tps8_def tps0 k assms)

definition "tps9 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1)]"

lemma tm9 [transforms_intros]:
  assumes "ttt = 39 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n))"
  shows "transforms tm9 tps0 ttt tps9"
  unfolding tm9_def by (tform tps: tps8_def tps9_def tps0 k assms)

definition "tps10 ≡ tps0
  [9 := (⌊[]⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊2 * Suc (n + p n)⌋⇩_N, 1)]"

lemma tm10 [transforms_intros]:
  assumes "ttt = 53 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 3 * nlength (Suc (Suc (2 * n + 2 * p n)))"
  shows "transforms tm10 tps0 ttt tps10"
  unfolding tm10_def
proof (tform tps: tps9_def tps10_def tps0 k)
  show "tps9 ! 17 = (⌊0⌋⇩_N, 1)"
    using tps9_def canrepr_0 tps0 k by simp
  show "ttt = 39 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
      3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) +
      2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) +
      (14 + 3 * (nlength (Suc (Suc (2 * n + 2 * p n))) + nlength 0))"
    using assms by simp
qed

definition "tps11 ≡ tps0
  [9 := (⌊zs⌋, 1),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊0⌋⇩_N, 1)]"

lemma tm11 [transforms_intros]:
  assumes "ttt = 57 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 3 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    Suc (Suc (2 * n + 2 * p n)) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n))))"
  shows "transforms tm11 tps0 ttt tps11"
  unfolding tm11_def
proof (tform tps: tps10_def tps11_def tps0 k time: assms)
  show "tps11 = tps10
    [17 := (⌊0⌋⇩_N, 1),
     9 := (⌊replicate (Suc (Suc (2 * n + 2 * p n))) 2⌋, 1)]"
    unfolding tps11_def tps10_def using zs by (simp add: list_update_swap[of _ 9])
qed

definition "tps12 ≡ tps0
  [9 := (⌊zs⌋, 0),
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊0⌋⇩_N, 1)]"

lemma tm12 [transforms_intros]:
  assumes "ttt = 82 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n))))"
  shows "transforms tm12 tps0 ttt tps12"
  unfolding tm12_def
proof (tform tps: tps11_def tps12_def tps0 k time: assms)
  have "tps11 ! 9 |-| 1 = (⌊zs⌋, 0)"
    using tps11_def k by simp
  then show "tps12 = tps11[9 := tps11 ! 9 |-| 1]"
    unfolding tps12_def tps11_def by (simp add: list_update_swap[of _ 9])
qed

abbreviation exc :: "nat ⇒ config" where
  "exc t ≡ execute M (start_config 2 zs) t"

definition "tps13 ≡ tps0
  [9 := exc thalt <!> 0,
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊0⌋⇩_N, 1),
   3 := (⌊exc thalt <#> 0⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   6 := (⌊exc thalt <#> 1⌋⇩_N, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   10 := exc thalt <!> 1]"

lemma tm13 [transforms_intros]:
  assumes "ttt = 82 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt)"
  shows "transforms tm13 tps0 ttt tps13"
  unfolding tm13_def
proof (tform)
  show "turing_machine 2 G M"
    using M_tm .
  show "2 + 9 ≤ length tps12"
    using tps12_def k by simp
  show "∀t<thalt. fst (execute M (start_config 2 zs) t) < length M"
      "fst (execute M (start_config 2 zs) thalt) = length M"
    using thalt .
  show "symbols_lt G zs"
  proof -
    have "zs = replicate (2 * n + 2 * p n + 2) 2"
      using zs by simp
    then have "∀i<length zs. zs ! i = 2"
      using nth_replicate by (metis length_replicate)
    then show ?thesis
      using G by simp
  qed
  show "tps13 = tps12
    [2 + 1 := (⌊snd (exc thalt) :#: 0⌋⇩_N, 1),
     2 + 2 := (⌊map (λt. snd (exc t) :#: 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
     2 + 4 := (⌊snd (exc thalt) :#: 1⌋⇩_N, 1),
     2 + 5 := (⌊map (λt. snd (exc t) :#: 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
     2 + 7 := exc thalt <!> 0, 2 + 8 := exc thalt <!> 1]"
    unfolding tps13_def tps12_def by (simp add: list_update_swap[of _ 9])
  show "tps12 ! 2 = ⌈▹⌉"
    using tps12_def tps0 onesie_1 by simp
  show "tps12 ! (2 + 1) = (⌊0⌋⇩_N, 0)"
    using tps12_def tps0 canrepr_0 by simp
  show "tps12 ! (2 + 2) = (⌊[]⌋⇩_N⇩_L, 0)"
    using tps12_def tps0 nlcontents_Nil by simp
  show "tps12 ! (2 + 3) = ⌈▹⌉"
    using tps12_def tps0 onesie_1 by simp
  show "tps12 ! (2 + 4) = (⌊0⌋⇩_N, 0)"
    using tps12_def tps0 canrepr_0 by simp
  show "tps12 ! (2 + 5) = (⌊[]⌋⇩_N⇩_L, 0)"
    using tps12_def tps0 nlcontents_Nil by simp
  show "tps12 ! (2 + 6) = ⌈▹⌉"
    using tps12_def tps0 onesie_1 by simp
  show "tps12 ! (2 + 7) = (⌊zs⌋, 0)"
    using tps12_def k tps0 by simp
  show "tps12 ! (2 + 8) = (⌊[]⌋, 0)"
    using tps12_def tps0 by simp
  show "ttt = 82 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
      3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
      2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
      (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
      27 * Suc thalt * (9 + 2 * nlength thalt)"
    using assms by simp
qed

definition "tpsA ≡ tps0
  [9 := exc thalt <!> 0,
   3 := (⌊exc thalt <#> 0⌋⇩_N, 1),
   6 := (⌊exc thalt <#> 1⌋⇩_N, 1),
   10 := exc thalt <!> 1]"

definition "tps14 ≡ tps0
  [9 := exc thalt <!> 0,
   11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊Suc thalt⌋⇩_N, 1),
   3 := (⌊exc thalt <#> 0⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   6 := (⌊exc thalt <#> 1⌋⇩_N, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   10 := exc thalt <!> 1]"

lemma tm14:
  assumes "ttt = 87 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧²"
  shows "transforms tm14 tps0 ttt tps14"
  unfolding tm14_def
proof (tform)
  show "4 < length tps13" "17 < length tps13"
    using tps13_def k by (simp_all only: length_list_update)
  show "tps13 ! 4 = (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1)"
    using tps13_def k by (simp only: length_list_update nth_list_update_neq nth_list_update_eq)
  show "tps13 ! 17 = (⌊0⌋⇩_N, 1)"
    using tps13_def k by (simp only: length_list_update nth_list_update_neq nth_list_update_eq)
  show "tps14 = tps13
      [17 := (⌊length (map (λt. snd (exc t) :#: 0) [0..<Suc thalt])⌋⇩_N, 1)]"
    unfolding tps14_def tps13_def by (simp add: list_update_swap[of 17])
  show "ttt = 82 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
      3 * nlength (p n) +
      3 * max (nlength n) (nlength (p n)) +
      2 * nlength (n + p n) +
      2 * nlength (Suc (n + p n)) +
      7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
      (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
      (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
      (14 * (nllength (map (λt. snd (exc t) :#: 0) [0..<Suc thalt]))⇧² + 5)"
    using assms by simp
qed

definition "tps14' ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊Suc thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1)]"

lemma tps14': "tps14' = tps14"
  unfolding tps14'_def tps14_def tpsA_def by (simp add: list_update_swap)

lemma len_tpsA: "length tpsA = k"
  using tpsA_def k by simp

lemma tm14' [transforms_intros]:
  assumes "ttt = 87 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧²"
  shows "transforms tm14 tps0 ttt tps14'"
  using tm14 tps14' assms by simp

definition "tps15 ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1)]"

lemma tm15 [transforms_intros]:
  assumes "ttt = 95 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧² +
    2 * nlength (Suc thalt)"
  shows "transforms tm15 tps0 ttt tps15"
  unfolding tm15_def
proof (tform tps: tps14'_def len_tpsA k time: assms)
  show "tps15 = tps14'[17 := (⌊Suc thalt - 1⌋⇩_N, 1)]"
    unfolding tps15_def tps14'_def by (simp add: list_update_swap)
qed

definition "tps16 ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   18 := (⌊2 * Suc (n + p n)⌋⇩_N, 1)]"

lemma tm16 [transforms_intros]:
  assumes "ttt = 109 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧² +
    2 * nlength (Suc thalt)"
  shows "transforms tm16 tps0 ttt tps16"
  unfolding tm16_def
proof (tform tps: tps15_def tps16_def k len_tpsA)
  have "tps15 ! 18 = tpsA ! 18"
    using tps15_def by simp
  also have "... = tps0 ! 18"
    using tpsA_def by simp
  also have "... = (⌊0⌋⇩_N, 1)"
    using tps0 canrepr_0 k by simp
  finally show "tps15 ! 18 = (⌊0⌋⇩_N, 1)" .
  show "ttt = 95 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
      3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) +
      2 * nlength (n + p n) + 2 * nlength (Suc (n + p n)) +
      7 * nlength (Suc (Suc (2 * n + 2 * p n))) +
      (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) + (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
      14 * (nllength
        (map (λt. snd (exc t) :#: 0) [0..<thalt] @ [snd (exc thalt) :#: 0]))⇧² +
      2 * nlength (Suc thalt) + (14 + 3 * (nlength (Suc (Suc (2 * n + 2 * p n))) + nlength 0))"
    using assms by simp
qed

definition "tps17 ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   18 := (⌊Suc (2 * Suc (n + p n))⌋⇩_N, 1)]"

lemma tm17 [transforms_intros]:
  assumes "ttt = 114 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧² +
    2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))"
  shows "transforms tm17 tps0 ttt tps17"
  unfolding tm17_def by (tform tps: tps16_def tps17_def k len_tpsA time: assms)

definition "tps18 ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   18 := (⌊thalt + Suc (2 * Suc (n + p n))⌋⇩_N, 1)]"

lemma tm18 [transforms_intros]:
  assumes "ttt = 124 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧² +
    2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    3 * max (nlength thalt) (nlength (Suc (Suc (Suc (2 * n + 2 * p n)))))"
  shows "transforms tm18 tps0 ttt tps18"
  unfolding tm18_def by (tform tps: tps17_def tps18_def k len_tpsA time: assms)

definition "tps19 ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   18 := (⌊thalt + Suc (2 * Suc (n + p n))⌋⇩_N, 1),
   19 := (⌊max G (length M)⌋⇩_N, 1)]"

lemma tm19 [transforms_intros]:
  assumes "ttt = 134 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧² +
    2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    3 * max (nlength thalt) (nlength (Suc (Suc (Suc (2 * n + 2 * p n))))) +
    2 * nlength (max G (length M))"
  shows "transforms tm19 tps0 ttt tps19"
  unfolding tm19_def
proof (tform tps: assms nlength_0)
  have "tps18 ! 19 = tpsA ! 19"
    using tps18_def by simp
  also have "... = tps0 ! 19"
    using tpsA_def by simp
  also have "... = (⌊0⌋⇩_N, 1)"
    using tps0 canrepr_0 k by simp
  finally show "tps18 ! 19 = (⌊0⌋⇩_N, 1)" .
  show "19 < length tps18"
    using tps18_def len_tpsA k by simp
  show "tps19 = tps18[19 := (⌊max G (length M)⌋⇩_N, 1)]"
    using tps19_def tps18_def len_tpsA k by presburger
qed

definition "tps20 ≡ tpsA
  [11 := (⌊n⌋⇩_N, 1),
   15 := (⌊p n⌋⇩_N, 1),
   16 := (⌊2 * Suc (n + p n)⌋⇩_N, 1),
   17 := (⌊thalt⌋⇩_N, 1),
   4 := (⌊map (λt. exc t <#> 0) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   7 := (⌊map (λt. exc t <#> 1) [0..<Suc thalt]⌋⇩_N⇩_L, 1),
   18 := (⌊thalt + Suc (2 * Suc (n + p n))⌋⇩_N, 1),
   19 := (⌊max G (length M)⌋⇩_N, 1),
   20 := (⌊(thalt + Suc (2 * Suc (n + p n))) * max G (length M)⌋⇩_N, 1)]"

lemma tm20:
  assumes "ttt = 138 + 11 * n⇧² + (d_polynomial p + d_polynomial p * (nlength n)⇧²) +
    3 * nlength (p n) + 3 * max (nlength n) (nlength (p n)) + 2 * nlength (n + p n) +
    2 * nlength (Suc (n + p n)) + 10 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    (2 * n + 2 * p n) * (12 + 2 * nlength (Suc (Suc (2 * n + 2 * p n)))) +
    (27 + 27 * thalt) * (9 + 2 * nlength thalt) +
    14 * (nllength (map (λt. exc t <#> 0) [0..<thalt] @ [exc thalt <#> 0]))⇧² +
    2 * nlength (Suc thalt) + 2 * nlength (Suc (Suc (2 * n + 2 * p n))) +
    3 * max (nlength thalt) (nlength (Suc (Suc (Suc (2 * n + 2 * p n))))) +
    2 * nlength (max G (length M)) +
    26 * (nlength (Suc (Suc (Suc (thalt + (2 * n + 2 * p n))))) + nlength (max G (length M))) *
     (nlength (Suc (Suc (Suc (thalt + (2 * n + 2 * p n))))) + nlength (max G (length M)))"
  shows "transforms tm20 tps0 ttt tps20"
  unfolding tm20_def
proof (tform time: assms)
  have "tps19 ! 20 = tpsA ! 20"
    using tps19_def by simp
  also have "... = tps0 ! 20"
    using tpsA_def by simp
  also have "... = (⌊0⌋⇩_N, 1)"
    using tps0 canrepr_0 k by simp
  finally show "tps19 ! 20 = (⌊0⌋⇩_N, 1)" .
  show "tps20 = tps19
      [20 := (⌊Suc (Suc (Suc (thalt + (2 * n + 2 * p n)))) * max G (length M)⌋⇩_N, 1)]"
    unfolding tps20_def tps19_def by (simp add: list_update_swap)
  show "18 < length tps19" "19 < length tps19" "20 < length tps19"
    using tps19_def k len_tpsA by (simp_all only: length_list_update)
  have "tps19 ! 18 = (⌊thalt + Suc (2 * Suc