Theory Sat_TM_CNF

section ‹Turing machines for the parts of $\Phi$\label{s:tmcnf}›

theory Sat_TM_CNF
  imports Aux_TM_Reducing
begin

text ‹
In this section we build Turing machines for all parts $\Phi_0,\dots,\Phi_9$ of
the CNF formula $\Phi$. Some of them ($\Phi_0$, $\Phi_1$, $\Phi_2$, and
$\Phi_8$) are just fixed-length sequences of $\Psi$ formulas constructible by
fixed-length sequences of @{const tm_Psigamma} machines.  Others ($\Phi_3$,
$\Phi_4$, $\Phi_5$, $\Phi_6$) are variable-length and require looping over a
@{const tm_Psigamma} machine. The TM for $\Phi_7$ is a loop over @{const
tm_Upsilongamma}. Lastly, the TM for $\Phi_9$ is a loop over a TM that generates
the formulas $\chi_t$.

Ideally we would want to prove the semantics of the TMs inside the locale
@{locale reduction_sat}, in which $\Phi$ was defined. However, we use locales to
prove the semantics of TMs, and locales cannot be nested. For this reason we
have to define the TMs on the theory level and prove their semantics there, too,
just as we have done with all TMs until now. In the next chapter the semantics
lemmas will be transferred to the locale @{locale reduction_sat}.

Unlike most TMs so far, the TMs in this section are not meant to be reusable
but serve a special purpose, namely to be combined into one large TM computing
$\Phi$. For this reason the TMs are somewhat peculiar. For example, they write
their output to the fixed tape~$1$ rather than having a parameter for the output
tape. They also often expect the tapes to be initialized in a very special way.
Moreover, the TMs often leave the work tapes in a ``dirty'' state with remnants
of intermediate calculations. The combined TM for all of $\Phi$ will simply
allocate a new batch of work tapes for every individual TM.
›


subsection ‹A Turing machine for $\Phi_0$›

text ‹
The next Turing machine expects a number $i$ on tape $j$ and a number $H$ on
tape $j + 1$ and outputs to tape $1$ the formula $\Psi([i\dots H, (i+1)\dots H),
1) \land \Psi([(i+1)\dots H, (i+2)\dots H), 1) \land \Psi([(i+2)\dots H,
(i+3)\dots H), 0)$, which is just $\Phi_0$ for suitable values of $i$ and $H$.
›

definition tm_PHI0 :: "tapeidx ⇒ machine" where
  "tm_PHI0 j ≡
    tm_setn (j + 2) 1 ;;
    tm_Psigamma j ;;
    tm_extendl_erase 1 (j + 6) ;;
    tm_incr j ;;
    tm_Psigamma j ;;
    tm_extendl_erase 1 (j + 6) ;;
    tm_incr j ;;
    tm_setn (j + 2) 0 ;;
    tm_Psigamma j ;;
    tm_extendl 1 (j + 6)"

lemma tm_PHI0_tm:
  assumes "0 < j" and "j + 8 < k" and "G ≥ 6"
  shows "turing_machine k G (tm_PHI0 j)"
  unfolding tm_PHI0_def
  using assms tm_Psigamma_tm tm_extendl_tm tm_erase_cr_tm tm_times2_tm tm_incr_tm tm_setn_tm tm_cr_tm
    tm_extendl_erase_tm
  by simp

locale turing_machine_PHI0 =
  fixes j :: tapeidx
begin

definition "tm1 ≡ tm_setn (j + 2) 1"
definition "tm2 ≡ tm1 ;; tm_Psigamma j"
definition "tm3 ≡ tm2 ;; tm_extendl_erase 1 (j + 6)"
definition "tm5 ≡ tm3 ;; tm_incr j"
definition "tm6 ≡ tm5 ;; tm_Psigamma j"
definition "tm7 ≡ tm6 ;; tm_extendl_erase 1 (j + 6)"
definition "tm9 ≡ tm7 ;; tm_incr j"
definition "tm10 ≡ tm9 ;; tm_setn (j + 2) 0"
definition "tm11 ≡ tm10 ;; tm_Psigamma j"
definition "tm12 ≡ tm11 ;; tm_extendl 1 (j + 6)"

lemma tm12_eq_tm_PHI0: "tm12 = tm_PHI0 j"
  using tm12_def tm11_def tm10_def tm9_def tm7_def tm6_def tm5_def
  using tm3_def tm2_def tm1_def tm_PHI0_def
  by simp

context
  fixes tps0 :: "tape list" and k idx H :: nat
  assumes jk: "length tps0 = k" "1 < j" "j + 8 < k"
    and H: "H ≥ 3"
  assumes tps0:
    "tps0 ! 1 = (⌊[]⌋, 1)"
    "tps0 ! j = (⌊idx⌋⇩_N, 1)"
    "tps0 ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps0 ! (j + 2) = (⌊[]⌋, 1)"
    "tps0 ! (j + 3) = (⌊[]⌋, 1)"
    "tps0 ! (j + 4) = (⌊[]⌋, 1)"
    "tps0 ! (j + 5) = (⌊[]⌋, 1)"
    "tps0 ! (j + 6) = (⌊[]⌋, 1)"
    "tps0 ! (j + 7) = (⌊[]⌋, 1)"
    "tps0 ! (j + 8) = (⌊[]⌋, 1)"
begin

definition "tps1 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1)]"

lemma tm1 [transforms_intros]:
  assumes "ttt = 12"
  shows "transforms tm1 tps0 ttt tps1"
  unfolding tm1_def
proof (tform tps: tps0 tps1_def jk)
  show "tps0 ! (j + 2) = (⌊0⌋⇩_N, 1)"
    using tps0 jk canrepr_0 by simp
  show "ttt = 10 + 2 * nlength 0 + 2 * nlength 1"
    using assms canrepr_1 by simp
qed

definition "tps2 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi (idx * H) H 1⌋⇩_N⇩_L⇩_L, 1)]"

lemma tm2 [transforms_intros]:
  assumes "ttt = 12 + 1851 * H ^ 4 * (nlength (Suc idx))⇧²"
  shows "transforms tm2 tps0 ttt tps2"
  unfolding tm2_def by (tform tps: assms tps0 H tps1_def tps2_def jk)

definition "tps3 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1),
   1 := nlltape (nll_Psi (idx * H) H (Suc 0)),
   j + 6 := (⌊[]⌋, 1)]"

lemma tm3 [transforms_intros]:
  assumes "ttt = 23 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H (Suc 0))"
  shows "transforms tm3 tps0 ttt tps3"
  unfolding tm3_def
proof (tform tps: tps0 H tps2_def tps3_def jk time: assms)
  show "tps2 ! 1 = nlltape []"
    using tps2_def jk nllcontents_Nil tps0 by simp
  show "tps3 = tps2
      [1 := nlltape ([] @ nll_Psi (idx * H) H (Suc 0)),
       j + 6 := (⌊[]⌋, 1)]"
    unfolding tps3_def tps2_def using jk by (simp add: list_update_swap)
qed

definition "tps5 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1),
   1 := nlltape (nll_Psi (idx * H) H (Suc 0)),
   j + 6 := (⌊[]⌋, 1),
   j := (⌊Suc idx⌋⇩_N, 1)]"

lemma tm5 [transforms_intros]:
  assumes "ttt = 28 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) +
      2 * nlength idx"
  shows "transforms tm5 tps0 ttt tps5"
  unfolding tm5_def by (tform tps: tps0 H tps3_def tps5_def jk time: assms)

definition "tps6 ≡ tps0
  [j := (⌊Suc idx⌋⇩_N, 1),
   j + 2 := (⌊1⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi (Suc idx * H) H (Suc 0)⌋⇩_N⇩_L⇩_L, 1),
   1 := nlltape (nll_Psi (idx * H) H 1)]"

lemma tm6 [transforms_intros]:
  assumes "ttt = 28 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧²"
  shows "transforms tm6 tps0 ttt tps6"
  unfolding tm6_def
proof (tform tps: tps0 H tps5_def tps6_def jk time: assms)
  show "tps6 = tps5[j + 6 := (⌊nll_Psi (Suc idx * H) H (Suc 0)⌋⇩_N⇩_L⇩_L, 1)]"
    unfolding tps5_def tps6_def using jk
    by (simp add: list_update_swap[of j] list_update_swap[of _ "j + 6"])
qed

definition "tps7 ≡ tps0
  [j := (⌊Suc idx⌋⇩_N, 1),
   j + 2 := (⌊1⌋⇩_N, 1),
   j + 6 := (⌊[]⌋, 1),
   1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"

lemma tm7 [transforms_intros]:
  assumes "ttt = 39 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
    4 * nlllength (nll_Psi (idx * H) H 1) +
    2 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² +
    4 * nlllength (nll_Psi (H + idx * H) H 1)"
  shows "transforms tm7 tps0 ttt tps7"
  unfolding tm7_def by (tform tps: assms tps6_def tps7_def jk)

definition "tps9 ≡ tps0
  [j := (⌊Suc (Suc idx)⌋⇩_N, 1),
   j + 2 := (⌊1⌋⇩_N, 1),
   j + 6 := (⌊[]⌋, 1),
   1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"

lemma tm9 [transforms_intros]:
  assumes "ttt = 44 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx)"
  shows "transforms tm9 tps0 ttt tps9"
  unfolding tm9_def
proof (tform tps: tps0 H tps7_def tps9_def jk time: assms)
  show "tps9 = tps7[j := (⌊Suc (Suc idx)⌋⇩_N, 1)]"
    using tps9_def tps7_def jk by (simp add: list_update_swap)
qed

definition "tps10 ≡ tps0
  [j := (⌊Suc (Suc idx)⌋⇩_N, 1),
   j + 2 := (⌊0⌋⇩_N, 1),
   j + 6 := (⌊[]⌋, 1),
   1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"

lemma tm10 [transforms_intros]:
  assumes "ttt = 56 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx)"
  shows "transforms tm10 tps0 ttt tps10"
  unfolding tm10_def
proof (tform tps: tps0 H tps9_def tps10_def jk)
  show "ttt = 44 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx) + (10 + 2 * nlength (Suc 0) + 2 * nlength 0) "
    using assms canrepr_1 by simp
qed

definition "tps11 ≡ tps0
  [j := (⌊Suc (Suc idx)⌋⇩_N, 1),
   j + 2 := (⌊0⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi (Suc (Suc idx) * H) H 0⌋⇩_N⇩_L⇩_L, 1),
   1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1)]"

lemma tm11 [transforms_intros]:
  assumes "ttt = 56 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧²"
  shows "transforms tm11 tps0 ttt tps11"
  unfolding tm11_def by (tform tps: tps0 H tps10_def tps11_def jk time: assms)

definition "tps12 ≡ tps0
  [j := (⌊Suc (Suc idx)⌋⇩_N, 1),
   j + 2 := (⌊0⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi (Suc (Suc idx) * H) H 0⌋⇩_N⇩_L⇩_L, 1),
   1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1 @ nll_Psi (Suc (Suc idx) * H) H 0)]"

lemma tm12:
  assumes "ttt = 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
  shows "transforms tm12 tps0 ttt tps12"
  unfolding tm12_def by (tform tps: tps11_def tps12_def jk assms)

lemma tm12':
  assumes "ttt = 5627 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧²"
  shows "transforms tm12 tps0 ttt tps12"
proof -
  let ?ttt = "60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * nlllength (nll_Psi (idx * H) H 1) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
  have "?ttt ≤ 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * nlllength (nll_Psi (H + idx * H) H 1) +
      2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
    using nlllength_nll_Psi_le'[of "idx * H" "2 * H + idx * H" "H"] by simp
  also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * H * (3 + nlength (3 * H + idx * H)) +
      2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      2 * nlllength (nll_Psi (H + (H + idx * H)) H 0)"
    using nlllength_nll_Psi_le'[of "H + idx * H" "2 * H + idx * H" "H"] by simp
  also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      4 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 4 * H * (3 + nlength (3 * H + idx * H)) +
      2 * nlength (Suc idx) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      2 * H * (3 + nlength (3 * H + idx * H))"
    using nlllength_nll_Psi_le'[of "H + (H + idx * H)" "2 * H + idx * H" "H"] by simp
  also have "... = 60 + 1851 * H ^ 4 * (nlength (Suc idx))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² + 2 * nlength (Suc idx) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧²"
    by simp
  also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc (Suc idx)))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² + 2 * nlength (Suc idx) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧²"
    using nlength_mono linear_le_pow by simp
  also have "... ≤ 60 + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² + 2 * nlength (Suc idx) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧²"
    using nlength_mono linear_le_pow by simp
  also have "... = 60 + 5553 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength idx + 2 * nlength (Suc idx)"
    by simp
  also have "... ≤ 60 + 5553 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 2 * nlength (Suc idx) + 2 * nlength (Suc idx)"
    using nlength_mono by simp
  also have "... = 60 + 5553 * H ^ 4 * (nlength (Suc (Suc (Suc idx))))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 4 * nlength (Suc idx)"
    by simp
  also have "... ≤ 60 + 5553 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧² +
      10 * H * (3 + nlength (3 * H + idx * H)) + 4 * nlength (Suc idx)"
  proof -
    have "Suc (Suc (Suc idx)) ≤ 3 * H + idx * H"
    proof (cases "idx = 0")
      case True
      then show ?thesis
        using H by simp
    next
      case False
      then show ?thesis
        using H
        by (metis One_nat_def Suc3_eq_add_3 comm_semiring_class.distrib le_Suc_eq less_eq_nat.simps(1) mult.commute
          mult_1 mult_le_mono1 nle_le not_numeral_le_zero)
    qed
    then have "nlength (Suc (Suc (Suc idx))) ≤ 3 + nlength (3 * H + idx * H)"
      using nlength_mono trans_le_add2 by presburger
    then have "nlength (Suc (Suc (Suc idx))) ^ 2 ≤ (3 + nlength (3 * H + idx * H)) ^ 2"
      by simp
    then show ?thesis
      by simp
  qed
  also have "... ≤ 60 + 5553 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧² +
      10 * H ^ 4 * (3 + nlength (3 * H + idx * H)) + 4 * nlength (Suc idx)"
    using linear_le_pow by simp
  also have "... ≤ 60 + 5553 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧² +
      10 * H ^ 4 * (3 + nlength (3 * H + idx * H)) ^ 2 + 4 * nlength (Suc idx)"
    using linear_le_pow by simp
  also have "... = 60 + 5563 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧² + 4 * nlength (Suc idx)"
    by simp
  also have "... ≤ 60 + 5563 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧² +
    4 * H^4 * (3 + nlength (3 * H + idx * H))^2"
  proof -
    have "idx ≤ idx * H"
      using H by simp
    then have "Suc idx ≤ 3 * H + idx * H"
      using H by linarith
    then have "nlength (Suc idx) ≤ 3 + nlength (3 * H + idx * H)"
      using nlength_mono trans_le_add2 by presburger
    also have "... ≤ (3 + nlength (3 * H + idx * H)) ^ 2"
      by (simp add: power2_eq_square)
    also have "... ≤ H * (3 + nlength (3 * H + idx * H)) ^ 2"
      using H by simp
    also have "... ≤ H^4 * (3 + nlength (3 * H + idx * H)) ^ 2"
      using linear_le_pow by simp
    finally have "nlength (Suc idx) ≤ H^4 * (3 + nlength (3 * H + idx * H)) ^ 2" .
    then show ?thesis
      by simp
  qed
  also have "... = 60 + 5567 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧²"
    by simp
  also have "... ≤ 60 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧² + 5567 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧²"
    using H linear_le_pow by simp
  also have "... = 5627 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧²"
    by simp
  finally have "?ttt ≤ ttt"
    using assms by simp
  then show ?thesis
    using tm12 transforms_monotone by simp
qed

end  (* context tps0 *)

end  (* locale turing_machine_PHI0 *)

lemma transforms_tm_PHI0I:
  fixes j :: tapeidx
  fixes tps tps' :: "tape list" and ttt k idx H :: nat
  assumes "length tps = k" and "1 < j" and "j + 8 < k" and "H ≥ 3"
  assumes
    "tps ! 1 = (⌊[]⌋, 1)"
    "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 "tps' = tps
    [j := (⌊Suc (Suc idx)⌋⇩_N, 1),
     j + 2 := (⌊0⌋⇩_N, 1),
     j + 6 := (⌊nll_Psi (Suc (Suc idx) * H) H 0⌋⇩_N⇩_L⇩_L, 1),
     1 := nlltape (nll_Psi (idx * H) H 1 @ nll_Psi (H + idx * H) H 1 @ nll_Psi (Suc (Suc idx) * H) H 0)]"
  assumes "ttt = 5627 * H ^ 4 * (3 + nlength (3 * H + idx * H))⇧²"
  shows "transforms (tm_PHI0 j) tps ttt tps'"
proof -
  interpret loc: turing_machine_PHI0 j .
  show ?thesis
    using loc.tps12_def loc.tm12' loc.tm12_eq_tm_PHI0 assms by metis
qed


subsection ‹A Turing machine for $\Phi_1$›

text ‹
The next TM expects a number $H$ on tape $j + 1$ and appends to the formula on
tape $1$ the formula $\Psi([0, H), 1)$.
›

definition tm_PHI1 :: "tapeidx ⇒ machine" where
  "tm_PHI1 j ≡
    tm_setn (j + 2) 1 ;;
    tm_Psigamma j ;;
    tm_extendl 1 (j + 6)"

lemma tm_PHI1_tm:
  assumes "0 < j" and "j + 7 < k" and "G ≥ 6"
  shows "turing_machine k G (tm_PHI1 j)"
  unfolding tm_PHI1_def using assms tm_Psigamma_tm tm_setn_tm tm_extendl_tm by simp

locale turing_machine_PHI1 =
  fixes j :: tapeidx
begin

definition "tm1 ≡ tm_setn (j + 2) 1"
definition "tm2 ≡ tm1 ;; tm_Psigamma j"
definition "tm3 ≡ tm2 ;; tm_extendl 1 (j + 6)"

lemma tm3_eq_tm_PHI1: "tm3 = tm_PHI1 j"
  using tm3_def tm2_def tm1_def tm_PHI1_def by simp

context
  fixes tps0 :: "tape list" and k idx H :: nat and nss :: "nat list list"
  assumes jk: "length tps0 = k" "1 < j" "j + 7 < k"
    and H: "H ≥ 3"
  assumes tps0:
    "tps0 ! 1 = nlltape nss"
    "tps0 ! j = (⌊0⌋⇩_N, 1)"
    "tps0 ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps0 ! (j + 2) = (⌊[]⌋, 1)"
    "tps0 ! (j + 3) = (⌊[]⌋, 1)"
    "tps0 ! (j + 4) = (⌊[]⌋, 1)"
    "tps0 ! (j + 5) = (⌊[]⌋, 1)"
    "tps0 ! (j + 6) = (⌊[]⌋, 1)"
    "tps0 ! (j + 7) = (⌊[]⌋, 1)"
begin

definition "tps1 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1)]"

lemma tm1 [transforms_intros]:
  assumes "ttt = 12"
  shows "transforms tm1 tps0 ttt tps1"
  unfolding tm1_def
proof (tform tps: tps0 tps1_def jk)
  show "tps0 ! (j + 2) = (⌊0⌋⇩_N, 1)"
    using tps0 jk canrepr_0 by simp
  show "ttt = 10 + 2 * nlength 0 + 2 * nlength 1"
    using assms canrepr_1 by simp
qed

definition "tps2 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi 0 H 1⌋⇩_N⇩_L⇩_L, 1)]"

lemma tm2 [transforms_intros]:
  assumes "ttt = 12 + 1851 * H ^ 4"
  shows "transforms tm2 tps0 ttt tps2"
  unfolding tm2_def
proof (tform tps: tps0 H tps1_def tps2_def jk)
  show "ttt = 12 + 1851 * H ^ 4 * (nlength (Suc 0))⇧²"
    using canrepr_1 assms by simp
qed

definition "tps3 ≡ tps0
  [j + 2 := (⌊1⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi 0 H 1⌋⇩_N⇩_L⇩_L, 1),
   1 := nlltape (nss @ nll_Psi 0 H 1)]"

lemma tm3:
  assumes "ttt = 16 + 1851 * H ^ 4 + 2 * nlllength (nll_Psi 0 H 1)"
  shows "transforms tm3 tps0 ttt tps3"
  unfolding tm3_def by (tform tps: tps0 H tps2_def tps3_def jk time: assms)

lemma tm3':
  assumes "ttt = 1875 * H ^ 4"
  shows "transforms tm3 tps0 ttt tps3"
proof -
  let ?ttt = "16 + 1851 * H ^ 4 + 2 * nlllength (nll_Psi 0 H 1)"
  have "?ttt ≤ 16 + 1851 * H ^ 4 + 2 * H * (3 + nlength H)"
    using nlllength_nll_Psi_le
    by (metis (mono_tags, lifting) add_left_mono mult.assoc nat_mult_le_cancel1 plus_nat.add_0 rel_simps(51))
  also have "... = 16 + 1851 * H ^ 4 + 6 * H + 2 * H * nlength H"
    by algebra
  also have "... ≤ 16 + 1851 * H ^ 4 + 6 * H + 2 * H * H"
    using nlength_le_n by simp
  also have "... ≤ 16 + 1851 * H ^ 4 + 6 * H * H + 2 * H * H"
    by simp
  also have "... = 16 + 1851 * H ^ 4 + 8 * H^2"
    by algebra
  also have "... ≤ 16 + 1851 * H ^ 4 + 8 * H^4"
    using pow_mono'[of 2 4 H] by simp
  also have "... = 16 + 1859 * H ^ 4"
    by simp
  also have "... ≤ 16 * H^4 + 1859 * H ^ 4"
    using H by simp
  also have "... = 1875 * H ^ 4"
    by simp
  finally have "?ttt ≤ 1875 * H ^ 4" .
  then show ?thesis
    using assms tm3 transforms_monotone by simp
qed

end  (* context tps0 *)

end  (* locale turing_machine_PHI1 *)

lemma transforms_tm_PHI1I:
  fixes j :: tapeidx
  fixes tps tps' :: "tape list" and ttt k H :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 7 < k" and "H ≥ 3"
  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 @ nll_Psi 0 H 1)]"
  assumes "ttt = 1875 * H ^ 4"
  shows "transforms (tm_PHI1 j) tps ttt tps'"
proof -
  interpret loc: turing_machine_PHI1 j .
  show ?thesis
    using loc.tps3_def loc.tm3' loc.tm3_eq_tm_PHI1 assms by metis
qed


subsection ‹A Turing machine for $\Phi_2$›

text ‹
The next TM expects a number $i$ on tape $j$ and a number $H$ on tape $j + 1$.
It appends to the formula on tape~$1$ the formula $\Psi([(2i+1)H, (2i+2)H), 3)
\land \Psi([(2i+2)H, (2i+3)H), 3)$.
›

definition tm_PHI2 :: "tapeidx ⇒ machine" where
  "tm_PHI2 j ≡
    tm_times2 j ;;
    tm_incr j ;;
    tm_setn (j + 2) 3 ;;
    tm_Psigamma j ;;
    tm_extendl_erase 1 (j + 6) ;;
    tm_incr j ;;
    tm_Psigamma j ;;
    tm_extendl 1 (j + 6)"

lemma tm_PHI2_tm:
  assumes "0 < j" and "j + 8 < k" and "G ≥ 6"
  shows "turing_machine k G (tm_PHI2 j)"
  unfolding tm_PHI2_def
  using assms tm_Psigamma_tm tm_extendl_tm tm_erase_cr_tm tm_times2_tm tm_incr_tm tm_setn_tm tm_cr_tm tm_extendl_erase_tm
  by simp

locale turing_machine_PHI2 =
  fixes j :: tapeidx
begin

definition "tm1 ≡ tm_times2 j"
definition "tm2 ≡ tm1 ;; tm_incr j"
definition "tm3 ≡ tm2 ;; tm_setn (j + 2) 3"
definition "tm4 ≡ tm3 ;; tm_Psigamma j"
definition "tm5 ≡ tm4 ;; tm_extendl_erase 1 (j + 6)"
definition "tm7 ≡ tm5 ;; tm_incr j"
definition "tm8 ≡ tm7 ;; tm_Psigamma j"
definition "tm9 ≡ tm8 ;; tm_extendl 1 (j + 6)"

lemma tm9_eq_tm_PHI2: "tm9 = tm_PHI2 j"
  using tm9_def tm8_def tm7_def tm5_def tm4_def tm3_def tm2_def tm1_def tm_PHI2_def
  by simp

context
  fixes tps0 :: "tape list" and k idx H :: nat and nss :: "nat list list"
  assumes jk: "length tps0 = k" "1 < j" "j + 7 < k"
    and H: "H ≥ 3"
  assumes tps0:
    "tps0 ! 1 = nlltape nss"
    "tps0 ! j = (⌊idx⌋⇩_N, 1)"
    "tps0 ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps0 ! (j + 2) = (⌊[]⌋, 1)"
    "tps0 ! (j + 3) = (⌊[]⌋, 1)"
    "tps0 ! (j + 4) = (⌊[]⌋, 1)"
    "tps0 ! (j + 5) = (⌊[]⌋, 1)"
    "tps0 ! (j + 6) = (⌊[]⌋, 1)"
    "tps0 ! (j + 7) = (⌊[]⌋, 1)"
begin

definition "tps1 ≡ tps0
  [j := (⌊2 * idx⌋⇩_N, 1)]"

lemma tm1 [transforms_intros]:
  assumes "ttt = 5 + 2 * nlength idx"
  shows "transforms tm1 tps0 ttt tps1"
  unfolding tm1_def by (tform tps: tps0 tps1_def jk assms)

definition "tps2 ≡ tps0
  [j := (⌊2 * idx + 1⌋⇩_N, 1)]"

lemma tm2:
  assumes "ttt = 10 + 2 * nlength idx + 2 * nlength (2 * idx)"
  shows "transforms tm2 tps0 ttt tps2"
  unfolding tm2_def by (tform tps: tps0 H tps1_def tps2_def jk assms)

lemma tm2' [transforms_intros]:
  assumes "ttt = 12 + 4 * nlength idx"
  shows "transforms tm2 tps0 ttt tps2"
proof -
  have "10 + 2 * nlength idx + 2 * nlength (2 * idx) ≤ 10 + 2 * nlength idx + 2 * (Suc (nlength idx))"
    using nlength_times2 by (meson add_left_mono mult_le_mono2)
  then have "10 + 2 * nlength idx + 2 * nlength (2 * idx) ≤ ttt"
    using assms by simp
  then show ?thesis
    using tm2 transforms_monotone by simp
qed

definition "tps3 ≡ tps0
  [j := (⌊2 * idx + 1⌋⇩_N, 1),
   j + 2 := (⌊3⌋⇩_N, 1)]"

lemma tm3 [transforms_intros]:
  assumes "ttt = 26 + 4 * nlength idx"
  shows "transforms tm3 tps0 ttt tps3"
  unfolding tm3_def
proof (tform tps: tps0 H tps2_def tps3_def jk)
  show "tps2 ! (j + 2) = (⌊0⌋⇩_N, 1)"
    using tps2_def jk canrepr_0 tps0 by simp
  show "ttt = 12 + 4 * nlength idx + (10 + 2 * nlength 0 + 2 * nlength 3)"
    using nlength_3 assms by simp
qed

definition "tps4 ≡ tps0
  [j := (⌊2 * idx + 1⌋⇩_N, 1),
   j + 2 := (⌊3⌋⇩_N, 1),
   j + 6 := (⌊nll_Psi (Suc (2 * idx) * H) H 3⌋⇩_N⇩_L⇩_L, 1)]"

lemma tm4 [transforms_intros]:
  assumes "ttt = 26 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧²"
  shows "transforms tm4 tps0 ttt tps4"
  unfolding tm4_def by (tform tps: tps0 H tps3_def tps4_def jk time: assms)

definition "tps5 ≡ tps0
  [j := (⌊2 * idx + 1⌋⇩_N, 1),
   j + 2 := (⌊3⌋⇩_N, 1),
   j + 6 := (⌊[]⌋, 1),
   1 := nlltape (nss @ nll_Psi (H + 2 * idx * H) H 3)]"

lemma tm5 [transforms_intros]:
  assumes "ttt = 37 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3)"
  shows "transforms tm5 tps0 ttt tps5"
  unfolding tm5_def by (tform tps: tps0 H tps4_def tps5_def jk time: assms)

definition "tps7 ≡ tps0
  [j := (⌊2 * idx + 2⌋⇩_N, 1),
   j + 2 := (⌊3⌋⇩_N, 1),
   j + 6 := (⌊[]⌋, 1),
   1 := nlltape (nss @ nll_Psi (H + 2 * idx * H) H 3)]"

lemma tm7:
  assumes "ttt = 42 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
    4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) + 2 * nlength (Suc (2 * idx))"
  shows "transforms tm7 tps0 ttt tps7"
  unfolding tm7_def
proof (tform tps: tps0 H tps5_def tps7_def jk time: assms)
  show "tps7 = tps5[j := (⌊Suc (Suc (2 * idx))⌋⇩_N, 1)]"
    using tps5_def tps7_def jk by (simp add: list_update_swap)
qed

lemma tm7' [transforms_intros]:
  assumes "ttt = 44 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3)"
  shows "transforms tm7 tps0 ttt tps7"
proof -
  let ?ttt = "42 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
      2 * nlength (Suc (2 * idx))"
  have "?ttt ≤ 42 + 4 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
      2 * (Suc (nlength idx))"
    using nlength_times2plus1 by (metis add.commute add_left_mono mult_le_mono2 plus_1_eq_Suc)
  then have "?ttt ≤ ttt"
    using assms by simp
  then show ?thesis
    using tm7 transforms_monotone by simp
qed

definition "tps8 ≡ tps0
  [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 @ nll_Psi (H + 2 * idx * H) H 3)]"

lemma tm8 [transforms_intros]:
  assumes "ttt = 44 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧²"
  shows "transforms tm8 tps0 ttt tps8"
  unfolding tm8_def
proof (tform tps: tps0 H tps7_def tps8_def jk time: assms)
  show "tps8 = tps7
      [j + 6 := (⌊nll_Psi (Suc (Suc (2 * idx)) * H) H 3⌋⇩_N⇩_L⇩_L, 1)]"
    unfolding tps8_def tps7_def by (simp add: list_update_swap[of "j+6"])
qed

definition "tps9 ≡ tps0
  [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 @ nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3)]"

lemma tm9:
  assumes "ttt = 48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧² +
      2 * nlllength (nll_Psi (2 * H + 2 * idx * H) H 3)"
  shows "transforms tm9 tps0 ttt tps9"
  unfolding tm9_def by (tform tps: tps0 H tps9_def tps8_def jk time: assms)

lemma tm9':
  assumes "ttt = 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧²"
  shows "transforms tm9 tps0 ttt tps9"
proof -
  let ?ttt = "48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * nlllength (nll_Psi (H + 2 * idx * H) H 3) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧² +
      2 * nlllength (nll_Psi (2 * H + 2 * idx * H) H 3)"
  have "?ttt ≤ 48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      4 * H * (3 + nlength (2 * H + 2 * idx * H + H)) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧² +
      2 * nlllength (nll_Psi (2 * H + 2 * idx * H) H 3)"
    using nlllength_nll_Psi_le'[of "H + 2 * idx * H" "2 * H + 2 * idx * H" H 3] by simp
  also have "... ≤ 48 + 6 * nlength idx + 1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      5 * H * (3 + nlength (2 * H + 2 * idx * H + H)) + 1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧² +
      3 * H * (3 + nlength (2 * H + 2 * idx * H + H))"
    using nlllength_nll_Psi_le'[of "2 * H + 2 * idx * H" "2 * H + 2 * idx * H" H 3] by simp
  also have "... = 48 + 6 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc (2 * idx))))⇧² +
      8 * H * (3 + nlength (2 * H + 2 * idx * H + H)) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧²"
    by simp
  also have "... ≤ 48 + 6 * nlength idx +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧² +
      8 * H * (3 + nlength (2 * H + 2 * idx * H + H)) +
      1851 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧²"
    using H4_nlength H by simp
  also have "... = 48 + 6 * nlength idx + 3702 * H ^ 4 * (nlength (Suc (Suc (Suc (2 * idx)))))⇧² +
      8 * H * (3 + nlength (3 * H + 2 * idx * H))"
    by simp
  also have "... ≤ 48 + 6 * nlength idx + 3702 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧² +
      8 * H * (3 + nlength (3 * H + 2 * idx * H))"
  proof -
    have "Suc (Suc (Suc (2 * idx))) ≤ 3 * H + 2 * idx * H"
      using H
      by (metis One_nat_def Suc3_eq_add_3 Suc_eq_plus1_left add_leD1 comm_monoid_mult_class.mult_1
        distrib_right mult.commute mult_le_mono1)
    then have "nlength (Suc (Suc (Suc (2 * idx)))) ≤ 3 + nlength (3 * H + 2 * idx * H)"
      using nlength_mono trans_le_add2 by blast
    then show ?thesis
      by simp
  qed
  also have "... ≤ 48 + 6 * nlength idx + 3702 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧² +
      8 * H^4 * (3 + nlength (3 * H + 2 * idx * H))"
    using linear_le_pow by simp
  also have "... ≤ 48 + 6 * nlength idx + 3702 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧² +
      8 * H^4 * (3 + nlength (3 * H + 2 * idx * H))^2"
    using linear_le_pow by simp
  also have "... = 48 + 6 * nlength idx + 3710 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧²"
    by simp
  also have "... ≤ 48 + 3716 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧²"
  proof -
    have "nlength idx ≤ nlength (3 * H + 2 * idx * H)"
      using H by (intro nlength_mono) (simp add: trans_le_add2)
    also have "... ≤ 3 + nlength (3 * H + 2 * idx * H)"
      by simp
    also have "... ≤ (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
      using linear_le_pow by simp
    also have "... ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
      using H by simp
    finally have "nlength idx ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2" .
    then show ?thesis
      by simp
  qed
  also have "... ≤ 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧²"
  proof -
    have "1 ≤ nlength (3 * H + 2 * idx * H)"
      using H nlength_0
      by (metis One_nat_def Suc_leI add_eq_0_iff_both_eq_0 length_0_conv length_greater_0_conv mult_Suc
        not_numeral_le_zero numeral_3_eq_3)
    also have "... ≤ 3 + nlength (3 * H + 2 * idx * H)"
      by simp
    also have "... ≤ (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
      using linear_le_pow by simp
    also have "... ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2"
      using H by simp
    finally have "1 ≤ H ^ 4 * (3 + nlength (3 * H + 2 * idx * H)) ^ 2" .
    then show ?thesis
      by simp
  qed
  finally have "?ttt ≤ 3764 * H ^ 4 * (3 + nlength (3 * H + 2 * idx * H))⇧²" .
  then show ?thesis
    using assms tm9 transforms_monotone by simp
qed

end  (* context tps0 *)

end  (* locale turing_machine_PHI2 *)

lemma transforms_tm_PHI2I:
  fixes j :: tapeidx
  fixes tps tps' :: "tape list" and ttt k idx H :: nat and nss :: "nat list list"
  assumes "length tps = k" and "1 < j" and "j + 8 < k"
    and "H ≥ 3"
  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 @ nll_Psi (H + 2 * idx * H) H 3 @ nll_Psi (2 * H + 2 * idx * H) H 3)]"
  shows "transforms (tm_PHI2 j) tps ttt tps'"
proof -
  interpret loc: turing_machine_PHI2 j .
  show ?thesis
    using loc.tm9' loc.tps9_def loc.tm9_eq_tm_PHI2 assms by simp
qed


subsection ‹Turing machines for $\Phi_3$, $\Phi_4$, and $\Phi_5$›

text ‹
The CNF formulas $\Phi_3$, $\Phi_4$, and $\Phi_5$ have a similar structure and
can thus be handled by the same Turing machine. The following TM has a parameter
$step$ and the usual tape parameter $j$. It expects on tape $j$ a number $idx$,
on tape $j + 1$ a number $H$, on tape $j + 2$ a number $\kappa$, and on tape $j
+ 8$ the number $idx + step \cdot numiter$ for some number $numiter$. It appends
to the CNF formula on tape~$1$ the formula $\Psi(\gamma_{idx}, \kappa) \land
\Psi(\gamma_{idx + step\cdot (numiter - 1)}, \kappa)$, where $\gamma_i = [iH,
(i+1)H)$.

\null
›

definition tm_PHI345 :: "nat ⇒ tapeidx ⇒ machine" where
  "tm_PHI345 step j ≡
    WHILE tm_equalsn j (j + 8) (j + 3) ; λrs. rs ! (j + 3) = □ DO
      tm_Psigamma j ;;
      tm_extendl_erase 1 (j + 6) ;;
      tm_plus_const step j
    DONE"

lemma tm_PHI345_tm:
  assumes "G ≥ 6" and "0 < j" and "j + 8 < k"
  shows "turing_machine k G (tm_PHI345 step j)"
  unfolding tm_PHI345_def
  using assms tm_equalsn_tm tm_Psigamma_tm tm_extendl_erase_tm tm_plus_const_tm
    turing_machine_loop_turing_machine
  by simp

locale turing_machine_PHI345 =
  fixes step :: nat and j :: tapeidx
begin

definition "tmC ≡ tm_equalsn j (j + 8) (j + 3)"
definition "tm1 ≡ tm_Psigamma j"
definition "tm2 ≡ tm1 ;; tm_extendl_erase 1 (j + 6)"
definition "tm4 ≡ tm2 ;; tm_plus_const step j"
definition "tmL ≡ WHILE tmC ; λrs. rs ! (j + 3) = □ DO tm4 DONE"

lemma tmL_eq_tm_PHI345: "tmL = tm_PHI345 step j"
  unfolding tmL_def tm4_def tm2_def tm1_def tm_PHI345_def tmC_def by simp

context
  fixes tps0 :: "tape list" and numiter H k idx kappa :: nat and nss :: "nat list list"
  assumes jk: "length tps0 = k" "1 < j" "j + 8 < k"
    and H: "H ≥ 3"
    and kappa: "kappa ≤ H"
    and step: "step > 0"
  assumes tps0:
    "tps0 ! 1 = nlltape nss"
    "tps0 ! j = (⌊idx⌋⇩_N, 1)"
    "tps0 ! (j + 1) = (⌊H⌋⇩_N, 1)"
    "tps0 ! (j + 2) = (⌊kappa⌋⇩_N, 1)"
    "tps0 ! (j + 3) = (⌊[]⌋, 1)"
    "tps0 ! (j + 4) = (⌊[]⌋, 1)"
    "tps0 ! (j + 5) = (⌊[]⌋, 1)"
    "tps0 ! (j + 6) = (⌊[]⌋, 1)"
    "tps0 ! (j + 7) = (⌊[]⌋, 1)"
    "tps0 ! (j + 8) = (⌊idx + step * numiter⌋⇩_N, 1)"
begin

definition tpsL :: "nat ⇒ tape list" where
  "tpsL t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]))]"

lemma tpsL_eq_tps0: "tpsL 0 = tps0"
proof -
  have "⌊idx⌋⇩_N = ⌊idx + step * 0⌋⇩_N"
    by simp
  moreover have "nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<0])) = nlltape nss"
    using nllcontents_Nil by simp
  ultimately show ?thesis
    using tpsL_def tps0 jk by (metis list_update_id)
qed

definition tpsC :: "nat ⇒ tape list" where
  "tpsC t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])),
     j + 3 := (⌊t = numiter⌋⇩_B, 1)]"

lemma tmC:
  assumes "t ≤ numiter"
    and "ttt = 3 * nlength (idx + step * t) + 7"
  shows "transforms tmC (tpsL t) ttt (tpsC t)"
  unfolding tmC_def
proof (tform tps: tps0 tpsL_def jk)
  show "tpsL t ! (j + 3) = (⌊0⌋⇩_N, 1)"
    using canrepr_0 jk tpsL_def tps0 by simp
  show "(0::nat) ≤ 1"
    by simp
  show "tpsC t = (tpsL t)
      [j + 3 := (⌊idx + step * t = idx + step * numiter⌋⇩_B, 1)]"
    using step tpsC_def jk tpsL_def tps0 by simp
  show "ttt = 3 * nlength (min (idx + step * t) (idx + step * numiter)) + 7"
    using assms by (simp add: min_def)
qed

lemma tmC' [transforms_intros]:
  assumes "t ≤ numiter"
    and "ttt = 3 * nlength (idx + step * numiter) + 7"
  shows "transforms tmC (tpsL t) ttt (tpsC t)"
proof -
  have "3 * nlength (idx + step * t) + 7 ≤ ttt"
    using assms nlength_mono by simp
  then show ?thesis
    using assms tmC transforms_monotone by blast
qed

definition tpsL0 :: "nat ⇒ tape list" where
  "tpsL0 t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]))]"

lemma tpsL0_eq_tpsC:
  assumes "t < numiter"
  shows "tpsL0 t = tpsC t"
  unfolding tpsL0_def tpsC_def
  using assms jk ncontents_0 tps0 list_update_id[of tps0 "j + 3"]
  by (simp add: list_update_swap)

definition tpsL1 :: "nat ⇒ tape list" where
  "tpsL1 t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])),
     j + 6 := (⌊nll_Psi ((idx+step*t) * H) H kappa⌋⇩_N⇩_L⇩_L, 1)]"

lemma tm1 [transforms_intros]:
  assumes "t < numiter"
    and "ttt = 1851 * H ^ 4 * (nlength (Suc (idx+step*t)))⇧²"
  shows "transforms tm1 (tpsL0 t) ttt (tpsL1 t)"
  unfolding tm1_def by (tform tps: H kappa tps0 tpsL0_def tpsL1_def jk time: assms(2))

definition tpsL2 :: "nat ⇒ tape list" where
  "tpsL2 t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])),
     j + 6 := (⌊[]⌋, 1),
     1 := nlltape ((nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t])) @ nll_Psi ((idx+step*t) * H) H kappa)]"

lemma tm2:
  assumes "t < numiter"
    and "ttt = 1851 * H ^ 4 * (nlength (Suc (idx + step * t)))⇧² +
      (11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
  shows "transforms tm2 (tpsL0 t) ttt (tpsL2 t)"
  unfolding tm2_def by (tform tps: assms H kappa tps0 tpsL1_def tpsL2_def jk)

definition tpsL2' :: "nat ⇒ tape list" where
  "tpsL2' t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     j + 6 := (⌊[]⌋, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]) @ nll_Psi ((idx+step*t) * H) H kappa)]"

lemma tpsL2': "tpsL2 t = tpsL2' t"
  unfolding tpsL2_def tpsL2'_def by (simp only: list_update_swap list_update_overwrite) simp

lemma tm2':
  assumes "t < numiter"
    and "ttt = 1851 * H ^ 4 * (nlength (idx + step * numiter))⇧² +
      (11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
  shows "transforms tm2 (tpsL0 t) ttt (tpsL2' t)"
proof -
  let ?ttt = "1851 * H ^ 4 * (nlength (Suc (idx + step * t)))⇧² +
      (11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
  have "?ttt ≤ 1851 * H ^ 4 * (nlength (idx + step * numiter))⇧² +
      (11 + 4 * nlllength (nll_Psi ((idx + step * t) * H) H kappa))"
  proof -
    have "Suc (idx + step * t) ≤ Suc (idx + step * (numiter - 1))"
      using assms(1) step by simp
    also have "... = Suc (idx + step * numiter - step)"
      by (metis Nat.add_diff_assoc One_nat_def Suc_le_eq add_less_same_cancel1 assms(1) mult.right_neutral
       nat_mult_le_cancel_disj nat_neq_iff not_add_less1 right_diff_distrib')
    also have "... ≤ idx + step * numiter"
      using step Suc_le_eq assms(1) by simp
    finally have "Suc (idx + step * t) ≤ idx + step * numiter" .
    then have "nlength (Suc (idx + step * t)) ≤ nlength (idx + step * numiter)"
      using nlength_mono by simp
    then show ?thesis
      by simp
  qed
  then have "transforms tm2 (tpsL0 t) ttt (tpsL2 t)"
    using assms tm2 transforms_monotone by blast
  then show ?thesis
    using tpsL2' by simp
qed

definition tpsL2'' :: "nat ⇒ tape list" where
  "tpsL2'' t ≡ tps0
    [j := (⌊idx + step * t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<Suc t])),
     j + 6 := (⌊[]⌋, 1)]"

lemma tpsL2'': "tpsL2'' t = tpsL2' t"
proof -
  have "nll_Psi ((idx+step*t) * H) H kappa = nll_Psi (H * (idx+step*t)) H kappa"
    by (simp add: mult.commute)
  then have "concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<t]) @ nll_Psi ((idx+step*t) * H) H kappa =
      concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0..<Suc t])"
    by simp
  then show "tpsL2'' t = tpsL2' t"
    using tpsL2'_def tpsL2''_def by (simp add: list_update_swap)
qed

lemma nlllength_nll_Psi:
  assumes "t < numiter"
  shows "nlllength (nll_Psi ((idx + step * t) * H) H kappa) ≤ 5 * H ^ 4 * nlength (idx + step * numiter)^2"
proof -
  have "nlllength (nll_Psi ((idx + step * t) * H) H kappa) ≤ H * (3 + nlength ((idx + step * t) * H + H))"
    using nlllength_nll_Psi_le by simp
  also have "... ≤ H * (3 + nlength ((idx + step * numiter) * H))"
  proof -
    have "(idx + 1 + step * t) ≤ (idx + step * Suc t)"
      using step by simp
    then have "(idx + 1 + step * t) ≤ (idx + step * numiter)"
      using assms(1) Suc_le_eq by auto
    then have "(idx + 1 + step * t) * H ≤ (idx + step * numiter) * H"
      using mult_le_cancel2 by blast
    then show ?thesis
      using nlength_mono by simp
  qed
  also have "... = 3 * H + H * nlength ((idx + step * numiter) * H)"
    by algebra
  also have "... ≤ 3 * H + H * (nlength (idx + step * numiter) + nlength H)"
    using nlength_prod by simp
  also have "... ≤ 3 * H + H * (nlength (idx + step * numiter) + H)"
    using nlength_le_n by simp
  also have "... = 3 * H + H ^ 2 + H * nlength (idx + step * numiter)"
    by algebra
  also have "... ≤ 3 * H^4 + H ^ 2 + H * nlength (idx + step * numiter)"
    using linear_le_pow by simp
  also have "... ≤ 3 * H^4 + H ^ 4 + H * nlength (idx + step * numiter)"
    using pow_mono' by simp
  also have "... ≤ 4 * H^4 + H ^ 4 * nlength (idx + step * numiter)"
    using linear_le_pow by simp
  also have "... ≤ 4 * H^4 + H ^ 4 * nlength (idx + step * numiter)^2"
    using linear_le_pow by simp
  also have "... ≤ 5 * H ^ 4 * nlength (idx + step * numiter)^2"
  proof -
    have "idx + step * numiter > 0"
      using assms(1) step by simp
    then have "nlength (idx + step * numiter) > 0"
      using nlength_0 by simp
    then have "nlength (idx + step * numiter) ^ 2 > 0"
      by simp
    then have "H ^ 4 ≤ H ^ 4 * nlength (idx + step * numiter) ^ 2"
      by (metis One_nat_def Suc_leI mult_numeral_1_right nat_mult_le_cancel_disj numerals(1))
    then show ?thesis
      by simp
  qed
  finally show ?thesis .
qed

lemma tm2'' [transforms_intros]:
  assumes "t < numiter" and "ttt = 1871 * H ^ 4 * (nlength (idx + step * numiter))⇧² + 11"
  shows "transforms tm2 (tpsL0 t) ttt (tpsL2'' t)"
proof -
  have "transforms tm2 (tpsL0 t) ttt (tpsL2' t)"
    using tm2'[OF assms(1)] nlllength_nll_Psi[OF assms(1)] transforms_monotone assms(2) by simp
  then show ?thesis
    using tpsL2' tpsL2'' by simp
qed

definition tpsL4 :: "nat ⇒ tape list" where
  "tpsL4 t ≡ tps0
    [j := (⌊idx + step * Suc t⌋⇩_N, 1),
     1 := nlltape (nss @ concat (map (λi. nll_Psi (H * (idx + step * i)) H kappa) [0