Theory AlphabetEnlargement_ValidationBound

theory AlphabetEnlargement_ValidationBound
  imports AlphabetEnlargement_ValidationStep
begin

subsection ‹Validation sweeps, post-state, and step bound›

subsubsection ‹Validation sweeps and tape correspondence›

text ‹Forward-sweep iteration helper.  Starting from
  ‹ae_init_config M w›, after ‹Suc k› validation steps along a
  ‹k›-pure prefix of ‹w›, the head on tape 0 is at position
  ‹Suc k› and the phase is still ‹VFwd›.  The chain is built
  by induction on ‹k›, applying ‹ae_step_val_fwd_advance› once
  per step (the LE block at position 0 takes the first step, then
  each pure block along positions ‹1…k› takes one more).›

lemma ae_validation_fwd_sweep_pure:
  fixes M :: "('q, 'a) mttm"
    and w :: "(('c :: enum) ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and s_in_Q: "s_tm M ∈ Q_tm M"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
      and k_bound: "k ≤ length w"
      and pure: "∀i < k. is_pure_block (bl_tm M) (w ! i)"
  shows "(ae_init_config M w,
            Config⇩M (s_tm M, init_stage (le_tm M))
                     (mt_tape (ae_init_config M w))
                     (λi :: nat. if i = 0 then Suc k else 0))
           ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc k"
  using k_bound pure
proof (induction k)
  case 0
  let ?ts = "mt_tape (ae_init_config M w)"
  let ?n0 = "λ_ :: nat. 0 :: nat"
  let ?n1 = "λi :: nat. if i = 0 then Suc 0 else 0"
  have init_eq: "ae_init_config M w
                  = Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n0"
    by (simp add: ae_init_config_def)
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have read: "?ts 0 (?n0 0) = LE_block (le_tm M)
              ∨ is_pure_block (bl_tm M) (?ts 0 (?n0 0))"
    using ae_init_config_tape_le[OF kpos] by auto
  have bt_all: "∀j≥k_tm M. ∀i. ?ts j i = bl_block (bl_tm M)"
    using ae_init_config_tape_blank_tail by blast
  have gamma: "∀kk :: nat. ?ts kk (?n0 kk) ∈ gamma_block (Γ_tm M)"
    using ae_init_config_in_gamma_block[OF vM w_sub] by simp
  have buf_gamma_init:
      "∀kk :: nat.
          fst (init_buffer (le_tm M) kk
                  :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
              ∈ gamma_block (Γ_tm M)
          ∧ fst (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)
          ∧ snd (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)"
    by (rule init_buffer_in_gamma_block_at_M[OF vM])
  have step1: "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                            init_dest, VFwd) ?ts ?n0,
                Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                            init_dest, VFwd) ?ts
                  (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                                 (?n0 kk)))
                ∈ mttm_step (alphabet_enlarge_delta M)"
    by (rule ae_step_val_fwd_advance[where ts = ?ts and n = ?n0,
                                     OF s_in_Q s_neq_t s_neq_r read bt_all
                                        init_stage_tail gamma buf_gamma_init])
  have post_eq:
    "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n0 kk)) = ?n1"
    by (rule ext) simp
  have step1_n1: "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                              init_dest, VFwd) ?ts ?n0,
                   Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                              init_dest, VFwd) ?ts ?n1)
                  ∈ mttm_step (alphabet_enlarge_delta M)"
    using step1 post_eq by simp
  have stage_eq: "init_stage (le_tm M)
                  = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
    unfolding init_stage_def ..
  have step1_init: "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n0,
                     Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n1)
                    ∈ mttm_step (alphabet_enlarge_delta M)"
    using step1_n1 unfolding stage_eq by simp
  have chain1: "(ae_init_config M w,
                  Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n1)
                 ∈ mttm_step (alphabet_enlarge_delta M)"
    using step1_init init_eq by simp
  show ?case using chain1 by (simp add: relpow_1)
next
  case (Suc k)
  let ?ts = "mt_tape (ae_init_config M w)"
  let ?n_k = "λi :: nat. if i = 0 then Suc k else 0"
  let ?n_Sk = "λi :: nat. if i = 0 then Suc (Suc k) else 0"
  have k_le: "k ≤ length w" using Suc.prems(1) by simp
  have pure_k: "∀i < k. is_pure_block (bl_tm M) (w ! i)"
    using Suc.prems(2) by simp
  from Suc.IH[OF k_le pure_k]
  have IH: "(ae_init_config M w,
              Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_k)
              ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc k" .
  have read_pure: "is_pure_block (bl_tm M) (w ! k)"
    using Suc.prems(2) by auto
  have Sk_pos: "1 ≤ Suc k" by simp
  have Sk_le: "Suc k ≤ length w" using Suc.prems(1) .
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have read_eq: "?ts 0 (Suc k) = w ! k"
    using ae_init_config_tape_input[OF Sk_pos Sk_le kpos] by simp
  have read: "?ts 0 (?n_k 0) = LE_block (le_tm M)
              ∨ is_pure_block (bl_tm M) (?ts 0 (?n_k 0))"
    using read_pure read_eq by simp
  have bt_all: "∀j≥k_tm M. ∀i. ?ts j i = bl_block (bl_tm M)"
    using ae_init_config_tape_blank_tail by blast
  have gamma: "∀kk :: nat. ?ts kk (?n_k kk) ∈ gamma_block (Γ_tm M)"
    using ae_init_config_in_gamma_block[OF vM w_sub] by simp
  have buf_gamma_init:
      "∀kk :: nat.
          fst (init_buffer (le_tm M) kk
                  :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
              ∈ gamma_block (Γ_tm M)
          ∧ fst (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)
          ∧ snd (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)"
    by (rule init_buffer_in_gamma_block_at_M[OF vM])
  have step: "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                            init_dest, VFwd) ?ts ?n_k,
                Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                            init_dest, VFwd) ?ts
                  (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                                 (?n_k kk)))
                ∈ mttm_step (alphabet_enlarge_delta M)"
    by (rule ae_step_val_fwd_advance[where ts = ?ts and n = ?n_k,
                                     OF s_in_Q s_neq_t s_neq_r read bt_all
                                        init_stage_tail gamma buf_gamma_init])
  have post_eq:
    "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n_k kk)) = ?n_Sk"
    by (rule ext) simp
  have step_n_Sk: "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                                init_dest, VFwd) ?ts ?n_k,
                    Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                                init_dest, VFwd) ?ts ?n_Sk)
                   ∈ mttm_step (alphabet_enlarge_delta M)"
    using step post_eq by simp
  have stage_eq: "init_stage (le_tm M)
                  = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
    unfolding init_stage_def ..
  have step_init: "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_k,
                    Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_Sk)
                   ∈ mttm_step (alphabet_enlarge_delta M)"
    using step_n_Sk unfolding stage_eq by simp
  show ?case by (rule relpow_Suc_I[OF IH step_init])
qed

text ‹Return-sweep iteration helper.  Symmetric counterpart to
  the forward sweep: starting at ‹VRet› with the head on tape 0
  at position ‹p›, retreat to position 0 in ‹p› applications of
  ‹ae_step_val_ret_step›, then take one more step via
  ‹ae_step_val_ret_to_sim› to reach ‹SS1›.  Total: ‹Suc p›
  steps.  The non-LE constraint on positions ‹1…p› is hoisted
  into the goal as a ‹⟶›-form so the standard induction on
  ‹p› exposes the correct restriction at the IH.›

lemma ae_validation_ret_sweep:
  fixes M :: "('q, 'a) mttm"
    and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
    and q :: 'q
    and ofs :: "nat ⇒ 'c"
    and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
    and dest :: "nat ⇒ ae_dest"
    and p :: nat
  assumes q_in: "q ∈ Q_tm M"
      and tape_le: "ts (0 :: nat) 0 = LE_block (le_tm M)"
      and gamma: "∀k i. ts k i ∈ gamma_block (Γ_tm M)"
      and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
                            ∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
                            ∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
      and bt: "∀k≥k_tm M. ∀i. ts k i = bl_block (bl_tm M)"
      and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
                        ∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
                        ∧ (∀j≥k_tm M. dest j = init_dest j)"
  shows "(∀i. 1 ≤ i ∧ i ≤ p ⟶ ts 0 i ≠ LE_block (le_tm M))
         ⟶ (Config⇩M (q, ofs, buf, dest, VRet) ts
                       (λi :: nat. if i = 0 then p else 0),
              Config⇩M (q, ofs, buf, dest, SS1) ts (λ_. 0))
              ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc p"
proof (induction p)
  case 0
  let ?n0 = "λ_ :: nat. 0 :: nat"
  have read: "ts (0 :: nat) (?n0 0) = LE_block (le_tm M)"
    using tape_le by simp
  have gamma_at: "∀k :: nat. ts k (?n0 k) ∈ gamma_block (Γ_tm M)"
    using gamma by simp
  have step1: "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n0,
                 Config⇩M (q, ofs, buf, dest, SS1) ts ?n0)
                ∈ mttm_step (alphabet_enlarge_delta M)"
    by (rule ae_step_val_ret_to_sim[where ts = ts and n = ?n0,
                                    OF q_in read bt stage_tail gamma_at
                                       buf_gamma])
  have shape_eq: "(λi :: nat. if i = 0 then (0 :: nat) else 0) = ?n0"
    by (rule ext) simp
  show ?case
  proof
    assume "(∀i. 1 ≤ i ∧ i ≤ 0 ⟶ ts 0 i ≠ LE_block (le_tm M))"
    have one_step: "(Config⇩M (q, ofs, buf, dest, VRet) ts
                       (λi :: nat. if i = 0 then 0 else 0),
                     Config⇩M (q, ofs, buf, dest, SS1) ts (λ_. 0))
                    ∈ mttm_step (alphabet_enlarge_delta M)"
      using step1 shape_eq by simp
    thus "(Config⇩M (q, ofs, buf, dest, VRet) ts
              (λi :: nat. if i = 0 then 0 else 0),
            Config⇩M (q, ofs, buf, dest, SS1) ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc 0"
      by (simp add: relpow_1)
  qed
next
  case (Suc p)
  let ?n_Sp = "λi :: nat. if i = 0 then Suc p else 0"
  let ?n_p = "λi :: nat. if i = 0 then p else 0"
  show ?case
  proof
    assume tape_non_le_Sp:
      "(∀i. 1 ≤ i ∧ i ≤ Suc p ⟶ ts 0 i ≠ LE_block (le_tm M))"
    have read_non_le: "ts (0 :: nat) (?n_Sp 0) ≠ LE_block (le_tm M)"
      using tape_non_le_Sp[rule_format, of "Suc p"] by simp
    have gamma_Sp: "∀k :: nat. ts k (?n_Sp k) ∈ gamma_block (Γ_tm M)"
      using gamma by simp
    have step1: "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n_Sp,
                   Config⇩M (q, ofs, buf, dest, VRet) ts
                     (λkk. go_dir (if kk = (0 :: nat) then dir.L else dir.N)
                                   (?n_Sp kk)))
                  ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_ret_step[where ts = ts and n = ?n_Sp,
                                    OF q_in read_non_le bt stage_tail
                                       gamma_Sp buf_gamma])
    have post_eq:
      "(λkk :: nat. go_dir (if kk = 0 then dir.L else dir.N) (?n_Sp kk))
       = ?n_p"
      by (rule ext) simp
    have step1_p: "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n_Sp,
                    Config⇩M (q, ofs, buf, dest, VRet) ts ?n_p)
                   ∈ mttm_step (alphabet_enlarge_delta M)"
      using step1 post_eq by simp
    have tape_non_le_p:
      "∀i. 1 ≤ i ∧ i ≤ p ⟶ ts 0 i ≠ LE_block (le_tm M)"
      using tape_non_le_Sp by auto
    have IH_chain: "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n_p,
                     Config⇩M (q, ofs, buf, dest, SS1) ts (λ_. 0))
                    ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc p"
      using Suc.IH tape_non_le_p by blast
    show "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n_Sp,
            Config⇩M (q, ofs, buf, dest, SS1) ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc p)"
      by (rule relpow_Suc_I2[OF step1_p IH_chain])
  qed
qed

text ‹Partial return sweep: ‹m› leftward ‹VRet› steps from head
  ‹p› reach head ‹p - m›, staying in ‹VRet›, provided every visited
  cell ‹1 … p› is non-‹LE› (so the return never short-circuits to
  ‹SS1›).  This exposes each intermediate validation config as a
  reachable witness, which the full ‹ae_validation_ret_sweep› hides
  behind its composed endpoint.  Used by ‹ae_validation_prefix_markers›
  to supply return-phase witnesses for the prefix-uniqueness induction.›

lemma ae_validation_ret_partial:
  fixes M :: "('q, 'a) mttm"
    and ts :: "nat ⇒ nat ⇒ ('c :: enum ⇒ 'a)"
    and q :: 'q
    and ofs :: "nat ⇒ 'c"
    and buf :: "nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)"
    and dest :: "nat ⇒ ae_dest"
    and p :: nat
  assumes q_in: "q ∈ Q_tm M"
      and gamma: "∀k i. ts k i ∈ gamma_block (Γ_tm M)"
      and buf_gamma: "∀k. fst (buf k) ∈ gamma_block (Γ_tm M)
                            ∧ fst (snd (buf k)) ∈ gamma_block (Γ_tm M)
                            ∧ snd (snd (buf k)) ∈ gamma_block (Γ_tm M)"
      and bt: "∀k≥k_tm M. ∀i. ts k i = bl_block (bl_tm M)"
      and stage_tail: "(∀j≥k_tm M. ofs j = init_offset j)
                        ∧ (∀j≥k_tm M. buf j = init_buffer (le_tm M) j)
                        ∧ (∀j≥k_tm M. dest j = init_dest j)"
      and non_le: "∀i. 1 ≤ i ∧ i ≤ p ⟶ ts 0 i ≠ LE_block (le_tm M)"
  shows "m ≤ p
         ⟶ (Config⇩M (q, ofs, buf, dest, VRet) ts
                       (λi :: nat. if i = 0 then p else 0),
              Config⇩M (q, ofs, buf, dest, VRet) ts
                       (λi :: nat. if i = 0 then p - m else 0))
              ∈ mttm_step (alphabet_enlarge_delta M) ^^ m"
proof (induction m)
  case 0
  have eq: "p - 0 = p" by simp
  show ?case unfolding eq by simp
next
  case (Suc m)
  let ?n_pm = "λi :: nat. if i = 0 then p - m else 0"
  let ?n_pSm = "λi :: nat. if i = 0 then p - Suc m else 0"
  show ?case
  proof
    assume Sm_le: "Suc m ≤ p"
    have m_le: "m ≤ p" using Sm_le by simp
    have pm_pos: "1 ≤ p - m" using Sm_le by simp
    have pm_le: "p - m ≤ p" by simp
    have read_non_le: "ts (0 :: nat) (?n_pm 0) ≠ LE_block (le_tm M)"
      using non_le[rule_format, of "p - m"] pm_pos pm_le by simp
    have gamma_pm: "∀k :: nat. ts k (?n_pm k) ∈ gamma_block (Γ_tm M)"
      using gamma by simp
    have step1: "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n_pm,
                   Config⇩M (q, ofs, buf, dest, VRet) ts
                     (λkk. go_dir (if kk = (0 :: nat) then dir.L else dir.N)
                                   (?n_pm kk)))
                  ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_ret_step[where ts = ts and n = ?n_pm,
                                    OF q_in read_non_le bt stage_tail
                                       gamma_pm buf_gamma])
    have post_eq:
      "(λkk :: nat. go_dir (if kk = 0 then dir.L else dir.N) (?n_pm kk))
       = ?n_pSm"
      using pm_pos by (rule_tac ext) simp
    have step1_pSm:
      "(Config⇩M (q, ofs, buf, dest, VRet) ts ?n_pm,
         Config⇩M (q, ofs, buf, dest, VRet) ts ?n_pSm)
        ∈ mttm_step (alphabet_enlarge_delta M)"
      using step1 post_eq by simp
    have IH_chain:
      "(Config⇩M (q, ofs, buf, dest, VRet) ts
                 (λi :: nat. if i = 0 then p else 0),
        Config⇩M (q, ofs, buf, dest, VRet) ts ?n_pm)
        ∈ mttm_step (alphabet_enlarge_delta M) ^^ m"
      using Suc.IH m_le by blast
    show "(Config⇩M (q, ofs, buf, dest, VRet) ts
                    (λi :: nat. if i = 0 then p else 0),
           Config⇩M (q, ofs, buf, dest, VRet) ts ?n_pSm)
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc m"
      by (rule relpow_Suc_I[OF IH_chain step1_pSm])
  qed
qed

text ‹Tape correspondence at the initial configuration: the
  substrate's ‹init_config› tape (raw input ‹u›) corresponds to
  the AE-side ‹ae_init_config› tape (encoded block list
  ‹encode_input bl_M u›) under ‹ae_tape_correspondence›.  The
  three position regions match one-to-one:
  ▪ position ‹0›: substrate has ‹LE = le_M›; ae has ‹LE_block›
    (the correspondence's ‹tM 0 = le› conjunct);
  ▪ tape ‹0›, position ‹p = (s-1)⋅c + c_idx i + 1 ≤ length u›:
    substrate has ‹u ! (p-1)›; ae has ‹encode_input ! (s-1)› at
    offset ‹i›, which by ‹encode_input_nth› is ‹u ! (p-1)›;
  ▪ any position past the input or any tape ‹k ≠ 0›: both sides
    deliver ‹bl_M = blank_M›.›
lemma ae_tape_correspondence_init:
  fixes M :: "('q, 'a) mttm"
    and u :: "'a list"
  assumes vM: "valid_mttm M"
      and u_sub: "set u ⊆ Sigma_tm M"
  shows "∀k<k_tm M. ae_tape_correspondence (le_tm M)
              (mt_tape (init_config_mttm M u) k)
              (mt_tape (ae_init_config M
                         (encode_input (bl_tm M) u
                              :: ('c :: enum ⇒ 'a) list)) k)"
proof (intro allI impI)
  fix k :: nat
  assume k_lt: "k < k_tm M"
  have kpos: "0 < k_tm M" using k_lt by linarith
  obtain Q Σ Γ bl le δ sM tM r kM where MTTM:
    "M = MTTM Q Σ Γ bl le δ sM tM r kM"
    using mttm.exhaust by metis
  let ?w = "encode_input (bl_tm M) u :: ('c :: enum ⇒ 'a) list"
  let ?c = "card (UNIV :: 'c set)"
  show "ae_tape_correspondence (le_tm M)
          (mt_tape (init_config_mttm M u) k)
          (mt_tape (ae_init_config M ?w) k)"
    unfolding ae_tape_correspondence_def
  proof (intro conjI allI impI)
    show "mt_tape (init_config_mttm M u) k 0 = le_tm M"
      using MTTM k_lt by simp
  next
    fix s :: nat and i :: 'c
    assume s_ge: "1 ≤ s"
    let ?p = "(s - 1) * ?c + c_idx i + 1"
    have p_pos: "?p ≥ 1" by simp
    show "mt_tape (init_config_mttm M u) k ?p
          = mt_tape (ae_init_config M ?w) k s i"
    proof (cases "k = 0")
      case False
      have subst:
        "mt_tape (init_config_mttm M u) k ?p = bl_tm M"
        using MTTM False p_pos by simp
      have ae:
        "mt_tape (ae_init_config M ?w) k s i = bl_tm M"
        unfolding ae_init_config_def using s_ge False
        by (simp add: bl_block_def)
      show ?thesis using subst ae by simp
    next
      case True
      have k_eq: "k = 0" using True .
      show ?thesis
      proof (cases "?p ≤ length u")
        case False
        have p_gt: "length u < ?p" using False by simp
        have subst_bl:
          "mt_tape (init_config_mttm M u) k ?p = bl_tm M"
          using MTTM k_eq p_pos p_gt by simp
        have ae_bl:
          "mt_tape (ae_init_config M ?w) k s i = bl_tm M"
        proof (cases "s ≤ length ?w")
          case False
          thus ?thesis
            unfolding ae_init_config_def using s_ge k_eq
            by (simp add: bl_block_def)
        next
          case True
          have s_minus_1_lt: "s - 1 < length ?w"
            using True s_ge by simp
          have nth_eq:
            "(?w ! (s - 1)) i =
                (let j = (s - 1) * ?c + c_idx i in
                    if j < length u then u ! j else bl_tm M)"
            by (rule encode_input_nth[OF s_minus_1_lt])
          have j_ge: "(s - 1) * ?c + c_idx i ≥ length u"
            using p_gt by simp
          have ae_val: "(?w ! (s - 1)) i = bl_tm M"
            using nth_eq j_ge by (simp add: Let_def)
          have ae_lhs:
            "mt_tape (ae_init_config M ?w) k s i = (?w ! (s - 1)) i"
            unfolding ae_init_config_def using s_ge k_eq True kpos by simp
          show ?thesis using ae_lhs ae_val by simp
        qed
        show ?thesis using subst_bl ae_bl by simp
      next
        case True
        have p_le: "?p ≤ length u" using True .
        have subst_val:
          "mt_tape (init_config_mttm M u) k ?p
             = u ! ((s - 1) * ?c + c_idx i)"
          using MTTM k_eq p_pos p_le kpos by simp
        have c_pos: "?c > 0" using c_idx_lt_card[where x = i] by linarith
        have len_w: "length ?w = (length u + ?c - 1) div ?c"
          by (rule length_encode_input)
        have prod_lt: "(s - 1) * ?c < length u"
          using p_le by linarith
        have s_le_len_w: "s ≤ length ?w"
        proof -
          have s_times_c_eq: "s * ?c = (s - 1) * ?c + ?c"
            using s_ge by (auto simp: algebra_simps)
          have step: "s * ?c ≤ length u + ?c - 1"
            using prod_lt c_pos s_times_c_eq by linarith
          have s_div: "s * ?c div ?c = s" using c_pos by simp
          have "s = s * ?c div ?c" using s_div by simp
          also have "… ≤ (length u + ?c - 1) div ?c"
            using step by (rule div_le_mono)
          finally show ?thesis using len_w by simp
        qed
        have s_minus_1_lt: "s - 1 < length ?w"
          using s_le_len_w s_ge by simp
        have nth_eq:
          "(?w ! (s - 1)) i =
              (let j = (s - 1) * ?c + c_idx i in
                  if j < length u then u ! j else bl_tm M)"
          by (rule encode_input_nth[OF s_minus_1_lt])
        have j_lt: "(s - 1) * ?c + c_idx i < length u"
          using p_le by simp
        have ae_val: "(?w ! (s - 1)) i = u ! ((s - 1) * ?c + c_idx i)"
          using nth_eq j_lt by (simp add: Let_def)
        have ae_lhs:
          "mt_tape (ae_init_config M ?w) k s i = (?w ! (s - 1)) i"
          unfolding ae_init_config_def using s_ge k_eq s_le_len_w kpos
          by simp
        show ?thesis using subst_val ae_lhs ae_val by simp
      qed
    qed
  qed
qed

subsubsection ‹Validation post-state and step count›

text ‹Well-formed inputs (without ‹bl_block›) drive the validation
  chain to the explicit SS1 boundary configuration.  Extracted from
  the well-formed branch of ‹ae_validation_steps_bound› so that
  ‹ae_validation_post_state_canonical› can use the same chain to
  prove the simulation against the substrate's ‹init_config›
  (the steps-bound lemma's ‹obtains› form discards the explicit
  final config).

  This is the narrower companion of the general step-count form
  ‹ae_validation_phase_step_count› in theory
  ‹AlphabetEnlargement›: it gives the exact length
  ‹2 ⋅ |w| + 4› with SS1 as the only outcome under the
  stronger precondition ‹ae_input_well_formed (bl_tm M) w›,
  whereas the general form gives an existential bound
  ‹n ≤ 2 ⋅ |w| + f⇩v› with SS1-or-reject outcomes
  for any input (well-formed or not).  The linear-speedup proof
  uses this canonical form, applied via
  ‹encode_input_well_formed› to explicit encoder-image
  inputs.›
lemma ae_validation_well_formed_to_SS1:
  fixes M :: "('q, 'a) mttm"
    and w :: "('c :: enum ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and wf: "ae_input_well_formed (bl_tm M) w"
      and s_in_Q: "s_tm M ∈ Q_tm M"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  shows "(ae_init_config M w,
          Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                     init_dest, SS1)
                   (mt_tape (ae_init_config M w)) (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ (2 * length w + 4)"
proof -
  let ?init = "ae_init_config M w"
  let ?ts = "mt_tape ?init"
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have bt_all: "∀j≥k_tm M. ∀i. ?ts j i = bl_block (bl_tm M)"
    using ae_init_config_tape_blank_tail by blast
  have buf_gamma_init:
      "∀kk :: nat.
          fst (init_buffer (le_tm M) kk
                  :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
              ∈ gamma_block (Γ_tm M)
          ∧ fst (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)
          ∧ snd (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)"
    by (rule init_buffer_in_gamma_block_at_M[OF vM])
  have LE_neq_bl_block: "LE_block (le_tm M) ≠ bl_block (bl_tm M)"
    using le_neq_bl unfolding LE_block_def bl_block_def
    by (metis fun_eq_iff)
  have LE_notin: "LE_block (le_tm M) ∉ set w"
  proof -
    have le_notin: "le_tm M ∉ Sigma_tm M ∪ {bl_tm M}"
      using valid_mttm_LE_not_Sigma[OF vM] le_neq_bl by auto
    have "LE_block (le_tm M) ∉ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      using le_notin
      unfolding LE_block_def gamma_block_def by auto
    thus ?thesis using w_sub by auto
  qed
  ― ‹Determine whether all w-cells are pure or the last is padded.›
  have all_pure_or_last_padded:
    "(∀i < length w. is_pure_block (bl_tm M) (w ! i))
     ∨ (0 < length w
          ∧ (∀i < length w - 1. is_pure_block (bl_tm M) (w ! i))
          ∧ is_padded_block (bl_tm M) (w ! (length w - 1)))"
  proof (cases "length w = 0")
    case True
    thus ?thesis by simp
  next
    case False
    hence wpos: "0 < length w" by simp
    show ?thesis
    proof (cases "is_pure_block (bl_tm M) (w ! (length w - 1))")
      case True
      have "∀i < length w. is_pure_block (bl_tm M) (w ! i)"
      proof (intro allI impI)
        fix i assume i_lt: "i < length w"
        have "is_pure_block (bl_tm M) (w ! i)
              ∨ (i = length w - 1
                 ∧ is_padded_block (bl_tm M) (w ! i))"
          using wf i_lt unfolding ae_input_well_formed_def by auto
        thus "is_pure_block (bl_tm M) (w ! i)"
          using True by auto
      qed
      thus ?thesis by simp
    next
      case False
      have last_padded: "is_padded_block (bl_tm M) (w ! (length w - 1))"
      proof -
        have idx_lt: "length w - 1 < length w" using wpos by linarith
        have or_form: "is_pure_block (bl_tm M) (w ! (length w - 1))
              ∨ (length w - 1 = length w - 1
                 ∧ is_padded_block (bl_tm M) (w ! (length w - 1)))"
          using wf idx_lt unfolding ae_input_well_formed_def by blast
        thus ?thesis using False by auto
      qed
      have prefix_pure: "∀i < length w - 1. is_pure_block (bl_tm M) (w ! i)"
      proof (intro allI impI)
        fix i assume i_lt: "i < length w - 1"
        hence i_lt2: "i < length w" using wpos by linarith
        have "is_pure_block (bl_tm M) (w ! i)
              ∨ (i = length w - 1
                 ∧ is_padded_block (bl_tm M) (w ! i))"
          using wf i_lt2 unfolding ae_input_well_formed_def by auto
        thus "is_pure_block (bl_tm M) (w ! i)" using i_lt by auto
      qed
      show ?thesis using wpos prefix_pure last_padded by blast
    qed
  qed
  have tape_le: "?ts (0 :: nat) 0 = LE_block (le_tm M)"
    by (rule ae_init_config_tape_le[OF kpos])
  have gamma_all: "∀k i. ?ts k i ∈ gamma_block (Γ_tm M)"
    using ae_init_config_in_gamma_block[OF vM w_sub] by simp
  have stage_eq: "init_stage (le_tm M)
                  = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
    unfolding init_stage_def ..
  ― ‹Verify positions ‹1…Suc (length w)› on tape 0 are non-LE
      (from ‹LE_notin› for input positions; from
      ‹LE_neq_bl_block› for the blank tail).›
  have non_le: "∀i. 1 ≤ i ∧ i ≤ Suc (length w)
                     ⟶ ?ts 0 i ≠ LE_block (le_tm M)"
  proof (intro allI impI)
    fix i assume i_range: "1 ≤ i ∧ i ≤ Suc (length w)"
    have i_pos: "1 ≤ i" using i_range by simp
    consider (in_input) "i ≤ length w" | (past) "i = Suc (length w)"
      using i_range by linarith
    thus "?ts 0 i ≠ LE_block (le_tm M)"
    proof cases
      case in_input
      have eq: "?ts 0 i = w ! (i - 1)"
        using ae_init_config_tape_input[OF i_pos in_input kpos] by simp
      have "w ! (i - 1) ∈ set w" using i_pos in_input by auto
      thus ?thesis using LE_notin eq by auto
    next
      case past
      have ineq: "length w < i" using past by simp
      have eq: "?ts 0 i = bl_block (bl_tm M)"
        by (rule ae_init_config_tape_blank_after_input[OF ineq])
      have "LE_block (le_tm M) ≠ bl_block (bl_tm M)"
        by (rule LE_neq_bl_block)
      thus ?thesis using eq by force
    qed
  qed
  from all_pure_or_last_padded consider
      (all_pure) "∀i < length w. is_pure_block (bl_tm M) (w ! i)"
    | (last_padded) "0 < length w"
                     "∀i < length w - 1. is_pure_block (bl_tm M) (w ! i)"
                     "is_padded_block (bl_tm M) (w ! (length w - 1))"
    by blast
  thus ?thesis
  proof cases
    case all_pure
    let ?n_lwSS = "λi :: nat. if i = 0 then Suc (length w) else 0"
    have lw_le: "length w ≤ length w" by simp
    have sweep:
      "(?init,
          Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (length w)"
      by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                              s_neq_r lw_le all_pure])
    have lw_gt: "Suc (length w) > length w" by simp
    have read_bl: "?ts 0 (?n_lwSS 0) = bl_block (bl_tm M)"
      using ae_init_config_tape_blank_after_input[OF lw_gt] by simp
    have gamma_lwSS:
      "∀kk :: nat. ?ts kk (?n_lwSS kk) ∈ gamma_block (Γ_tm M)"
      using gamma_all by simp
    have step_to_ret:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwd) ?ts ?n_lwSS,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_fwd_to_ret[where ts = ?ts and n = ?n_lwSS,
            OF s_in_Q s_neq_t s_neq_r read_bl bt_all init_stage_tail
               gamma_lwSS buf_gamma_init])
    have step_to_ret_init:
      "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_lwSS,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M)"
      using step_to_ret unfolding stage_eq by simp
    have post_sweep:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc (length w))"
      by (rule relpow_Suc_I[OF sweep step_to_ret_init])
    have ret_arrow:
      "(∀i. 1 ≤ i ∧ i ≤ Suc (length w)
            ⟶ ?ts 0 i ≠ LE_block (le_tm M))
       ⟶ (Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VRet) ?ts ?n_lwSS,
            Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, SS1) ?ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc (length w))"
      by (rule ae_validation_ret_sweep[OF s_in_Q tape_le gamma_all
                                          buf_gamma_init bt_all init_stage_tail])
    have ret_chain:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ Suc (Suc (length w))"
      using ret_arrow non_le by (rule mp)
    have full_chain_pre:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ (Suc (Suc (length w)) + Suc (Suc (length w)))"
    proof -
      have comp:
        "(?init,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, SS1) ?ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc (length w))
              O mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc (length w))"
        using post_sweep ret_chain by (rule relcompI)
      thus ?thesis by (simp only: relpow_add)
    qed
    have total_eq:
      "Suc (Suc (length w)) + Suc (Suc (length w)) = 2 * length w + 4"
      by simp
    have full_chain:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ (2 * length w + 4)"
      using full_chain_pre unfolding total_eq .
    show ?thesis using full_chain .
  next
    case last_padded
    let ?lw = "length w"
    let ?lwm1 = "length w - 1"
    let ?n_lw = "λi :: nat. if i = 0 then ?lw else 0"
    let ?n_lwSS = "λi :: nat. if i = 0 then Suc ?lw else 0"
    have wpos: "0 < ?lw" using last_padded(1) .
    have m1_le: "?lwm1 ≤ ?lw" by simp
    have prefix_pure: "∀i < ?lwm1. is_pure_block (bl_tm M) (w ! i)"
      using last_padded(2) .
    have sweep:
      "(?init,
          Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                   (λi :: nat. if i = 0 then Suc ?lwm1 else 0))
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc ?lwm1"
      by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                              s_neq_r m1_le prefix_pure])
    have suc_m1_eq: "Suc ?lwm1 = ?lw" using wpos by simp
    have sweep_lw:
      "(?init,
          Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_lw)
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ ?lw"
      using sweep unfolding suc_m1_eq .
    have lw_pos: "1 ≤ ?lw" using wpos by linarith
    have lw_le: "?lw ≤ ?lw" by simp
    have read_at_lw_eq: "?ts 0 ?lw = w ! ?lwm1"
      using ae_init_config_tape_input[OF lw_pos lw_le kpos] by simp
    have read_padded:
      "is_padded_block (bl_tm M) (?ts 0 (?n_lw 0))"
      using read_at_lw_eq last_padded(3) by simp
    have gamma_lw:
      "∀kk :: nat. ?ts kk (?n_lw kk) ∈ gamma_block (Γ_tm M)"
      using gamma_all by simp
    have step_to_pad:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwd) ?ts ?n_lw,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts
                (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                               (?n_lw kk)))
          ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_fwd_to_padded[where ts = ?ts and n = ?n_lw,
            OF s_in_Q s_neq_t s_neq_r read_padded bt_all init_stage_tail
               gamma_lw buf_gamma_init])
    have post_eq_pad:
      "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n_lw kk))
       = ?n_lwSS"
      by (rule ext) simp
    have step_to_pad_norm:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwd) ?ts ?n_lw,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M)"
      using step_to_pad post_eq_pad by simp
    have step_to_pad_init:
      "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_lw,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M)"
      using step_to_pad_norm unfolding stage_eq by simp
    have lw_gt: "Suc ?lw > ?lw" by simp
    have read_bl_lwSS: "?ts 0 (?n_lwSS 0) = bl_block (bl_tm M)"
      using ae_init_config_tape_blank_after_input[OF lw_gt] by simp
    have gamma_lwSS:
      "∀kk :: nat. ?ts kk (?n_lwSS kk) ∈ gamma_block (Γ_tm M)"
      using gamma_all by simp
    have step_pad_to_ret:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_lwSS,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_pad_to_ret[where ts = ?ts and n = ?n_lwSS,
            OF s_in_Q read_bl_lwSS bt_all init_stage_tail
               gamma_lwSS buf_gamma_init])
    have chain_lw_to_VFwdPad:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc ?lw"
      by (rule relpow_Suc_I[OF sweep_lw step_to_pad_init])
    have chain_to_VRet:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS)
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc ?lw)"
      by (rule relpow_Suc_I[OF chain_lw_to_VFwdPad step_pad_to_ret])
    have ret_arrow:
      "(∀i. 1 ≤ i ∧ i ≤ Suc ?lw
            ⟶ ?ts 0 i ≠ LE_block (le_tm M))
       ⟶ (Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VRet) ?ts ?n_lwSS,
            Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, SS1) ?ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc ?lw)"
      by (rule ae_validation_ret_sweep[OF s_in_Q tape_le gamma_all
                                          buf_gamma_init bt_all init_stage_tail])
    have ret_chain:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VRet) ?ts ?n_lwSS,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ Suc (Suc ?lw)"
      using ret_arrow non_le by (rule mp)
    have full_chain_pre:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ (Suc (Suc ?lw) + Suc (Suc ?lw))"
    proof -
      have comp:
        "(?init,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, SS1) ?ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc ?lw)
              O mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc ?lw)"
        using chain_to_VRet ret_chain by (rule relcompI)
      thus ?thesis by (simp only: relpow_add)
    qed
    have total_eq:
      "Suc (Suc ?lw) + Suc (Suc ?lw) = 2 * ?lw + 4"
      by simp
    have full_chain:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ (2 * ?lw + 4)"
      using full_chain_pre unfolding total_eq .
    show ?thesis using full_chain .
  qed
qed

text ‹Every prefix of the validation run carries a ∗‹marker›
  witness: a config reachable in exactly ‹i› steps whose stage index
  is one of ‹VFwd› / ‹VFwdPad› / ‹VRet› (i.e.\ still inside the
  validation sweep, not yet at ‹SS1› nor rejected), for every
  ‹i < 2 * length w + 4›.  Forward witnesses for ‹i ≤ length w›
  come from ‹ae_validation_fwd_sweep_pure› at parameter ‹i - 1›;
  the boundary slot ‹i = Suc (length w)› is ‹VFwd› (all-pure) or
  ‹VFwdPad› (last-padded); return witnesses come from the partial
  return sweep.  This is the witness half of the prefix-uniqueness
  argument in ‹ae_validation_prefix_markers›.›

lemma ae_validation_prefix_witnesses:
  fixes M :: "('q, 'a) mttm"
    and w :: "('c :: enum ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and wf: "ae_input_well_formed (bl_tm M) w"
      and s_in_Q: "s_tm M ∈ Q_tm M"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  shows "∀i<2 * length w + 4. ∃d.
            (ae_init_config M w, d)
                ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
              ∧ snd (snd (snd (snd (mt_state d))))
                    ∈ {VFwd, VFwdPad, VRet}"
proof -
  let ?init = "ae_init_config M w"
  let ?ts = "mt_tape ?init"
  let ?R = "mttm_step (alphabet_enlarge_delta M)"
  let ?lw = "length w"
  let ?vfwd = "λh :: nat. Config⇩M (s_tm M, init_offset,
                  init_buffer (le_tm M), init_dest, VFwd) ?ts
                  (λi :: nat. if i = 0 then h else 0)"
  let ?vret = "λh :: nat. Config⇩M (s_tm M, init_offset,
                  init_buffer (le_tm M), init_dest, VRet) ?ts
                  (λi :: nat. if i = 0 then h else 0)"
  let ?vpad = "λh :: nat. Config⇩M (s_tm M, init_offset,
                  init_buffer (le_tm M), init_dest, VFwdPad) ?ts
                  (λi :: nat. if i = 0 then h else 0)"
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have bt_all: "∀j≥k_tm M. ∀i. ?ts j i = bl_block (bl_tm M)"
    using ae_init_config_tape_blank_tail by blast
  have buf_gamma_init:
      "∀kk :: nat.
          fst (init_buffer (le_tm M) kk
                  :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
              ∈ gamma_block (Γ_tm M)
          ∧ fst (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)
          ∧ snd (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)"
    by (rule init_buffer_in_gamma_block_at_M[OF vM])
  have LE_neq_bl_block: "LE_block (le_tm M) ≠ bl_block (bl_tm M)"
    using le_neq_bl unfolding LE_block_def bl_block_def
    by (metis fun_eq_iff)
  have LE_notin: "LE_block (le_tm M) ∉ set w"
  proof -
    have le_notin: "le_tm M ∉ Sigma_tm M ∪ {bl_tm M}"
      using valid_mttm_LE_not_Sigma[OF vM] le_neq_bl by auto
    have "LE_block (le_tm M) ∉ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      using le_notin unfolding LE_block_def gamma_block_def by auto
    thus ?thesis using w_sub by auto
  qed
  have tape_le: "?ts (0 :: nat) 0 = LE_block (le_tm M)"
    by (rule ae_init_config_tape_le[OF kpos])
  have gamma_all: "∀k i. ?ts k i ∈ gamma_block (Γ_tm M)"
    using ae_init_config_in_gamma_block[OF vM w_sub] by simp
  have stage_eq: "init_stage (le_tm M)
                  = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
    unfolding init_stage_def ..
  have non_le_Slw: "∀i. 1 ≤ i ∧ i ≤ Suc ?lw
                       ⟶ ?ts 0 i ≠ LE_block (le_tm M)"
  proof (intro allI impI)
    fix i assume i_range: "1 ≤ i ∧ i ≤ Suc ?lw"
    have i_pos: "1 ≤ i" using i_range by simp
    consider (in_input) "i ≤ ?lw" | (past) "i = Suc ?lw"
      using i_range by linarith
    thus "?ts 0 i ≠ LE_block (le_tm M)"
    proof cases
      case in_input
      have eq: "?ts 0 i = w ! (i - 1)"
        using ae_init_config_tape_input[OF i_pos in_input kpos] by simp
      have "w ! (i - 1) ∈ set w" using i_pos in_input by auto
      thus ?thesis using LE_notin eq by auto
    next
      case past
      have ineq: "?lw < i" using past by simp
      have eq: "?ts 0 i = bl_block (bl_tm M)"
        by (rule ae_init_config_tape_blank_after_input[OF ineq])
      thus ?thesis using LE_neq_bl_block by force
    qed
  qed
  ― ‹Forward witnesses for ‹i ≤ length w›, uniformly (the
      pure-prefix ‹∀j < i-1› holds for any well-formed input).›
  have vfwd_wit: "⋀i. i ≤ ?lw ⟹ (?init, ?vfwd i) ∈ ?R ^^ i"
  proof -
    fix i assume i_le: "i ≤ ?lw"
    show "(?init, ?vfwd i) ∈ ?R ^^ i"
    proof (cases "i = 0")
      case True
      have head0: "(λi :: nat. if i = 0 then 0 else (0 :: nat)) = (λ_. 0)"
        by simp
      have eq0: "?vfwd 0 = ?init"
        unfolding ae_init_config_def init_stage_def head0 by simp
      have "(?init, ?vfwd 0) ∈ ?R ^^ 0" using eq0 relpow_0_I by metis
      thus ?thesis unfolding True .
    next
      case False
      hence i_pos: "1 ≤ i" by simp
      have k_le: "i - 1 ≤ ?lw" using i_le by simp
      have pure_short: "∀j < i - 1. is_pure_block (bl_tm M) (w ! j)"
      proof (intro allI impI)
        fix j assume j_lt: "j < i - 1"
        have j_lt_lw: "j < ?lw" using j_lt i_le by linarith
        have j_neq: "j ≠ ?lw - 1" using j_lt i_le by linarith
        have "is_pure_block (bl_tm M) (w ! j)
              ∨ (j = ?lw - 1 ∧ is_padded_block (bl_tm M) (w ! j))"
          using wf j_lt_lw unfolding ae_input_well_formed_def by auto
        thus "is_pure_block (bl_tm M) (w ! j)" using j_neq by auto
      qed
      have sweep:
        "(?init, Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                          (λj :: nat. if j = 0 then Suc (i - 1) else 0))
            ∈ ?R ^^ Suc (i - 1)"
        by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                                s_neq_r k_le pure_short])
      have suci: "Suc (i - 1) = i" using i_pos by simp
      show ?thesis using sweep unfolding suci stage_eq by simp
    qed
  qed
  ― ‹Classify the input: all blocks pure, or the last padded.›
  have all_pure_or_last_padded:
    "(∀i < ?lw. is_pure_block (bl_tm M) (w ! i))
     ∨ (0 < ?lw
          ∧ (∀i < ?lw - 1. is_pure_block (bl_tm M) (w ! i))
          ∧ is_padded_block (bl_tm M) (w ! (?lw - 1)))"
  proof (cases "?lw = 0")
    case True thus ?thesis by simp
  next
    case False
    hence wpos: "0 < ?lw" by simp
    show ?thesis
    proof (cases "is_pure_block (bl_tm M) (w ! (?lw - 1))")
      case True
      have "∀i < ?lw. is_pure_block (bl_tm M) (w ! i)"
      proof (intro allI impI)
        fix i assume i_lt: "i < ?lw"
        have "is_pure_block (bl_tm M) (w ! i)
              ∨ (i = ?lw - 1 ∧ is_padded_block (bl_tm M) (w ! i))"
          using wf i_lt unfolding ae_input_well_formed_def by auto
        thus "is_pure_block (bl_tm M) (w ! i)" using True by auto
      qed
      thus ?thesis by simp
    next
      case False
      have last_padded: "is_padded_block (bl_tm M) (w ! (?lw - 1))"
      proof -
        have idx_lt: "?lw - 1 < ?lw" using wpos by linarith
        have "is_pure_block (bl_tm M) (w ! (?lw - 1))
              ∨ (?lw - 1 = ?lw - 1
                 ∧ is_padded_block (bl_tm M) (w ! (?lw - 1)))"
          using wf idx_lt unfolding ae_input_well_formed_def by blast
        thus ?thesis using False by auto
      qed
      have prefix_pure: "∀i < ?lw - 1. is_pure_block (bl_tm M) (w ! i)"
      proof (intro allI impI)
        fix i assume i_lt: "i < ?lw - 1"
        hence i_lt2: "i < ?lw" using wpos by linarith
        have "is_pure_block (bl_tm M) (w ! i)
              ∨ (i = ?lw - 1 ∧ is_padded_block (bl_tm M) (w ! i))"
          using wf i_lt2 unfolding ae_input_well_formed_def by auto
        thus "is_pure_block (bl_tm M) (w ! i)" using i_lt by auto
      qed
      show ?thesis using wpos prefix_pure last_padded by blast
    qed
  qed
  ― ‹Boundary witness at step ‹Suc (length w)›: ‹VFwd› head
      ‹Suc lw› (all-pure) or ‹VFwdPad› head ‹Suc lw› (last-padded).›
  have boundary_wit: "∃d. (?init, d) ∈ ?R ^^ Suc ?lw
            ∧ snd (snd (snd (snd (mt_state d)))) ∈ {VFwd, VFwdPad, VRet}"
  proof -
    from all_pure_or_last_padded consider
        (all_pure) "∀i < ?lw. is_pure_block (bl_tm M) (w ! i)"
      | (last_padded) "0 < ?lw"
                       "∀i < ?lw - 1. is_pure_block (bl_tm M) (w ! i)"
                       "is_padded_block (bl_tm M) (w ! (?lw - 1))"
      by blast
    thus ?thesis
    proof cases
      case all_pure
      have lw_le: "?lw ≤ ?lw" by simp
      have sweep:
        "(?init, Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                          (λi :: nat. if i = 0 then Suc ?lw else 0))
            ∈ ?R ^^ Suc ?lw"
        by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                                s_neq_r lw_le all_pure])
      have reach: "(?init, ?vfwd (Suc ?lw)) ∈ ?R ^^ Suc ?lw"
        using sweep unfolding stage_eq by simp
      have "snd (snd (snd (snd (mt_state (?vfwd (Suc ?lw))))))
              ∈ {VFwd, VFwdPad, VRet}" by simp
      thus ?thesis using reach by blast
    next
      case last_padded
      let ?n_lw = "λi :: nat. if i = 0 then ?lw else 0"
      have wpos: "0 < ?lw" using last_padded(1) .
      have m1_le: "?lw - 1 ≤ ?lw" by simp
      have sweep:
        "(?init, Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                   (λi :: nat. if i = 0 then Suc (?lw - 1) else 0))
            ∈ ?R ^^ Suc (?lw - 1)"
        by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                                s_neq_r m1_le last_padded(2)])
      have suc_m1_eq: "Suc (?lw - 1) = ?lw" using wpos by simp
      have sweep_lw: "(?init, ?vfwd ?lw) ∈ ?R ^^ ?lw"
        using sweep unfolding suc_m1_eq stage_eq by simp
      have lw_pos: "1 ≤ ?lw" using wpos by linarith
      have lw_le: "?lw ≤ ?lw" by simp
      have read_at_lw_eq: "?ts 0 ?lw = w ! (?lw - 1)"
        using ae_init_config_tape_input[OF lw_pos lw_le kpos] by simp
      have read_padded: "is_padded_block (bl_tm M) (?ts 0 (?n_lw 0))"
        using read_at_lw_eq last_padded(3) by simp
      have gamma_lw: "∀kk :: nat. ?ts kk (?n_lw kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_to_pad:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwd) ?ts ?n_lw,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwdPad) ?ts
                  (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                                 (?n_lw kk)))
            ∈ ?R"
        by (rule ae_step_val_fwd_to_padded[where ts = ?ts and n = ?n_lw,
              OF s_in_Q s_neq_t s_neq_r read_padded bt_all init_stage_tail
                 gamma_lw buf_gamma_init])
      have post_eq_pad:
        "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n_lw kk))
         = (λi :: nat. if i = 0 then Suc ?lw else 0)"
        by (rule ext) simp
      have step_to_pad_norm: "(?vfwd ?lw, ?vpad (Suc ?lw)) ∈ ?R"
        using step_to_pad post_eq_pad by simp
      have reach: "(?init, ?vpad (Suc ?lw)) ∈ ?R ^^ Suc ?lw"
        by (rule relpow_Suc_I[OF sweep_lw step_to_pad_norm])
      have "snd (snd (snd (snd (mt_state (?vpad (Suc ?lw))))))
              ∈ {VFwd, VFwdPad, VRet}" by simp
      thus ?thesis using reach by blast
    qed
  qed
  ― ‹Pivot witness into ‹VRet› at head ‹Suc lw›, reached in
      ‹Suc (Suc lw)› steps (both classification cases).›
  have to_VRet: "(?init, ?vret (Suc ?lw)) ∈ ?R ^^ Suc (Suc ?lw)"
  proof -
    from all_pure_or_last_padded consider
        (all_pure) "∀i < ?lw. is_pure_block (bl_tm M) (w ! i)"
      | (last_padded) "0 < ?lw"
                       "∀i < ?lw - 1. is_pure_block (bl_tm M) (w ! i)"
                       "is_padded_block (bl_tm M) (w ! (?lw - 1))"
      by blast
    thus ?thesis
    proof cases
      case all_pure
      let ?n_Slw = "λi :: nat. if i = 0 then Suc ?lw else 0"
      have lw_le: "?lw ≤ ?lw" by simp
      have sweep: "(?init, ?vfwd (Suc ?lw)) ∈ ?R ^^ Suc ?lw"
        using ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                  s_neq_r lw_le all_pure] unfolding stage_eq by simp
      have lw_gt: "Suc ?lw > ?lw" by simp
      have read_bl: "?ts 0 (?n_Slw 0) = bl_block (bl_tm M)"
        using ae_init_config_tape_blank_after_input[OF lw_gt] by simp
      have gamma_Slw: "∀kk :: nat. ?ts kk (?n_Slw kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_to_ret: "(?vfwd (Suc ?lw), ?vret (Suc ?lw)) ∈ ?R"
        by (rule ae_step_val_fwd_to_ret[where ts = ?ts and n = ?n_Slw,
              OF s_in_Q s_neq_t s_neq_r read_bl bt_all init_stage_tail
                 gamma_Slw buf_gamma_init])
      show ?thesis by (rule relpow_Suc_I[OF sweep step_to_ret])
    next
      case last_padded
      let ?n_lw = "λi :: nat. if i = 0 then ?lw else 0"
      let ?n_Slw = "λi :: nat. if i = 0 then Suc ?lw else 0"
      have wpos: "0 < ?lw" using last_padded(1) .
      have m1_le: "?lw - 1 ≤ ?lw" by simp
      have sweep:
        "(?init, Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                   (λi :: nat. if i = 0 then Suc (?lw - 1) else 0))
            ∈ ?R ^^ Suc (?lw - 1)"
        by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                                s_neq_r m1_le last_padded(2)])
      have suc_m1_eq: "Suc (?lw - 1) = ?lw" using wpos by simp
      have sweep_lw: "(?init, ?vfwd ?lw) ∈ ?R ^^ ?lw"
        using sweep unfolding suc_m1_eq stage_eq by simp
      have lw_pos: "1 ≤ ?lw" using wpos by linarith
      have lw_le: "?lw ≤ ?lw" by simp
      have read_at_lw_eq: "?ts 0 ?lw = w ! (?lw - 1)"
        using ae_init_config_tape_input[OF lw_pos lw_le kpos] by simp
      have read_padded: "is_padded_block (bl_tm M) (?ts 0 (?n_lw 0))"
        using read_at_lw_eq last_padded(3) by simp
      have gamma_lw: "∀kk :: nat. ?ts kk (?n_lw kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_to_pad:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwd) ?ts ?n_lw,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwdPad) ?ts
                  (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                                 (?n_lw kk)))
            ∈ ?R"
        by (rule ae_step_val_fwd_to_padded[where ts = ?ts and n = ?n_lw,
              OF s_in_Q s_neq_t s_neq_r read_padded bt_all init_stage_tail
                 gamma_lw buf_gamma_init])
      have post_eq_pad:
        "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n_lw kk))
         = ?n_Slw"
        by (rule ext) simp
      have step_to_pad_norm: "(?vfwd ?lw, ?vpad (Suc ?lw)) ∈ ?R"
        using step_to_pad post_eq_pad by simp
      have chain_lw_to_VFwdPad: "(?init, ?vpad (Suc ?lw)) ∈ ?R ^^ Suc ?lw"
        by (rule relpow_Suc_I[OF sweep_lw step_to_pad_norm])
      have read_bl_Slw: "?ts 0 (?n_Slw 0) = bl_block (bl_tm M)"
        using ae_init_config_tape_blank_after_input[OF lessI] by simp
      have gamma_Slw: "∀kk :: nat. ?ts kk (?n_Slw kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_pad_to_ret: "(?vpad (Suc ?lw), ?vret (Suc ?lw)) ∈ ?R"
        by (rule ae_step_val_pad_to_ret[where ts = ?ts and n = ?n_Slw,
              OF s_in_Q read_bl_Slw bt_all init_stage_tail
                 gamma_Slw buf_gamma_init])
      show ?thesis
        by (rule relpow_Suc_I[OF chain_lw_to_VFwdPad step_pad_to_ret])
    qed
  qed
  ― ‹Return witnesses: ‹m› leftward steps from the pivot reach
      ‹VRet› head ‹Suc lw - m› in ‹Suc (Suc lw) + m› steps.›
  have ret_reach: "⋀m. m ≤ Suc ?lw
            ⟹ (?init, ?vret (Suc ?lw - m)) ∈ ?R ^^ (Suc (Suc ?lw) + m)"
  proof -
    fix m assume mle: "m ≤ Suc ?lw"
    have rp: "(?vret (Suc ?lw), ?vret (Suc ?lw - m)) ∈ ?R ^^ m"
      by (rule mp[OF ae_validation_ret_partial[OF s_in_Q gamma_all
            buf_gamma_init bt_all init_stage_tail non_le_Slw] mle])
    have "(?init, ?vret (Suc ?lw - m)) ∈ ?R ^^ Suc (Suc ?lw) O ?R ^^ m"
      using to_VRet rp by (rule relcompI)
    thus "(?init, ?vret (Suc ?lw - m)) ∈ ?R ^^ (Suc (Suc ?lw) + m)"
      by (simp only: relpow_add)
  qed
  ― ‹Assemble: each step ‹i < 2 lw + 4› falls in the forward,
      boundary, or return region.›
  show ?thesis
  proof (intro allI impI)
    fix i :: nat assume i_lt: "i < 2 * ?lw + 4"
    consider (fwd) "i ≤ ?lw" | (bd) "i = Suc ?lw" | (ret) "Suc ?lw < i"
      by linarith
    thus "∃d. (?init, d) ∈ ?R ^^ i
              ∧ snd (snd (snd (snd (mt_state d)))) ∈ {VFwd, VFwdPad, VRet}"
    proof cases
      case fwd
      have "(?init, ?vfwd i) ∈ ?R ^^ i" by (rule vfwd_wit[OF fwd])
      moreover have "snd (snd (snd (snd (mt_state (?vfwd i)))))
                       ∈ {VFwd, VFwdPad, VRet}" by simp
      ultimately show ?thesis by blast
    next
      case bd
      show ?thesis using boundary_wit unfolding bd by blast
    next
      case ret
      define m where "m = i - Suc (Suc ?lw)"
      have i_ge: "Suc (Suc ?lw) ≤ i" using ret by simp
      have m_le: "m ≤ Suc ?lw" using i_lt m_def by simp
      have i_eq: "Suc (Suc ?lw) + m = i" using i_ge m_def by simp
      have "(?init, ?vret (Suc ?lw - m)) ∈ ?R ^^ i"
        using ret_reach[OF m_le] unfolding i_eq .
      moreover have "snd (snd (snd (snd (mt_state (?vret (Suc ?lw - m))))))
                       ∈ {VFwd, VFwdPad, VRet}" by simp
      ultimately show ?thesis by blast
    qed
  qed
qed

text ‹Prefix uniqueness: every config reachable from ‹ae_init_config›
  in ‹i < 2 * length w + 4› steps is a validation marker (stage index
  ‹VFwd› / ‹VFwdPad› / ‹VRet›).  This is the invariant the relpow
  validation-functional needs, and is ∗‹det-free›: the validation
  sweep is functional regardless of ‹M›'s (non)determinism, since the
  only nondeterministic substep of ‹alphabet_enlarge_delta› (the
  ‹SS4›-to-‹SS5› transition) is never reached before ‹SS1›.  Proof:
  strong induction on ‹i›;
  the induction hypothesis supplies the relpow-functional's invariant
  premise, so the arbitrary reachable ‹d› is forced equal to the
  marker witness exhibited by ‹ae_validation_prefix_witnesses›.›

lemma ae_validation_prefix_markers:
  fixes M :: "('q, 'a) mttm"
    and w :: "('c :: enum ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and wf: "ae_input_well_formed (bl_tm M) w"
      and s_in_Q: "s_tm M ∈ Q_tm M"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  shows "∀i<2 * length w + 4. ∀d.
            (ae_init_config M w, d)
                ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
              ⟶ snd (snd (snd (snd (mt_state d))))
                    ∈ {VFwd, VFwdPad, VRet}"
proof -
  let ?init = "ae_init_config M w"
  let ?R = "mttm_step (alphabet_enlarge_delta M)"
  let ?n_val = "2 * length w + 4"
  have wit: "∀i<?n_val. ∃d. (?init, d) ∈ ?R ^^ i
              ∧ snd (snd (snd (snd (mt_state d)))) ∈ {VFwd, VFwdPad, VRet}"
    by (rule ae_validation_prefix_witnesses[OF vM w_sub wf s_in_Q
                                              s_neq_t s_neq_r le_neq_bl])
  have main: "∀i0. i0 < ?n_val
                ⟶ (∀d. (?init, d) ∈ ?R ^^ i0
                          ⟶ snd (snd (snd (snd (mt_state d))))
                                ∈ {VFwd, VFwdPad, VRet})"
  proof (rule allI)
    fix i1 :: nat
    show "i1 < ?n_val
            ⟶ (∀d. (?init, d) ∈ ?R ^^ i1
                  ⟶ snd (snd (snd (snd (mt_state d))))
                        ∈ {VFwd, VFwdPad, VRet})"
    proof (induction i1 rule: less_induct)
      case (less i)
      show ?case
      proof (rule impI)
        assume i_lt: "i < ?n_val"
        show "∀d. (?init, d) ∈ ?R ^^ i
                    ⟶ snd (snd (snd (snd (mt_state d))))
                          ∈ {VFwd, VFwdPad, VRet}"
        proof (intro allI impI)
          fix d assume reach: "(?init, d) ∈ ?R ^^ i"
          have inv: "∀j<i. ∀d'. (?init, d') ∈ ?R ^^ j
                      ⟶ snd (snd (snd (snd (mt_state d'))))
                            ∈ {VFwd, VFwdPad, VRet}"
          proof (intro allI impI)
            fix j d' assume j_lt: "j < i" and reach': "(?init, d') ∈ ?R ^^ j"
            have "j < ?n_val" using j_lt i_lt by simp
            thus "snd (snd (snd (snd (mt_state d')))) ∈ {VFwd, VFwdPad, VRet}"
              using less.IH[OF j_lt] reach' by blast
          qed
          obtain wd where wreach: "(?init, wd) ∈ ?R ^^ i"
            and wmark: "snd (snd (snd (snd (mt_state wd)))) ∈ {VFwd, VFwdPad, VRet}"
            using wit i_lt by blast
          have "d = wd"
            by (rule mttm_step_alphabet_enlarge_val_relpow_functional
                       [OF le_neq_bl reach wreach inv])
          thus "snd (snd (snd (snd (mt_state d)))) ∈ {VFwd, VFwdPad, VRet}"
            using wmark by simp
        qed
      qed
    qed
  qed
  show ?thesis using main by blast
qed

lemma ae_validation_post_state_canonical:
  fixes M :: "('q, 'a) mttm"
    and u :: "'a list"
  assumes vM: "valid_mttm M"
      and u_sub: "set u ⊆ Sigma_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  obtains n :: nat and c' where
      "(ae_init_config M (encode_input (bl_tm M) u), c')
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and "ae_simulates M
            (init_config_mttm M u)
            (c' :: ('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config)"
    and "ae_buffer_in_gamma_block M c'"
    and "∀kk<k_tm M. mt_tape c' kk 0 = LE_block (le_tm M)"
    and "∀i<n. ∀d :: ('c :: enum ⇒ 'a,
                          'q × ('a, 'c) ae_stage) mt_config.
            (ae_init_config M (encode_input (bl_tm M) u), d)
                ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
              ⟶ snd (snd (snd (snd (mt_state d))))
                    ∈ {VFwd, VFwdPad, VRet}"
proof -
  let ?w = "encode_input (bl_tm M) u :: ('c :: enum ⇒ 'a) list"
  let ?init = "ae_init_config M ?w"
  let ?subst_init = "init_config_mttm M u :: ('a, 'q) mt_config"
  have w_sub: "set ?w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
    by (rule encode_input_in_gamma_block[OF u_sub])
  have wf: "ae_input_well_formed (bl_tm M) ?w"
    by (rule encode_input_well_formed[OF vM u_sub])
  have s_in_Q: "s_tm M ∈ Q_tm M" by (rule s_tm_in_Q_tm[OF vM])
  ― ‹Tape correspondence is shared across the s-degenerate and
      s-nondegenerate cases (the chain doesn't modify the tape).›
  have tape_corr:
    "∀k<k_tm M. ae_tape_correspondence (le_tm M)
            (mt_tape ?subst_init k) (mt_tape ?init k)"
    by (rule ae_tape_correspondence_init[OF vM u_sub])
  ― ‹Gamma-block invariant on the M'-tape: also shared across
      both cases since the validation chain in the nondegen case
      reuses ‹mt_tape ?init› verbatim (no writes).›
  have gamma_block_init: "ae_tape_in_gamma_block M ?init"
    unfolding ae_tape_in_gamma_block_def
  proof (intro conjI)
    show "∀k p. mt_tape ?init k p ∈ gamma_block (Γ_tm M)"
      using ae_init_config_in_gamma_block[OF vM w_sub] by simp
  next
    show "∀j≥k_tm M. ∀p. mt_tape ?init j p = bl_block (bl_tm M)"
      using ae_init_config_tape_blank_tail by blast
  qed
  ― ‹Position correspondence: substrate's ‹n_M k = 0›; ae's
      ‹n_M' k = 0›; ‹ae_decode_pos 0 _ = 0›.›
  have ae_pos_zero: "∀k. mt_pos ?init k = 0"
    unfolding ae_init_config_def by simp
  have subst_pos_zero: "∀k. mt_pos ?subst_init k = 0"
    by (cases M) simp
  have pos_corr_init:
    "∀k. mt_pos ?subst_init k
            = ae_decode_pos (mt_pos ?init k) ((init_offset :: nat ⇒ 'c) k)"
    using ae_pos_zero subst_pos_zero
    unfolding ae_decode_pos_def by simp
  consider (degen) "s_tm M = t_tm M ∨ s_tm M = r_tm M"
         | (nondegen) "s_tm M ≠ t_tm M ∧ s_tm M ≠ r_tm M"
    by blast
  thus ?thesis
  proof cases
    case degen
    ― ‹‹n = 0›: chain is reflexive; simulation's halt-branch fires.›
    have chain_0:
      "(?init, ?init) ∈ mttm_step (alphabet_enlarge_delta M) ^^ 0"
      by simp
    have qM_subst: "mt_state ?subst_init = s_tm M"
      by (cases M) simp
    have init_state:
      "mt_state ?init = (s_tm M, init_offset,
                          init_buffer (le_tm M), init_dest, VFwd)"
      unfolding ae_init_config_def init_stage_def by simp
    have simulation: "ae_simulates M ?subst_init ?init"
      unfolding ae_simulates_def Let_def init_state init_stage_def
      using qM_subst tape_corr pos_corr_init degen gamma_block_init by simp
    ― ‹‹buf_gamma›: ‹?init›'s state buffer is ‹init_buffer (le_tm M)›,
        which is constant ‹LE_block (le_tm M)› in every slot;
        ‹init_buffer_in_gamma_block_at_M› discharges.›
    have buf_gamma_init: "ae_buffer_in_gamma_block M ?init"
      unfolding ae_buffer_in_gamma_block_def init_state init_stage_def
      using init_buffer_in_gamma_block_at_M[OF vM] by simp
    ― ‹‹le_anchor›: position 0 of every M'-tape is ‹LE_block (le_tm M)›
        by ‹ae_init_config_def›.›
    have le_anchor_init:
        "∀kk<k_tm M. mt_tape ?init kk 0 = LE_block (le_tm M)"
      by (auto intro: ae_init_config_tape_le)
    ― ‹‹n = 0›, so the prefix-marker clause is vacuous.›
    have markers_0:
      "∀i<(0 :: nat). ∀d.
          (?init, d) ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
            ⟶ snd (snd (snd (snd (mt_state d)))) ∈ {VFwd, VFwdPad, VRet}"
      by simp
    show ?thesis
      using chain_0 simulation buf_gamma_init le_anchor_init markers_0
      by (rule that)
  next
    case nondegen
    ― ‹Build SS1-landing chain via helper; simulation's SS1-branch
        fires.›
    have s_neq_t: "s_tm M ≠ t_tm M" using nondegen by simp
    have s_neq_r: "s_tm M ≠ r_tm M" using nondegen by simp
    let ?c' = "Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                          init_dest, SS1)
                       (mt_tape ?init) (λ_ :: nat. (0 :: nat))
                  :: ('c ⇒ 'a, 'q × ('a, 'c) ae_stage) mt_config"
    have chain:
      "(?init, ?c') ∈ mttm_step (alphabet_enlarge_delta M)
                        ^^ (2 * length ?w + 4)"
      by (rule ae_validation_well_formed_to_SS1[OF vM w_sub wf
            s_in_Q s_neq_t s_neq_r le_neq_bl])
    have qM_subst: "mt_state ?subst_init = s_tm M"
      by (cases M) simp
    have c'_state:
      "mt_state ?c' = (s_tm M, init_offset,
                          init_buffer (le_tm M), init_dest, SS1)"
      by simp
    have pos_corr_c':
      "∀k. mt_pos ?subst_init k
              = ae_decode_pos (mt_pos ?c' k)
                              ((init_offset :: nat ⇒ 'c) k)"
      using subst_pos_zero by (simp add: ae_decode_pos_def)
    have gamma_block_c': "ae_tape_in_gamma_block M ?c'"
      unfolding ae_tape_in_gamma_block_def
      using gamma_block_init unfolding ae_tape_in_gamma_block_def
      by simp
    have simulation: "ae_simulates M ?subst_init ?c'"
      unfolding ae_simulates_def Let_def c'_state
      using qM_subst tape_corr pos_corr_c' gamma_block_c'
            s_neq_t s_neq_r by simp
    ― ‹‹buf_gamma›: SS1-landing config still carries the canonical
        ‹init_buffer (le_tm M)›; ‹init_buffer_in_gamma_block_at_M›
        discharges as in the degen case.›
    have buf_gamma_c': "ae_buffer_in_gamma_block M ?c'"
      unfolding ae_buffer_in_gamma_block_def
      using init_buffer_in_gamma_block_at_M[OF vM] by simp
    ― ‹‹le_anchor›: the SS1-landing config's tape equals
        ‹mt_tape ?init› verbatim (validation does not write the
        M'-tape); position 0 inherits ‹LE_block (le_tm M)› from
        ‹ae_init_config_tape_le›.›
    have le_anchor_c':
        "∀kk<k_tm M. mt_tape ?c' kk 0 = LE_block (le_tm M)"
      by (auto intro: ae_init_config_tape_le)
    ― ‹The validation prefix is uniquely a marker run (det-free).›
    have markers:
      "∀i<2 * length ?w + 4. ∀d.
          (?init, d) ∈ mttm_step (alphabet_enlarge_delta M) ^^ i
            ⟶ snd (snd (snd (snd (mt_state d)))) ∈ {VFwd, VFwdPad, VRet}"
      by (rule ae_validation_prefix_markers[OF vM w_sub wf s_in_Q
            s_neq_t s_neq_r le_neq_bl])
    show ?thesis
      using chain simulation buf_gamma_c' le_anchor_c' markers
      by (rule that)
  qed
qed

text ‹Noncanonical inputs reject.  The ‹bl_block bl_M ∉ set w›
  hypothesis matches ‹M'›'s input alphabet ‹Σ'›
  (‹Σ' = gamma_block (Σ_M ∪ {bl_M}) - {bl_block, LE_block}›).
  Without it, e.g.\ ‹w = [bl_block bl_M]›
  triggers ‹ae_delta_val_fwd_to_ret› at the first input
  block, mistaking it for end-of-input — validation passes
  rather than rejecting, falsifying the lemma as previously
  stated.  ‹LE_block le_M ∉ set w› follows already from
  ‹set w ⊆ gamma_block (Σ_M ∪ {bl_M})› plus
  ‹le_M ∉ Σ_M ∪ {bl_M}›, so it need not be assumed
  separately.›

lemma ae_validation_post_state_noncanonical:
  fixes M :: "('q, 'a) mttm"
    and w :: "(('c :: enum) ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and bl_notin: "bl_block (bl_tm M) ∉ set w"
      and w_bad: "¬ ae_input_well_formed (bl_tm M) w"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
  obtains n :: nat and c' where
      "n ≤ length w + 2"
    and "(ae_init_config M w, c')
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and "case mt_state c' of (qM', _, _, _, _) ⇒ qM' = r_tm M"
proof -
  let ?init = "ae_init_config M w"
  let ?ts = "mt_tape ?init"
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have bt_all: "∀j≥k_tm M. ∀i. ?ts j i = bl_block (bl_tm M)"
    using ae_init_config_tape_blank_tail by blast
  have buf_gamma_init:
      "∀kk :: nat.
          fst (init_buffer (le_tm M) kk
                  :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
              ∈ gamma_block (Γ_tm M)
          ∧ fst (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)
          ∧ snd (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)"
    by (rule init_buffer_in_gamma_block_at_M[OF vM])
  have s_in_Q: "s_tm M ∈ Q_tm M" by (rule s_tm_in_Q_tm[OF vM])
  from w_bad have failure_exists:
    "∃s'. s' < length w
          ∧ ¬ is_pure_block (bl_tm M) (w ! s')
          ∧ ¬ (s' = length w - 1
               ∧ is_padded_block (bl_tm M) (w ! s'))"
    unfolding ae_input_well_formed_def by auto
  define P where
    "P = (λs'. s' < length w
               ∧ ¬ is_pure_block (bl_tm M) (w ! s')
               ∧ ¬ (s' = length w - 1
                    ∧ is_padded_block (bl_tm M) (w ! s')))"
  define s where "s = (LEAST s'. P s')"
  have failure_exists_P: "∃s'. P s'"
    using failure_exists unfolding P_def by simp
  from failure_exists_P have P_s: "P s"
    unfolding s_def by (rule LeastI_ex)
  have s_lt: "s < length w" using P_s unfolding P_def by simp
  have w_pos: "0 < length w" using s_lt by linarith
  have s_not_pure: "¬ is_pure_block (bl_tm M) (w ! s)"
    using P_s unfolding P_def by simp
  have s_not_last_padded:
    "¬ (s = length w - 1 ∧ is_padded_block (bl_tm M) (w ! s))"
    using P_s unfolding P_def by simp
  have s_min: "∀s'. P s' ⟶ s ≤ s'"
    unfolding s_def using Least_le by metis
  have pure_prefix: "∀i < s. is_pure_block (bl_tm M) (w ! i)"
  proof (intro allI impI)
    fix i assume i_lt_s: "i < s"
    have i_lt_lw: "i < length w" using i_lt_s s_lt by simp
    have i_neq_last: "i ≠ length w - 1"
      using i_lt_s s_lt w_pos by linarith
    have not_P_i: "¬ P i" using s_min i_lt_s by force
    hence "is_pure_block (bl_tm M) (w ! i)
           ∨ (i = length w - 1
              ∧ is_padded_block (bl_tm M) (w ! i))"
      using i_lt_lw unfolding P_def by auto
    thus "is_pure_block (bl_tm M) (w ! i)"
      using i_neq_last by auto
  qed
  have s_le_lw: "s ≤ length w" using s_lt by simp
  have sweep:
    "(?init,
       Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                (λi :: nat. if i = 0 then Suc s else 0))
      ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc s"
    by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t s_neq_r
                                            s_le_lw pure_prefix])
  have Sk_pos: "1 ≤ Suc s" by simp
  have Sk_le: "Suc s ≤ length w" using s_lt by simp
  have read_at_Ss: "?ts 0 (Suc s) = w ! s"
    using ae_init_config_tape_input[OF Sk_pos Sk_le kpos] by simp
  have w_s_in_set: "w ! s ∈ set w" using s_lt by auto
  have w_s_neq_bl: "w ! s ≠ bl_block (bl_tm M)"
    using w_s_in_set bl_notin by auto
  have w_s_neq_le: "w ! s ≠ LE_block (le_tm M)"
  proof (cases "le_tm M = bl_tm M")
    case True
    have eq: "LE_block (le_tm M) = bl_block (bl_tm M)"
      using True unfolding LE_block_def bl_block_def by simp
    have "w ! s ≠ bl_block (bl_tm M)" using w_s_in_set bl_notin by auto
    thus ?thesis using eq by metis
  next
    case False
    have le_notin: "le_tm M ∉ Sigma_tm M ∪ {bl_tm M}"
      using valid_mttm_LE_not_Sigma[OF vM] False by auto
    have "LE_block (le_tm M) ∉ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      using le_notin
      unfolding LE_block_def gamma_block_def by auto
    moreover have "w ! s ∈ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      using w_s_in_set w_sub by auto
    ultimately show ?thesis by auto
  qed
  have case_split: "(¬ is_canonical_block (bl_tm M) (w ! s))
                     ∨ (is_padded_block (bl_tm M) (w ! s)
                        ∧ Suc s < length w)"
  proof (cases "is_padded_block (bl_tm M) (w ! s)")
    case True
    have "s ≠ length w - 1" using s_not_last_padded True by simp
    hence "Suc s < length w" using s_lt by linarith
    thus ?thesis using True by simp
  next
    case False
    hence "¬ is_canonical_block (bl_tm M) (w ! s)"
      using s_not_pure unfolding is_canonical_block_def by simp
    thus ?thesis by simp
  qed
  consider
      (noncan) "¬ is_canonical_block (bl_tm M) (w ! s)"
    | (pad_misplaced) "is_padded_block (bl_tm M) (w ! s)"
                       "Suc s < length w"
    using case_split by blast
  thus ?thesis
  proof cases
    case noncan
    let ?n_Ss = "λi :: nat. if i = 0 then Suc s else 0"
    have read_nle: "?ts 0 (?n_Ss 0) ≠ LE_block (le_tm M)"
      using read_at_Ss w_s_neq_le by simp
    have read_nbl: "?ts 0 (?n_Ss 0) ≠ bl_block (bl_tm M)"
      using read_at_Ss w_s_neq_bl by simp
    have read_ncan: "¬ is_canonical_block (bl_tm M) (?ts 0 (?n_Ss 0))"
      using read_at_Ss noncan by simp
    have gamma: "∀kk :: nat. ?ts kk (?n_Ss kk) ∈ gamma_block (Γ_tm M)"
      using ae_init_config_in_gamma_block[OF vM w_sub] by simp
    have step_rej:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwd) ?ts ?n_Ss,
         Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Ss)
        ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_fwd_reject[where ts = ?ts and n = ?n_Ss,
            OF vM s_in_Q s_neq_t s_neq_r read_nle read_nbl read_ncan
            bt_all init_stage_tail gamma buf_gamma_init])
    have stage_eq: "init_stage (le_tm M)
                    = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
      unfolding init_stage_def ..
    have step_rej_init:
      "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_Ss,
         Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Ss)
        ∈ mttm_step (alphabet_enlarge_delta M)"
      using step_rej unfolding stage_eq by simp
    have full_chain:
      "(?init, Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Ss)
        ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc s)"
      by (rule relpow_Suc_I[OF sweep step_rej_init])
    have bound: "Suc (Suc s) ≤ length w + 2" using s_lt by linarith
    have q_eq:
      "case mt_state (Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Ss)
         of (qM', _, _, _, _) ⇒ qM' = r_tm M"
      by (simp add: init_stage_def)
    show ?thesis
      by (rule that[OF bound full_chain q_eq])
  next
    case pad_misplaced
    let ?n_Ss = "λi :: nat. if i = 0 then Suc s else 0"
    let ?n_SSs = "λi :: nat. if i = 0 then Suc (Suc s) else 0"
    have read_pad: "is_padded_block (bl_tm M) (?ts 0 (?n_Ss 0))"
      using read_at_Ss pad_misplaced(1) by simp
    have gamma_Ss: "∀kk :: nat. ?ts kk (?n_Ss kk) ∈ gamma_block (Γ_tm M)"
      using ae_init_config_in_gamma_block[OF vM w_sub] by simp
    have step_to_pad:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwd) ?ts ?n_Ss,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts
                  (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                                 (?n_Ss kk)))
        ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_fwd_to_padded[where ts = ?ts and n = ?n_Ss,
            OF s_in_Q s_neq_t s_neq_r read_pad bt_all init_stage_tail
               gamma_Ss buf_gamma_init])
    have post_eq:
      "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n_Ss kk))
       = ?n_SSs"
      by (rule ext) simp
    have step_to_pad_SS:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwd) ?ts ?n_Ss,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_SSs)
        ∈ mttm_step (alphabet_enlarge_delta M)"
      using step_to_pad post_eq by simp
    have stage_eq: "init_stage (le_tm M)
                    = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
      unfolding init_stage_def ..
    have step_to_pad_init:
      "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_Ss,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_SSs)
        ∈ mttm_step (alphabet_enlarge_delta M)"
      using step_to_pad_SS unfolding stage_eq by simp
    have SSs_pos: "1 ≤ Suc (Suc s)" by simp
    have SSs_le: "Suc (Suc s) ≤ length w"
      using pad_misplaced(2) by linarith
    have read_at_SSs: "?ts 0 (Suc (Suc s)) = w ! Suc s"
      using ae_init_config_tape_input[OF SSs_pos SSs_le kpos] by simp
    have wSs_in_set: "w ! Suc s ∈ set w"
      using SSs_le by auto
    have wSs_neq_bl: "w ! Suc s ≠ bl_block (bl_tm M)"
      using wSs_in_set bl_notin by auto
    have read_nbl_SS: "?ts 0 (?n_SSs 0) ≠ bl_block (bl_tm M)"
      using read_at_SSs wSs_neq_bl by simp
    have gamma_SS: "∀kk :: nat. ?ts kk (?n_SSs kk) ∈ gamma_block (Γ_tm M)"
      using ae_init_config_in_gamma_block[OF vM w_sub] by simp
    have step_pad_rej:
      "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_SSs,
         Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_SSs)
        ∈ mttm_step (alphabet_enlarge_delta M)"
      by (rule ae_step_val_pad_reject[where ts = ?ts and n = ?n_SSs,
            OF vM s_in_Q read_nbl_SS bt_all init_stage_tail
               gamma_SS buf_gamma_init])
    have post_sweep:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, VFwdPad) ?ts ?n_SSs)
        ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc s)"
      by (rule relpow_Suc_I[OF sweep step_to_pad_init])
    have full_chain:
      "(?init, Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_SSs)
        ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc (Suc s))"
      by (rule relpow_Suc_I[OF post_sweep step_pad_rej])
    have bound: "Suc (Suc (Suc s)) ≤ length w + 2"
      using pad_misplaced(2) by linarith
    have q_eq:
      "case mt_state (Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_SSs)
         of (qM', _, _, _, _) ⇒ qM' = r_tm M"
      by (simp add: init_stage_def)
    show ?thesis
      by (rule that[OF bound full_chain q_eq])
  qed
qed

lemma ae_validation_steps_bound:
  fixes M :: "('q, 'a) mttm"
    and w :: "('c :: enum ⇒ 'a) list"
  assumes vM: "valid_mttm M"
      and w_sub: "set w ⊆ gamma_block (Sigma_tm M ∪ {bl_tm M})"
      and s_neq_t: "s_tm M ≠ t_tm M"
      and s_neq_r: "s_tm M ≠ r_tm M"
      and le_neq_bl: "le_tm M ≠ bl_tm M"
  obtains f⇩v :: nat and n :: nat and c' where
      "n ≤ 2 * length w + f⇩v"
    and "(ae_init_config M w, c')
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
    and "case mt_state c' of (qM', _, _, _, idx) ⇒
            idx = SS1 ∨ qM' = r_tm M"
proof -
  let ?init = "ae_init_config M w"
  let ?ts = "mt_tape ?init"
  have kpos: "0 < k_tm M" by (rule valid_mttm_k_pos[OF vM])
  have bt_all: "∀j≥k_tm M. ∀i. ?ts j i = bl_block (bl_tm M)"
    using ae_init_config_tape_blank_tail by blast
  have buf_gamma_init:
      "∀kk :: nat.
          fst (init_buffer (le_tm M) kk
                  :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
              ∈ gamma_block (Γ_tm M)
          ∧ fst (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)
          ∧ snd (snd (init_buffer (le_tm M) kk
                        :: ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a)))
              ∈ gamma_block (Γ_tm M)"
    by (rule init_buffer_in_gamma_block_at_M[OF vM])
  have s_in_Q: "s_tm M ∈ Q_tm M" by (rule s_tm_in_Q_tm[OF vM])
  consider
      (no_bl_wf)
        "bl_block (bl_tm M) ∉ set w" "ae_input_well_formed (bl_tm M) w"
    | (no_bl_nwf)
        "bl_block (bl_tm M) ∉ set w" "¬ ae_input_well_formed (bl_tm M) w"
    | (has_bl)
        "bl_block (bl_tm M) ∈ set w"
    by blast
  thus ?thesis
  proof cases
    case no_bl_nwf
    obtain n c' where
        bound: "n ≤ length w + 2"
      and chain: "(ae_init_config M w, c')
                    ∈ mttm_step (alphabet_enlarge_delta M) ^^ n"
      and state_eq: "case mt_state c' of (qM', _, _, _, _) ⇒ qM' = r_tm M"
      using ae_validation_post_state_noncanonical[OF vM w_sub
              no_bl_nwf(1) no_bl_nwf(2) s_neq_t s_neq_r] by metis
    have bound2: "n ≤ 2 * length w + 4" using bound by linarith
    have state_eq_disj: "case mt_state c'
            of (qM', _, _, _, idx) ⇒ idx = SS1 ∨ qM' = r_tm M"
      using state_eq by (cases "mt_state c'") auto
    show ?thesis using bound2 chain state_eq_disj by (rule that)
  next
    case no_bl_wf
    have wf: "ae_input_well_formed (bl_tm M) w" using no_bl_wf(2) .
    have full_chain:
      "(?init,
         Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                    init_dest, SS1) ?ts (λ_. 0))
          ∈ mttm_step (alphabet_enlarge_delta M)
              ^^ (2 * length w + 4)"
      by (rule ae_validation_well_formed_to_SS1[OF vM w_sub wf s_in_Q
            s_neq_t s_neq_r le_neq_bl])
    have bound: "(2 * length w + 4 :: nat) ≤ 2 * length w + 4" by simp
    have state_eq:
      "case mt_state (Config⇩M (s_tm M, init_offset,
                                     init_buffer (le_tm M),
                                     init_dest, SS1) ?ts (λ_. 0))
          of (qM', _, _, _, idx) ⇒ idx = SS1 ∨ qM' = r_tm M"
      by simp
    show ?thesis by (rule that[OF bound full_chain state_eq])
  next
    case has_bl
    have LE_neq_bl_block: "LE_block (le_tm M) ≠ bl_block (bl_tm M)"
      using le_neq_bl unfolding LE_block_def bl_block_def
      by (metis fun_eq_iff)
    have tape_le: "?ts (0 :: nat) 0 = LE_block (le_tm M)"
      by (rule ae_init_config_tape_le[OF kpos])
    have gamma_all: "∀k i. ?ts k i ∈ gamma_block (Γ_tm M)"
      using ae_init_config_in_gamma_block[OF vM w_sub] by simp
    have stage_eq: "init_stage (le_tm M)
                    = (init_offset, init_buffer (le_tm M), init_dest, VFwd)"
      unfolding init_stage_def ..
    ― ‹Show ‹LE_block le_M ∉ set w›: in the ‹le ≠ bl›
        regime, ‹le ∉ Σ ∪ {bl}› forces ‹LE_block› out of
        ‹gamma_block›.›
    have LE_notin: "LE_block (le_tm M) ∉ set w"
    proof -
      have le_notin: "le_tm M ∉ Sigma_tm M ∪ {bl_tm M}"
        using valid_mttm_LE_not_Sigma[OF vM] le_neq_bl by auto
      have "LE_block (le_tm M) ∉ gamma_block (Sigma_tm M ∪ {bl_tm M})"
        using le_notin
        unfolding LE_block_def gamma_block_def by auto
      thus ?thesis using w_sub by auto
    qed
    ― ‹Find the first non-pure index — well-defined because
        ‹bl_block› is non-pure and present somewhere in ‹w›.›
    define P where
      "P = (λi. i < length w ∧ ¬ is_pure_block (bl_tm M) (w ! i))"
    have ex_P: "∃i. P i"
    proof -
      from has_bl obtain j where j_lt: "j < length w" and j_eq: "w ! j = bl_block (bl_tm M)"
        by (auto simp: in_set_conv_nth)
      have "¬ is_pure_block (bl_tm M) (bl_block (bl_tm M))"
        unfolding is_pure_block_def bl_block_def by auto
      hence "¬ is_pure_block (bl_tm M) (w ! j)" using j_eq by simp
      thus ?thesis unfolding P_def using j_lt by auto
    qed
    define k where "k = (LEAST i. P i)"
    from ex_P have P_k: "P k" unfolding k_def by (rule LeastI_ex)
    have k_lt: "k < length w" using P_k unfolding P_def by simp
    have k_not_pure: "¬ is_pure_block (bl_tm M) (w ! k)"
      using P_k unfolding P_def by simp
    have k_min: "∀j. P j ⟶ k ≤ j"
      unfolding k_def using Least_le by metis
    have pure_prefix: "∀i < k. is_pure_block (bl_tm M) (w ! i)"
    proof (intro allI impI)
      fix i assume i_lt_k: "i < k"
      have i_lt_w: "i < length w" using i_lt_k k_lt by simp
      have "¬ P i" using k_min i_lt_k by force
      thus "is_pure_block (bl_tm M) (w ! i)" unfolding P_def using i_lt_w by auto
    qed
    have k_le_lw: "k ≤ length w" using k_lt by simp
    have sweep:
      "(?init,
          Config⇩M (s_tm M, init_stage (le_tm M)) ?ts
                   (λi :: nat. if i = 0 then Suc k else 0))
          ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc k"
      by (rule ae_validation_fwd_sweep_pure[OF vM w_sub s_in_Q s_neq_t
                                              s_neq_r k_le_lw pure_prefix])
    let ?n_Sk = "λi :: nat. if i = 0 then Suc k else 0"
    have Sk_pos: "1 ≤ Suc k" by simp
    have Sk_le: "Suc k ≤ length w" using k_lt by simp
    have read_at_Sk: "?ts 0 (Suc k) = w ! k"
      using ae_init_config_tape_input[OF Sk_pos Sk_le kpos] by simp
    have w_k_in_set: "w ! k ∈ set w" using k_lt by auto
    have w_k_neq_le: "w ! k ≠ LE_block (le_tm M)"
      using w_k_in_set LE_notin by auto
    ― ‹Case-split on ‹w!k›: ‹bl_block› (passes), padded
        (sub-case on next), or non-canonical (rejects).›
    consider
        (case_bl) "w ! k = bl_block (bl_tm M)"
      | (case_pad) "is_padded_block (bl_tm M) (w ! k)"
      | (case_noncan) "¬ is_canonical_block (bl_tm M) (w ! k)"
                       "w ! k ≠ bl_block (bl_tm M)"
      using k_not_pure unfolding is_canonical_block_def by blast
    thus ?thesis
    proof cases
      case case_bl
      ― ‹Forward sweep + ‹fwd_to_ret› + return sweep, ending at SS1.›
      have read_bl: "?ts 0 (?n_Sk 0) = bl_block (bl_tm M)"
        using read_at_Sk case_bl by simp
      have gamma_Sk:
        "∀kk :: nat. ?ts kk (?n_Sk kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_to_ret:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwd) ?ts ?n_Sk,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VRet) ?ts ?n_Sk)
            ∈ mttm_step (alphabet_enlarge_delta M)"
        by (rule ae_step_val_fwd_to_ret[where ts = ?ts and n = ?n_Sk,
              OF s_in_Q s_neq_t s_neq_r read_bl bt_all init_stage_tail
                 gamma_Sk buf_gamma_init])
      have step_to_ret_init:
        "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_Sk,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VRet) ?ts ?n_Sk)
            ∈ mttm_step (alphabet_enlarge_delta M)"
        using step_to_ret unfolding stage_eq by simp
      have post_sweep:
        "(?init,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VRet) ?ts ?n_Sk)
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc k)"
        by (rule relpow_Suc_I[OF sweep step_to_ret_init])
      have non_le_Sk: "∀i. 1 ≤ i ∧ i ≤ Suc k
                          ⟶ ?ts 0 i ≠ LE_block (le_tm M)"
      proof (intro allI impI)
        fix i assume i_range: "1 ≤ i ∧ i ≤ Suc k"
        have i_pos: "1 ≤ i" using i_range by simp
        have i_le_lw: "i ≤ length w" using i_range Sk_le by linarith
        have eq: "?ts 0 i = w ! (i - 1)"
          using ae_init_config_tape_input[OF i_pos i_le_lw kpos] by simp
        have "w ! (i - 1) ∈ set w" using i_pos i_le_lw by auto
        thus "?ts 0 i ≠ LE_block (le_tm M)" using LE_notin eq by auto
      qed
      have ret_arrow:
        "(∀i. 1 ≤ i ∧ i ≤ Suc k
              ⟶ ?ts 0 i ≠ LE_block (le_tm M))
         ⟶ (Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                          init_dest, VRet) ?ts ?n_Sk,
              Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                          init_dest, SS1) ?ts (λ_. 0))
              ∈ mttm_step (alphabet_enlarge_delta M)
                  ^^ Suc (Suc k)"
        by (rule ae_validation_ret_sweep[OF s_in_Q tape_le gamma_all
                                          buf_gamma_init bt_all init_stage_tail])
      have ret_chain:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VRet) ?ts ?n_Sk,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, SS1) ?ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M)
                ^^ Suc (Suc k)"
        using ret_arrow non_le_Sk by (rule mp)
      have full_chain_pre:
        "(?init,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, SS1) ?ts (λ_. 0))
            ∈ mttm_step (alphabet_enlarge_delta M)
                ^^ (Suc (Suc k) + Suc (Suc k))"
      proof -
        have comp:
          "(?init,
             Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, SS1) ?ts (λ_. 0))
              ∈ mttm_step (alphabet_enlarge_delta M)
                  ^^ Suc (Suc k)
                O mttm_step (alphabet_enlarge_delta M)
                  ^^ Suc (Suc k)"
          using post_sweep ret_chain by (rule relcompI)
        thus ?thesis by (simp only: relpow_add)
      qed
      have bound: "Suc (Suc k) + Suc (Suc k) ≤ 2 * length w + 4"
        using k_lt by linarith
      have state_eq:
        "case mt_state (Config⇩M (s_tm M, init_offset,
                                       init_buffer (le_tm M),
                                       init_dest, SS1) ?ts (λ_. 0))
            of (qM', _, _, _, idx) ⇒ idx = SS1 ∨ qM' = r_tm M"
        by simp
      show ?thesis by (rule that[OF bound full_chain_pre state_eq])
    next
      case case_pad
      ― ‹In ‹has_bl› + first-non-pure-padded, the ‹bl_block› must
          appear at some position ‹j > k›, hence ‹Suc k < length
          w›.›
      have Sk_lt: "Suc k < length w"
      proof -
        from has_bl obtain j where j_lt: "j < length w"
              and j_eq: "w ! j = bl_block (bl_tm M)" by (auto simp: in_set_conv_nth)
        have "j ≥ k"
        proof (rule ccontr)
          assume "¬ j ≥ k"
          hence "j < k" by simp
          hence "is_pure_block (bl_tm M) (w ! j)" using pure_prefix by simp
          moreover have "¬ is_pure_block (bl_tm M) (bl_block (bl_tm M))"
            unfolding is_pure_block_def bl_block_def by auto
          ultimately show False using j_eq by auto
        qed
        moreover have "j ≠ k"
        proof
          assume "j = k"
          hence wk_bl: "w ! k = bl_block (bl_tm M)" using j_eq by simp
          have not_padded:
            "¬ is_padded_block (bl_tm M) ((bl_block (bl_tm M)) :: 'c ⇒ 'a)"
          proof
            assume "is_padded_block (bl_tm M)
                    ((bl_block (bl_tm M)) :: 'c ⇒ 'a)"
            then obtain k_pad where
                k_pad_pos: "k_pad ≥ 1"
              and k_pad_lt: "k_pad < length (enum_class.enum :: 'c list)"
              and prefix_cond:
                "∀x. c_idx x < k_pad
                      ⟶ ((bl_block (bl_tm M)) :: 'c ⇒ 'a) x ≠ bl_tm M"
              unfolding is_padded_block_def by blast
            have len_pos: "0 < length (enum_class.enum :: 'c list)"
              using k_pad_lt k_pad_pos by linarith
            have "c_idx ((enum_class.enum :: 'c list) ! 0) = 0"
              by (rule c_idx_enum_nth[OF len_pos])
            hence c_first_idx: "c_idx (c_first :: 'c) = 0"
              unfolding c_first_def .
            hence "c_idx (c_first :: 'c) < k_pad"
              using k_pad_pos by simp
            hence "(bl_block (bl_tm M) :: 'c ⇒ 'a) c_first ≠ bl_tm M"
              using prefix_cond by blast
            thus False unfolding bl_block_def by simp
          qed
          show False using case_pad wk_bl not_padded by simp
        qed
        ultimately have "j > k" by simp
        thus ?thesis using j_lt by linarith
      qed
      let ?n_SSk = "λi :: nat. if i = 0 then Suc (Suc k) else 0"
      have read_pad: "is_padded_block (bl_tm M) (?ts 0 (?n_Sk 0))"
        using read_at_Sk case_pad by simp
      have gamma_Sk:
        "∀kk :: nat. ?ts kk (?n_Sk kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_to_pad:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwd) ?ts ?n_Sk,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwdPad) ?ts
                  (λkk. go_dir (if kk = (0 :: nat) then dir.R else dir.N)
                                 (?n_Sk kk)))
            ∈ mttm_step (alphabet_enlarge_delta M)"
        by (rule ae_step_val_fwd_to_padded[where ts = ?ts and n = ?n_Sk,
              OF s_in_Q s_neq_t s_neq_r read_pad bt_all init_stage_tail
                 gamma_Sk buf_gamma_init])
      have post_eq_pad:
        "(λkk :: nat. go_dir (if kk = 0 then dir.R else dir.N) (?n_Sk kk))
         = ?n_SSk"
        by (rule ext) simp
      have step_to_pad_norm:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwd) ?ts ?n_Sk,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwdPad) ?ts ?n_SSk)
            ∈ mttm_step (alphabet_enlarge_delta M)"
        using step_to_pad post_eq_pad by simp
      have step_to_pad_init:
        "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_Sk,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwdPad) ?ts ?n_SSk)
            ∈ mttm_step (alphabet_enlarge_delta M)"
        using step_to_pad_norm unfolding stage_eq by simp
      have post_sweep_VFwdPad:
        "(?init,
           Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwdPad) ?ts ?n_SSk)
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc k)"
        by (rule relpow_Suc_I[OF sweep step_to_pad_init])
      have SSk_pos: "1 ≤ Suc (Suc k)" by simp
      have SSk_le: "Suc (Suc k) ≤ length w" using Sk_lt by linarith
      have read_at_SSk: "?ts 0 (Suc (Suc k)) = w ! Suc k"
        using ae_init_config_tape_input[OF SSk_pos SSk_le kpos] by simp
      have wSk_in_set: "w ! Suc k ∈ set w" using SSk_le by auto
      have gamma_SSk:
        "∀kk :: nat. ?ts kk (?n_SSk kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      ― ‹Sub-case on ‹w ! Suc k›: ‹bl_block› (passes via
          ‹pad_to_ret›) or non-‹bl_block› (rejects via ‹pad_reject›).›
      consider
          (pad_pass) "w ! Suc k = bl_block (bl_tm M)"
        | (pad_reject) "w ! Suc k ≠ bl_block (bl_tm M)"
        by blast
      thus ?thesis
      proof cases
        case pad_pass
        have read_bl_SSk: "?ts 0 (?n_SSk 0) = bl_block (bl_tm M)"
          using read_at_SSk pad_pass by simp
        have step_pad_to_ret:
          "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VFwdPad) ?ts ?n_SSk,
             Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VRet) ?ts ?n_SSk)
              ∈ mttm_step (alphabet_enlarge_delta M)"
          by (rule ae_step_val_pad_to_ret[where ts = ?ts and n = ?n_SSk,
                OF s_in_Q read_bl_SSk bt_all init_stage_tail
                   gamma_SSk buf_gamma_init])
        have post_sweep_VRet:
          "(?init,
             Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VRet) ?ts ?n_SSk)
              ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc (Suc k))"
          by (rule relpow_Suc_I[OF post_sweep_VFwdPad step_pad_to_ret])
        have non_le_SSk: "∀i. 1 ≤ i ∧ i ≤ Suc (Suc k)
                              ⟶ ?ts 0 i ≠ LE_block (le_tm M)"
        proof (intro allI impI)
          fix i assume i_range: "1 ≤ i ∧ i ≤ Suc (Suc k)"
          have i_pos: "1 ≤ i" using i_range by simp
          have i_le_lw: "i ≤ length w" using i_range SSk_le by linarith
          have eq: "?ts 0 i = w ! (i - 1)"
            using ae_init_config_tape_input[OF i_pos i_le_lw kpos] by simp
          have "w ! (i - 1) ∈ set w" using i_pos i_le_lw by auto
          thus "?ts 0 i ≠ LE_block (le_tm M)" using LE_notin eq by auto
        qed
        have ret_arrow:
          "(∀i. 1 ≤ i ∧ i ≤ Suc (Suc k)
                ⟶ ?ts 0 i ≠ LE_block (le_tm M))
           ⟶ (Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                            init_dest, VRet) ?ts ?n_SSk,
                Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                            init_dest, SS1) ?ts (λ_. 0))
                ∈ mttm_step (alphabet_enlarge_delta M)
                    ^^ Suc (Suc (Suc k))"
          by (rule ae_validation_ret_sweep[OF s_in_Q tape_le gamma_all
                                          buf_gamma_init bt_all init_stage_tail])
        have ret_chain:
          "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VRet) ?ts ?n_SSk,
             Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, SS1) ?ts (λ_. 0))
              ∈ mttm_step (alphabet_enlarge_delta M)
                  ^^ Suc (Suc (Suc k))"
          using ret_arrow non_le_SSk by (rule mp)
        have full_chain:
          "(?init,
             Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, SS1) ?ts (λ_. 0))
              ∈ mttm_step (alphabet_enlarge_delta M)
                  ^^ (Suc (Suc (Suc k)) + Suc (Suc (Suc k)))"
        proof -
          have comp:
            "(?init,
               Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                          init_dest, SS1) ?ts (λ_. 0))
                ∈ mttm_step (alphabet_enlarge_delta M)
                    ^^ Suc (Suc (Suc k))
                  O mttm_step (alphabet_enlarge_delta M)
                    ^^ Suc (Suc (Suc k))"
            using post_sweep_VRet ret_chain by (rule relcompI)
          thus ?thesis by (simp only: relpow_add)
        qed
        have bound:
          "Suc (Suc (Suc k)) + Suc (Suc (Suc k)) ≤ 2 * length w + 4"
          using Sk_lt by linarith
        have state_eq:
          "case mt_state (Config⇩M (s_tm M, init_offset,
                                         init_buffer (le_tm M),
                                         init_dest, SS1) ?ts (λ_. 0))
              of (qM', _, _, _, idx) ⇒ idx = SS1 ∨ qM' = r_tm M"
          by simp
        show ?thesis by (rule that[OF bound full_chain state_eq])
      next
        case pad_reject
        have read_nbl_SSk: "?ts 0 (?n_SSk 0) ≠ bl_block (bl_tm M)"
          using read_at_SSk pad_reject by simp
        have step_pad_rej:
          "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                        init_dest, VFwdPad) ?ts ?n_SSk,
             Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_SSk)
              ∈ mttm_step (alphabet_enlarge_delta M)"
          by (rule ae_step_val_pad_reject[where ts = ?ts and n = ?n_SSk,
                OF vM s_in_Q read_nbl_SSk bt_all init_stage_tail
                   gamma_SSk buf_gamma_init])
        have full_chain:
          "(?init, Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_SSk)
              ∈ mttm_step (alphabet_enlarge_delta M)
                  ^^ Suc (Suc (Suc k))"
          by (rule relpow_Suc_I[OF post_sweep_VFwdPad step_pad_rej])
        have bound: "Suc (Suc (Suc k)) ≤ 2 * length w + 4"
          using Sk_lt by linarith
        have state_eq:
          "case mt_state (Config⇩M (r_tm M, init_stage (le_tm M))
                                       ?ts ?n_SSk)
              of (qM', _, _, _, idx) ⇒ idx = SS1 ∨ qM' = r_tm M"
          by (simp add: init_stage_def)
        show ?thesis by (rule that[OF bound full_chain state_eq])
      qed
    next
      case case_noncan
      have read_nle: "?ts 0 (?n_Sk 0) ≠ LE_block (le_tm M)"
        using read_at_Sk w_k_neq_le by simp
      have read_nbl: "?ts 0 (?n_Sk 0) ≠ bl_block (bl_tm M)"
        using read_at_Sk case_noncan(2) by simp
      have read_ncan: "¬ is_canonical_block (bl_tm M) (?ts 0 (?n_Sk 0))"
        using read_at_Sk case_noncan(1) by simp
      have gamma_Sk:
        "∀kk :: nat. ?ts kk (?n_Sk kk) ∈ gamma_block (Γ_tm M)"
        using gamma_all by simp
      have step_rej:
        "(Config⇩M (s_tm M, init_offset, init_buffer (le_tm M),
                      init_dest, VFwd) ?ts ?n_Sk,
           Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Sk)
            ∈ mttm_step (alphabet_enlarge_delta M)"
        by (rule ae_step_val_fwd_reject[where ts = ?ts and n = ?n_Sk,
              OF vM s_in_Q s_neq_t s_neq_r read_nle read_nbl read_ncan
              bt_all init_stage_tail gamma_Sk buf_gamma_init])
      have step_rej_init:
        "(Config⇩M (s_tm M, init_stage (le_tm M)) ?ts ?n_Sk,
           Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Sk)
            ∈ mttm_step (alphabet_enlarge_delta M)"
        using step_rej unfolding stage_eq by simp
      have full_chain:
        "(?init, Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Sk)
            ∈ mttm_step (alphabet_enlarge_delta M) ^^ Suc (Suc k)"
        by (rule relpow_Suc_I[OF sweep step_rej_init])
      have bound: "Suc (Suc k) ≤ 2 * length w + 4" using k_lt by linarith
      have state_eq:
        "case mt_state (Config⇩M (r_tm M, init_stage (le_tm M)) ?ts ?n_Sk)
            of (qM', _, _, _, idx) ⇒ idx = SS1 ∨ qM' = r_tm M"
        by (simp add: init_stage_def)
      show ?thesis by (rule that[OF bound full_chain state_eq])
    qed
  qed
qed

end