Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_ComputeCorrect

theory AlphabetEnlargement_ComputeCorrect
  imports AlphabetEnlargement_ValidationBound
begin

text ‹Entry point of the ‹alphabet_enlarge›
  forward-simulation chain (the combinator is defined in
  ‹AlphabetEnlargement_Simulation›).  The chain establishes
  that ‹M' = alphabet_enlarge M› simulates ‹M›, and
  culminates in the three top-level theorems characterising the
  combinator — well-formedness preservation
  (‹alphabet_enlarge_wf›), forward language preservation
  modulo input encoding
  (‹alphabet_enlarge_language_forward›), and the linear
  time bound (‹alphabet_enlarge_time›) — which are proved
  in theory ‹AlphabetEnlargement› at the end of the chain.
  The construction follows the linear-speedup theorem of
  Hartmanis and Stearns
  \<^cite>‹‹Theorem 2› in "Hartmanis1965:computational"›,
  modernised in Hopcroft and Ullman
  \<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"›.

  The forward chain is split across theories in dependency
  order, each importing the previous:
  ▪ ‹AlphabetEnlargement_ComputeCorrect› (this theory):
    per-substep state shape and invariant preservation, the
    ‹mttm_step› lift, and buffered c-fold compute
    correctness.
  ▪ ‹AlphabetEnlargement_SS4›: SS4 trace-existence and
    the buffer characterisations at SS4 entry.
  ▪ ‹AlphabetEnlargement_OutputWF›: home classification
    and output well-formedness.
  ▪ ‹AlphabetEnlargement_ForwardStage›: the per-tape
    unified forward stage
    ‹ae_simulates_forward_stage_general›.
  ▪ ‹AlphabetEnlargement_Acceptance›: acceptance
    correspondence and the step-count / chunked simulation
    engine.
  ▪ ‹AlphabetEnlargement›: the three top-level
    theorems.›

subsection ‹Forward simulation chain›

subsubsection ‹Per-substep state shape and invariant preservation›

text ‹Per-substep mid-stage invariant preservation lemmas.
  Eight in total, one per simulation substep transition
  SS‹n›‹→›SS‹n+1› (with SS9 ‹≡› SS1 by
  wrap-around).›

text ‹Common skeleton: each per-substep delta is a set of
  tuples whose post-state component fixes ‹idx› at the target
  substep and constrains ‹q› via ‹q ∈ Q_tm M›.
  This helper packages the ‹mttm_step›-elimination plus the
  set-comprehension destructuring once, reducing each per-substep
  proof to a one-line shape obligation discharged by ‹auto› on
  the relevant ‹ae_delta_ss<N>_ss<N+1>_def›.

  The helper does not apply to ‹ae_step_ss8_ss1_invariant›:
  that substep's halting branch lands at ‹idx = VFwd›, not
  ‹idx = SS1›, so the post-state's ‹idx› is not uniformly
  fixed.›

lemma ae_substep_state_shape:
  fixes M :: "('q, 'a) mttm"
    and δ :: "(('q × ('a, 'c :: enum) ae_stage)
              × (nat ⇒ ('c ⇒ 'a))
              × ('q × ('a, 'c) ae_stage)
              × (nat ⇒ ('c ⇒ 'a))
              × (nat ⇒ dir)) set"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
    and tgt :: substep_idx
  assumes step: "(c', c'') ∈ mttm_step δ"
      and shape: "⋀s a s' a' d.
                    (s, a, s', a', d) ∈ δ
                      ⟹ ∃q ofs buf dest.
                            s' = (q, ofs, buf, dest, tgt)
                            ∧ q ∈ Q_tm M"
  shows "case mt_state c'' of (qM', _, _, _, idx) ⇒
            idx = tgt ∧ qM' ∈ Q_tm M"
proof -
  from step obtain s ts n s' a' d where
      c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ δ"
    by (auto elim: mttm_step.cases)
  from shape[OF rel] obtain q ofs buf dest where
      s'_eq: "s' = (q, ofs, buf, dest, tgt)"
      and q_in: "q ∈ Q_tm M"
    by blast
  show ?thesis using c''_eq s'_eq q_in by simp
qed

lemma ae_step_ss1_ss2_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss1 M c'"
      and "(c', c'') ∈ mttm_step (ae_delta_ss1_ss2 M)"
    shows "ae_inv_ss2 M c''"
proof -
  have shape: "⋀s a s' a' d.
                  (s, a, s', a', d) ∈ ae_delta_ss1_ss2 M
                    ⟹ ∃q ofs buf dest.
                          s' = (q, ofs, buf, dest, SS2)
                          ∧ q ∈ Q_tm M"
    by (force simp: ae_delta_ss1_ss2_def)
  show "ae_inv_ss2 M c''"
    unfolding ae_inv_ss2_def
    using ae_substep_state_shape[OF assms(3) shape] .
qed

lemma ae_step_ss2_ss3_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss2 M c'"
      and "(c', c'') ∈ mttm_step (ae_delta_ss2_ss3 M)"
    shows "ae_inv_ss3 M c''"
proof -
  have shape: "⋀s a s' a' d.
                  (s, a, s', a', d) ∈ ae_delta_ss2_ss3 M
                    ⟹ ∃q ofs buf dest.
                          s' = (q, ofs, buf, dest, SS3)
                          ∧ q ∈ Q_tm M"
    by (force simp: ae_delta_ss2_ss3_def)
  show "ae_inv_ss3 M c''"
    unfolding ae_inv_ss3_def
    using ae_substep_state_shape[OF assms(3) shape] .
qed

lemma ae_step_ss3_ss4_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss3 M c'"
      and "(c', c'') ∈ mttm_step (ae_delta_ss3_ss4 M)"
    shows "ae_inv_ss4 M c''"
proof -
  have shape: "⋀s a s' a' d.
                  (s, a, s', a', d) ∈ ae_delta_ss3_ss4 M
                    ⟹ ∃q ofs buf dest.
                          s' = (q, ofs, buf, dest, SS4)
                          ∧ q ∈ Q_tm M"
    by (force simp: ae_delta_ss3_ss4_def)
  show "ae_inv_ss4 M c''"
    unfolding ae_inv_ss4_def
    using ae_substep_state_shape[OF assms(3) shape] .
qed

lemma ae_step_ss4_ss5_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes valM: "valid_mttm M"
      and "ae_inv_ss4 M c'"
      and step: "(c', c'') ∈ mttm_step (ae_delta_ss4_ss5 M)"
    shows "ae_inv_ss5 M c''"
proof -
  ― ‹Unlike the template substeps, ss4 ‹→›
      ss5 advances the ‹q›-component via
      ‹m_steps_buffered›; ‹Q_tm›-membership is preserved
      through the chain by
      ‹m_steps_buffered_state_preservation›.  The
      ‹ae_substep_state_shape› helper does not apply directly
      because its uniform shape obligation can't pull in
      ‹valM› at the right scope; we instead inline the
      ‹mttm_step›-elimination.›
  from step obtain s ts n s' a' d where
      c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ ae_delta_ss4_ss5 M"
    by (auto elim: mttm_step.cases)
  from rel[unfolded ae_delta_ss4_ss5_def mem_Collect_eq]
  obtain q ofs buf dest_old q' ofs' buf' dest'
         buf_full end_pos bufC
    where s_eq: "s = (q, ofs, buf, dest_old, SS4)"
      and s'_eq: "s' = (q', ofs', buf', dest', SS5)"
      and q_Q: "q ∈ Q_tm M"
      and m_steps: "((q, buf_full, λk. (AE_Home, ofs k)),
                      (q', bufC, end_pos))
                        ∈ m_steps_buffered M"
    by auto
  from m_steps_buffered_state_preservation[OF valM m_steps q_Q]
  have q'_in_Q: "q' ∈ Q_tm M" .
  show "ae_inv_ss5 M c''"
    unfolding ae_inv_ss5_def using c''_eq s'_eq q'_in_Q by simp
qed

lemma ae_step_ss5_ss6_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss5 M c'"
      and "(c', c'') ∈ mttm_step (ae_delta_ss5_ss6 M)"
    shows "ae_inv_ss6 M c''"
proof -
  have shape: "⋀s a s' a' d.
                  (s, a, s', a', d) ∈ ae_delta_ss5_ss6 M
                    ⟹ ∃q ofs buf dest.
                          s' = (q, ofs, buf, dest, SS6)
                          ∧ q ∈ Q_tm M"
    by (force simp: ae_delta_ss5_ss6_def)
  show "ae_inv_ss6 M c''"
    unfolding ae_inv_ss6_def
    using ae_substep_state_shape[OF assms(3) shape] .
qed

lemma ae_step_ss6_ss7_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss6 M c'"
      and "(c', c'') ∈ mttm_step (ae_delta_ss6_ss7 M)"
    shows "ae_inv_ss7 M c''"
proof -
  have shape: "⋀s a s' a' d.
                  (s, a, s', a', d) ∈ ae_delta_ss6_ss7 M
                    ⟹ ∃q ofs buf dest.
                          s' = (q, ofs, buf, dest, SS7)
                          ∧ q ∈ Q_tm M"
    by (force simp: ae_delta_ss6_ss7_def)
  show "ae_inv_ss7 M c''"
    unfolding ae_inv_ss7_def
    using ae_substep_state_shape[OF assms(3) shape] .
qed

lemma ae_step_ss7_ss8_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss7 M c'"
      and "(c', c'') ∈ mttm_step (ae_delta_ss7_ss8 M)"
    shows "ae_inv_ss8 M c''"
proof -
  have shape: "⋀s a s' a' d.
                  (s, a, s', a', d) ∈ ae_delta_ss7_ss8 M
                    ⟹ ∃q ofs buf dest.
                          s' = (q, ofs, buf, dest, SS8)
                          ∧ q ∈ Q_tm M"
    by (force simp: ae_delta_ss7_ss8_def)
  show "ae_inv_ss8 M c''"
    unfolding ae_inv_ss8_def
    using ae_substep_state_shape[OF assms(3) shape] .
qed

lemma ae_step_ss8_ss1_invariant:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes "valid_mttm M"
      and "ae_inv_ss8 M c'"
      and non_halt: "case mt_state c' of (qM', _, _, _, _) ⇒
                        qM' ≠ t_tm M ∧ qM' ≠ r_tm M"
      and step: "(c', c'') ∈ mttm_step (ae_delta_ss8_ss1 M)"
    shows "ae_inv_ss1 M c''"
proof -
  ― ‹The cycle-closure substep has a halting branch
      (‹q ∈ {t_tm M, r_tm M}›) that lands at ‹idx = VFwd›,
      not ‹idx = SS1›; the ‹non_halt› assumption forces
      the steady-state branch.›
  from step obtain s ts n s' a' d where
      c'_eq: "c' = Config⇩M s ts n"
      and c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ ae_delta_ss8_ss1 M"
    by (auto elim: mttm_step.cases)
  from rel obtain q ofs buf dest stage' where
      s_eq: "s = (q, ofs, buf, dest, SS8)"
      and s'_eq: "s' = (q, stage')"
      and q_in: "q ∈ Q_tm M"
      and stage'_eq: "stage' = (if q ∈ {t_tm M, r_tm M}
                                  then init_stage (le_tm M)
                                  else (ofs, buf, init_dest, SS1))"
    by (auto simp: ae_delta_ss8_ss1_def)
  from non_halt c'_eq s_eq have q_non_halt: "q ≠ t_tm M ∧ q ≠ r_tm M"
    by simp
  with stage'_eq have stage'_resolved:
      "stage' = (ofs, buf, init_dest, SS1)" by simp
  show "ae_inv_ss1 M c''"
    unfolding ae_inv_ss1_def
    using c''_eq s'_eq stage'_resolved q_in by simp
qed

text ‹Halt-branch invariant for SS8‹→›SS1: when
  ‹M›'s simulated state at SS8 is halting
  (‹qM' ∈ {t_tm M, r_tm M}›), the SS8‹→›SS1
  step routes to ‹init_stage le› (post-idx is ‹VFwd›, not
  ‹SS1›) and preserves the halt-state ‹q›.  Companion to
  ‹ae_step_ss8_ss1_invariant› (non-halt branch).  The chain
  proof in ‹ae_simulates_forward_stage› case-splits on whether
  ‹M›'s state is halting at SS8 and applies one of these two
  lemmas accordingly; the halt branch lands in the simulation's
  halt disjunct (‹qM' ∈ {t_tm M, r_tm M}›), the non-halt
  branch in the SS1 disjunct.›

lemma ae_step_ss8_ss1_invariant_halt:
  fixes M :: "('q, 'a) mttm"
    and c' c'' :: "('c :: enum ⇒ 'a,
                    'q × ('a, 'c) ae_stage) mt_config"
  assumes inv: "ae_inv_ss8 M c'"
      and halt: "case mt_state c' of (qM', _, _, _, _) ⇒
                    qM' ∈ {t_tm M, r_tm M}"
      and step: "(c', c'') ∈ mttm_step (ae_delta_ss8_ss1 M)"
    shows "(case mt_state c'' of (qM', _, _, _, idx) ⇒
              qM' ∈ {t_tm M, r_tm M} ∧ idx = VFwd)"
proof -
  from step obtain s ts n s' a' d where
      c'_eq: "c' = Config⇩M s ts n"
      and c''_eq: "c'' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d) ∈ ae_delta_ss8_ss1 M"
    by (auto elim: mttm_step.cases)
  from rel obtain q ofs buf dest stage' where
      s_eq: "s = (q, ofs, buf, dest, SS8)"
      and s'_eq: "s' = (q, stage')"
      and q_in: "q ∈ Q_tm M"
      and stage'_eq: "stage' = (if q ∈ {t_tm M, r_tm M}
                                  then init_stage (le_tm M)
                                  else (ofs, buf, init_dest, SS1))"
    by (auto simp: ae_delta_ss8_ss1_def)
  from halt c'_eq s_eq have q_halt: "q ∈ {t_tm M, r_tm M}"
    by simp
  with stage'_eq have stage'_resolved:
      "stage' = init_stage (le_tm M)" by simp
  show ?thesis
    using c''_eq s'_eq stage'_resolved q_halt
    unfolding init_stage_def by simp
qed

subsubsection ‹‹mttm_step› lifts of cross-phase exclusions›

text ‹‹mttm_step›-level lifts of the cross-phase exclusion
  lemmas ‹ae_delta_ssN_only›: when a substrate-level step
  in the alphabet-enlarged combinator's union has source
  ‹substep_idx› ‹SSN›, the step is in the canonical
  ‹ae_delta_ssN_ssM› substep relation.  Used by the reverse
  arm to commit each peeled ‹δ'›-step to its canonical
  substep before invoking the per-substep invariant
  propagation.›

lemma mttm_step_ae_delta_ss1_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss1: "snd (snd (snd (snd (mt_state c)))) = SS1"
    shows "(c, c') ∈ mttm_step (ae_delta_ss1_ss2 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss1 c_eq have s_ss1: "snd (snd (snd (snd s))) = SS1"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss1_ss2 M"
    by (rule ae_delta_ss1_only[OF rel s_ss1])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss2_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss2: "snd (snd (snd (snd (mt_state c)))) = SS2"
    shows "(c, c') ∈ mttm_step (ae_delta_ss2_ss3 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss2 c_eq have s_ss2: "snd (snd (snd (snd s))) = SS2"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss2_ss3 M"
    by (rule ae_delta_ss2_only[OF rel s_ss2])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss3_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss3: "snd (snd (snd (snd (mt_state c)))) = SS3"
    shows "(c, c') ∈ mttm_step (ae_delta_ss3_ss4 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss3 c_eq have s_ss3: "snd (snd (snd (snd s))) = SS3"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss3_ss4 M"
    by (rule ae_delta_ss3_only[OF rel s_ss3])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss4_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss4: "snd (snd (snd (snd (mt_state c)))) = SS4"
    shows "(c, c') ∈ mttm_step (ae_delta_ss4_ss5 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss4 c_eq have s_ss4: "snd (snd (snd (snd s))) = SS4"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss4_ss5 M"
    by (rule ae_delta_ss4_only[OF rel s_ss4])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss5_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss5: "snd (snd (snd (snd (mt_state c)))) = SS5"
    shows "(c, c') ∈ mttm_step (ae_delta_ss5_ss6 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss5 c_eq have s_ss5: "snd (snd (snd (snd s))) = SS5"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss5_ss6 M"
    by (rule ae_delta_ss5_only[OF rel s_ss5])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss6_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss6: "snd (snd (snd (snd (mt_state c)))) = SS6"
    shows "(c, c') ∈ mttm_step (ae_delta_ss6_ss7 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss6 c_eq have s_ss6: "snd (snd (snd (snd s))) = SS6"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss6_ss7 M"
    by (rule ae_delta_ss6_only[OF rel s_ss6])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss7_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss7: "snd (snd (snd (snd (mt_state c)))) = SS7"
    shows "(c, c') ∈ mttm_step (ae_delta_ss7_ss8 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss7 c_eq have s_ss7: "snd (snd (snd (snd s))) = SS7"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss7_ss8 M"
    by (rule ae_delta_ss7_only[OF rel s_ss7])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

lemma mttm_step_ae_delta_ss8_only:
  fixes M :: "('q, 'a) mttm"
    and c c' :: "('c :: enum ⇒ 'a,
                  'q × ('a, 'c) ae_stage) mt_config"
  assumes step: "(c, c') ∈ mttm_step (alphabet_enlarge_delta M)"
      and ss8: "snd (snd (snd (snd (mt_state c)))) = SS8"
    shows "(c, c') ∈ mttm_step (ae_delta_ss8_ss1 M)"
proof -
  from step obtain s ts n s' a' d where
      c_eq: "c = Config⇩M s ts n"
      and c'_eq: "c' = Config⇩M s' (λk. (ts k)(n k := a' k))
                                    (λk. go_dir (d k) (n k))"
      and rel: "(s, (λk. ts k (n k)), s', a', d)
                  ∈ alphabet_enlarge_delta M"
    by (auto elim: mttm_step.cases)
  from ss8 c_eq have s_ss8: "snd (snd (snd (snd s))) = SS8"
    by simp
  have rel_sub: "(s, (λk. ts k (n k)), s', a', d)
                    ∈ ae_delta_ss8_ss1 M"
    by (rule ae_delta_ss8_only[OF rel s_ss8])
  show ?thesis
    unfolding c_eq c'_eq
    by (rule mttm_step.step[where ts = ts and n = n and a = a' and dir = d,
                            OF rel_sub])
qed

subsubsection ‹Buffered c-fold compute correctness›

text ‹Algebraic correctness of the buffered c-fold compute:
  starting from a 3-block buffer matching a 3c-cell window of
  the M-tape, with M's head at the home block and within the
  non-LE region, the buffered compute simulates M's actual
  c-step trace.  The conclusion exhibits a buffered-compute
  trajectory and a matching M-trace, with the post-state buffer
  / head still satisfying the window invariant.

  Proof skeleton:

  Induction on a step counter ‹i ∈ [0, c]›.

  Base case (‹i = 0›): pre-state matches itself by the
  ‹window› hypothesis.

  Step case (‹i ≤ c›): assume the IH holds at step ‹i›.
  Either M halts at ‹i› (early-stop branch fires;
  ‹q_i ∈ {t, r}›; done), or M takes an ‹(i + 1)›-st step.
  In the second sub-case:

  1. Read symbol from the buffer at IH's ‹bp_i› via
     ‹read_bp›; the window invariant gives this equals
     ‹tsM_i (nM_i)›.
  2. Apply M's ‹δ› (total on non-halting states by
     ‹valid_mttm›) to get ‹(q_{i+1}, a', d)›.
  3. Write ‹a' k› back to the buffer via ‹write_bp›.
  4. Advance ‹bp_i› via ‹bp_advance_le›.  The load-bearing
     claim is that this returns ‹Some bp_{i+1}› (i.e., the
     head doesn't walk off the buffer).  This holds because
     displacement after ‹i + 1› steps is at most ‹i + 1
     ≤ c›, and the buffer covers 3c positions with the
     head starting at home (linearised positions
     ‹[c, 2c-1]›), so the head stays within
     ‹[1, 3c-2] ⊂ [0, 3c-1]›.
  5. Verify the post-state still satisfies the window
     invariant: same ‹p_start›; new ‹bp_{i+1}›;
     buffer's linearised reading at position
     ‹bp_linear bp_{i+1}› agrees with ‹tsM_{i+1}› at
     ‹nM_{i+1}›.

  The step case's load-bearing arithmetic (item 4) is a
  ‹bp_advance_le›-vs-tape-position commutation lemma:
  ‹bp_linear› of the advanced ‹bp› equals the
  linearised tape position relative to ‹p_start›.  This
  sub-lemma is non-trivial but standalone — it doesn't depend
  on M's ‹δ›, only on the encoding's arithmetic.

  The ‹delta_total› precondition rules out the
  stuck-non-halt case: the substrate's ‹δ_set› axiom
  permits non-halting states with no ‹δ›-successor
  (‹δ ⊆ (Q - {t,r}) × ...› is a subset, not an
  equality).  Without this hypothesis the conclusion is
  unprovable: a stuck ‹qM› has no buffered run and is
  non-halt, so neither disjunct of the final claim can hold.
  Hartmanis and Stearns's Theorem 2 implicitly assumes ‹δ› is
  total on ‹Q - {t,r}›; a caller whose machines are total by
  construction discharges this precondition trivially.›


text ‹Per-tape unified companion of ‹ae_coupled_run_aux›,
  ‹_le0›, and ‹_le1›.  Takes a per-tape regime
  selector ‹pos :: nat ⇒ nat› (= ‹mt_pos c' k›
  at the SS4 entry) and the per-tape hybrid window-invariant
  predicate ‹ae_window_invariant_general›, which
  dispatches internally on each tape's regime.  The buffered
  run is the same simultaneous ‹m_step_buffered M›
  relation as the three siblings — the regime selector is
  frozen per tape during the run (‹m_step_buffered›
  has no ‹c'› in scope), so per-tape regime case-splits
  commute with the induction on ‹n›.

  The no-LE hypothesis is per-tape regime-aware: width
  ‹c› for ‹pos = 0›, ‹2c› for
  ‹pos = 1›, ‹3c› for ‹pos ≥ 2›.
  Uniform ‹p_start = (pos - 2) * c + 1› simplifies to
  ‹1› on ‹pos ∈ {0, 1}› by nat arithmetic,
  matching the three siblings' ‹Suc i› shape.

  The post-compute left-slot guard
  (‹fst (buf' k) ≠ LE_block›) is preserved on
  ‹pos = 0› tapes (the generalisation of the le0 chain
  strengthening); le1 tapes have ‹fst (buf k) = LE_block›
  on entry, and steady tapes do not need this property at the
  SS4‹→›SS5 boundary.

  It sits alongside
  ‹ae_coupled_run_aux_le0› and ‹_le1› as
  load-bearing inductive helpers.  Consumer:
  ‹ae_m_steps_buffered_correct_trace_general›, feeding
  ‹ae_step_ss4_ss5_exists_general_trace›, which closes
  the SS4‹→›SS5 trace in
  ‹ae_simulates_forward_stage_general›'s body.›

lemma ae_coupled_run_aux_general:
  fixes M :: "('q, 'a) mttm"
    and qM :: 'q
    and tsM :: "nat ⇒ nat ⇒ 'a"
    and nM :: "nat ⇒ nat"
    and ofs :: "nat ⇒ ('c :: enum)"
    and buf_full :: "nat ⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))"
    and pos :: "nat ⇒ nat"
    and n :: nat
    and cM_n :: "('a, 'q) mt_config"
  assumes vM:        "valid_mttm M"
      and lu:        "le_unique M"
      and qM_in:     "qM ∈ Q_tm M"
      and window:    "∀k<k_tm M. ae_window_invariant_general (tsM k) (nM k)
                            (AE_Home, ofs k) (buf_full k) (pos k) (le_tm M)"
      and pad_home:  "∀k≥k_tm M. fst (snd (buf_full k)) = bl_block (bl_tm M)"
      and trace:     "(Config⇩M qM tsM nM, cM_n)
                        ∈ mttm_step (delta_tm M) ^^ n"
      and n_bound:   "n ≤ card (UNIV :: 'c set)"
      and no_le:
            "∀k. (pos k = 0
                    ⟶ (∀i. i < card (UNIV :: 'c set)
                              ⟶ tsM k (Suc i) ≠ le_tm M))
                 ∧ (pos k = 1
                      ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                                ⟶ tsM k (Suc i) ≠ le_tm M))
                 ∧ (pos k ≥ 2
                      ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                                ⟶ tsM k
                                      ((pos k - 2) * card (UNIV :: 'c set)
                                        + 1 + i)
                                    ≠ le_tm M))"
      and left_not_le_pos0:
            "∀k<k_tm M. pos k = 0 ⟶ fst (buf_full k) ≠ LE_block (le_tm M)"
  shows "∃buf' end_pos.
            ((qM, buf_full, λk. (AE_Home, ofs k)),
             (mt_state cM_n, buf', end_pos))
                ∈ (m_step_buffered M) ^^ n
          ∧ (∀k<k_tm M. ae_window_invariant_general
                    (mt_tape cM_n k) (mt_pos cM_n k)
                    (end_pos k) (buf' k) (pos k) (le_tm M))
          ∧ (∀k. (pos k = 0
                    ⟶ (∀i. i < card (UNIV :: 'c set)
                              ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
                 ∧ (pos k = 1
                      ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                                ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
                 ∧ (pos k ≥ 2
                      ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                                ⟶ mt_tape cM_n k
                                      ((pos k - 2) * card (UNIV :: 'c set)
                                        + 1 + i)
                                    ≠ le_tm M)))
          ∧ (∀k<k_tm M. pos k = 0
                    ⟶ fst (buf' k) ≠ LE_block (le_tm M))
          ∧ (∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos k) + n
                  ∧ bp_linear (end_pos k)
                        < 2 * card (UNIV :: 'c set) + n)
          ∧ (∀k≥k_tm M. fst (snd (buf' k)) = bl_block (bl_tm M)
                  ∧ end_pos k = (AE_Home, ofs k))"
  using trace n_bound
proof (induction n arbitrary: cM_n)
  case 0
  ― ‹Base case: zero ‹M›-steps means ‹cM_n› is the
    initial config, the buffered run is empty, and the four
    output conjuncts hold by direct lifting of the lemma's input
    hypotheses (‹window›, ‹no_le›,
    ‹left_not_le_pos0›) at the unchanged buffered state.
    Witnesses: ‹buf' = buf_full›,
    ‹end_pos = λk. (AE_Home, ofs k)›.›
  from ‹(Config⇩M qM tsM nM, cM_n)
            ∈ mttm_step (delta_tm M) ^^ 0›
  have cM_eq: "cM_n = Config⇩M qM tsM nM" by simp
  hence st: "mt_state cM_n = qM"
    and tp: "mt_tape cM_n = tsM"
    and ps: "mt_pos cM_n = nM" by auto
  show ?case
  proof (intro exI [where x = buf_full]
                exI [where x = "λk. (AE_Home, ofs k)"]
                conjI)
    show "((qM, buf_full, λk. (AE_Home, ofs k)),
            (mt_state cM_n, buf_full, λk. (AE_Home, ofs k)))
              ∈ (m_step_buffered M) ^^ 0"
      using st by simp
    show "∀k<k_tm M. ae_window_invariant_general
                (mt_tape cM_n k) (mt_pos cM_n k)
                ((λk. (AE_Home, ofs k)) k)
                (buf_full k) (pos k) (le_tm M)"
      using window tp ps by simp
    show "∀k. (pos k = 0
                ⟶ (∀i. i < card (UNIV :: 'c set)
                          ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
             ∧ (pos k = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
             ∧ (pos k ≥ 2
                  ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_n k
                                  ((pos k - 2) * card (UNIV :: 'c set)
                                    + 1 + i)
                                ≠ le_tm M))"
      using no_le tp by simp
    show "∀k<k_tm M. pos k = 0
                ⟶ fst (buf_full k) ≠ LE_block (le_tm M)"
      using left_not_le_pos0 .
    show "∀k. card (UNIV :: 'c set)
                ≤ bp_linear ((λk. (AE_Home, ofs k)) k) + 0
              ∧ bp_linear ((λk. (AE_Home, ofs k)) k)
                    < 2 * card (UNIV :: 'c set) + 0"
    proof (intro allI conjI)
      fix k
      have lin: "bp_linear ((λk. (AE_Home, ofs k)) k)
                    = card (UNIV :: 'c set) + c_idx (ofs k)"
        unfolding bp_linear_def by simp
      show "card (UNIV :: 'c set)
              ≤ bp_linear ((λk. (AE_Home, ofs k)) k) + 0"
        using lin by simp
      show "bp_linear ((λk. (AE_Home, ofs k)) k)
              < 2 * card (UNIV :: 'c set) + 0"
        using lin c_idx_lt_card[where x = "ofs k"] by simp
    qed
    show "∀k≥k_tm M. fst (snd (buf_full k)) = bl_block (bl_tm M)
                ∧ (λk. (AE_Home, ofs k)) k = (AE_Home, ofs k)"
      using pad_home by simp
  qed
next
  case (Suc n')
  ― ‹Inductive step: peel the last ‹M›-side step via
    ‹relpow_Suc_E› to obtain an intermediate config
    ‹cM_n'›; apply the IH at ‹n'› to obtain a
    coupled buffered run of length ‹n'›; extend it by one
    ‹m_step_buffered› step mirroring the M-side
    transition; re-establish the four output conjuncts at
    ‹n = Suc n'›.

    The four ingredients are: (i) buffered read matches M-side
    read via window-invariant buf-linearisation; (ii) same
    ‹δ›-tuple drives both sides; (iii)
    ‹bp_advance_le› is total at every reached head
    position (‹no_le› rules out the only None case);
    (iv) window invariant preserved by parallel writes and
    head advances.›
  have n'_bound: "n' ≤ card (UNIV :: 'c set)"
    using Suc.prems(2) by simp
  from Suc.prems(1) obtain cM_n' where
      trace_n': "(Config⇩M qM tsM nM, cM_n')
                    ∈ mttm_step (delta_tm M) ^^ n'"
    and last_step: "(cM_n', cM_n) ∈ mttm_step (delta_tm M)"
    by (rule relpow_Suc_E)
  from Suc.IH[OF trace_n' n'_bound]
  obtain buf_n' end_pos_n' where
      coupled_n':
        "((qM, buf_full, λk. (AE_Home, ofs k)),
          (mt_state cM_n', buf_n', end_pos_n'))
            ∈ (m_step_buffered M) ^^ n'"
    and window_n':
        "∀k<k_tm M. ae_window_invariant_general
                (mt_tape cM_n' k) (mt_pos cM_n' k)
                (end_pos_n' k) (buf_n' k) (pos k) (le_tm M)"
    and no_le_n':
        "∀k. (pos k = 0
                ⟶ (∀i. i < card (UNIV :: 'c set)
                          ⟶ mt_tape cM_n' k (Suc i)
                                ≠ le_tm M))
             ∧ (pos k = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_n' k (Suc i)
                                  ≠ le_tm M))
             ∧ (pos k ≥ 2
                  ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_n' k
                                  ((pos k - 2)
                                      * card (UNIV :: 'c set)
                                    + 1 + i)
                                ≠ le_tm M))"
    and left_n':
        "∀k<k_tm M. pos k = 0
              ⟶ fst (buf_n' k) ≠ LE_block (le_tm M)"
    and bp_bound_n':
        "∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos_n' k) + n'
              ∧ bp_linear (end_pos_n' k)
                    < 2 * card (UNIV :: 'c set) + n'"
    and pad_n':
        "∀k≥k_tm M. fst (snd (buf_n' k)) = bl_block (bl_tm M)
              ∧ end_pos_n' k = (AE_Home, ofs k)"
    by blast
  ― ‹Unpack ‹last_step› via ‹mttm_step.cases›
    into its ‹δ›-tuple ingredients: a state shape
    ‹cM_n' = Config q_pre ts_pre n_pre›, the resulting
    ‹cM_n› as the M-side write + head-advance, and the
    ‹(q_pre, read, q_post, a_step, dir_step)›
    ‹δ›-membership.›
  from last_step obtain q_pre ts_pre n_pre q_post a_step dir_step where
      cM_n'_eq: "cM_n' = Config⇩M q_pre ts_pre n_pre"
    and cM_n_eq:
        "cM_n = Config⇩M q_post
                  (λk. (ts_pre k)(n_pre k := a_step k))
                  (λk. go_dir (dir_step k) (n_pre k))"
    and delta_mem:
        "(q_pre, λk. ts_pre k (n_pre k),
            q_post, a_step, dir_step) ∈ delta_tm M"
    by (rule mttm_step.cases)
  ― ‹Derived closed forms on ‹cM_n'› /
    ‹cM_n›'s components — convenient handles for the
    buffered-side construction in the next increment.›
  have st_n': "mt_state cM_n' = q_pre"
   and tp_n': "mt_tape cM_n' = ts_pre"
   and ps_n': "mt_pos cM_n' = n_pre"
    using cM_n'_eq by auto
  have st_n: "mt_state cM_n = q_post"
   and tp_n: "∀k. mt_tape cM_n k
                    = (ts_pre k)(n_pre k := a_step k)"
   and ps_n: "∀k. mt_pos cM_n k
                    = go_dir (dir_step k) (n_pre k)"
    using cM_n_eq by auto
  ― ‹At this point we have:
    (a) the coupled buffered run of length ‹n'› ending at
        ‹(q_pre, buf_n', end_pos_n')›;
    (b) the four invariants at ‹cM_n'›;
    (c) the M-side ‹δ›-tuple
        ‹(q_pre, read, q_post, a_step, dir_step)›;
    (d) closed forms for ‹cM_n›'s state / tape / pos.›
  ― ‹Ingredient (i) of the inductive step: per-tape
    read-match.  The buffered read at ‹end_pos_n' k›
    equals the M-side read at ‹n_pre k›, via the unified
    ‹read_bp_via_window_general›.›
  have read_match:
      "∀k. read_bp (buf_n' k) (end_pos_n' k) = ts_pre k (n_pre k)"
  proof (intro allI)
    fix k
    show "read_bp (buf_n' k) (end_pos_n' k) = ts_pre k (n_pre k)"
    proof (cases "k < k_tm M")
      case True
      ― ‹Active tape: the read-match is the window invariant's
          buf-linearisation clause projected at the head offset.›
      from window_n'[rule_format, OF True] have wi_k:
          "ae_window_invariant_general
              (mt_tape cM_n' k) (mt_pos cM_n' k)
              (end_pos_n' k) (buf_n' k) (pos k) (le_tm M)" .
      hence wi_k':
          "ae_window_invariant_general
              (ts_pre k) (n_pre k)
              (end_pos_n' k) (buf_n' k) (pos k) (le_tm M)"
        using tp_n' ps_n' by simp
      show ?thesis
        by (rule read_bp_via_window_general[OF wi_k'])
    next
      case False
      ― ‹Padding tape ‹k ≥ k_tm M›: M reads blank
          (‹valid_mttm_delta_support›) and the buffered home block is
          blank with the head parked at home (‹pad_n'›), so both
          sides read ‹bl_tm M›.›
      hence kge: "k_tm M ≤ k" by simp
      from pad_n'[rule_format, OF kge]
      have ph: "fst (snd (buf_n' k)) = bl_block (bl_tm M)"
        and ep: "end_pos_n' k = (AE_Home, ofs k)" by simp_all
      have rd: "ts_pre k (n_pre k) = bl_tm M"
        using valid_mttm_delta_support[OF vM delta_mem kge] by simp
      obtain l h r where blk: "buf_n' k = (l, h, r)"
        by (cases "buf_n' k") auto
      from ph blk have h_eq: "h = bl_block (bl_tm M)" by simp
      have "read_bp (buf_n' k) (end_pos_n' k) = bl_tm M"
        using blk ep h_eq by (simp add: read_bp_def bl_block_def)
      thus ?thesis using rd by simp
    qed
  qed
  ― ‹Per-tape position bounds at step ‹n'›: the fifth
    output conjunct of the IH (‹bp_bound_n'›) plus the
    bound ‹Suc n' ≤ c› (giving ‹n' < c›) yields
    strict bounds ‹bp_linear < 3c - 1› and
    ‹0 < bp_linear› per tape, excluding both None
    configurations of ‹bp_advance›.›
  have c_pos: "1 ≤ card (UNIV :: 'c set)"
    using Suc.prems(2) by linarith
  have bp_lt_max:
      "∀k. bp_linear (end_pos_n' k)
              < 3 * card (UNIV :: 'c set) - 1"
  proof (intro allI)
    fix k
    have lin_lt: "bp_linear (end_pos_n' k) < 2 * card (UNIV :: 'c set) + n'"
      using bp_bound_n' by blast
    show "bp_linear (end_pos_n' k) < 3 * card (UNIV :: 'c set) - 1"
      using lin_lt Suc.prems(2) c_pos by linarith
  qed
  have bp_gt_zero:
      "∀k. 0 < bp_linear (end_pos_n' k)"
  proof (intro allI)
    fix k
    have low: "card (UNIV :: 'c set) ≤ bp_linear (end_pos_n' k) + n'"
      using bp_bound_n' by blast
    show "0 < bp_linear (end_pos_n' k)"
      using low Suc.prems(2) c_pos by linarith
  qed
  ― ‹Ingredient (iii): per-tape ‹bp_advance_le› totality
    at step ‹n'›.  Apply ‹bp_advance_le_total› per tape
    with ‹bp_lt_max›, ‹bp_gt_zero›; lift across tapes
    via choice to obtain the new per-tape head position function
    ‹end_pos_n :: nat ⇒ 'c bp›.›
  have per_tape_total:
      "∀k. ∃p'. bp_advance_le (le_tm M)
                    (ts_pre k (n_pre k))
                    (end_pos_n' k) (dir_step k)
                = Some p'"
  proof (intro allI)
    fix k
    show "∃p'. bp_advance_le (le_tm M)
                  (ts_pre k (n_pre k))
                  (end_pos_n' k) (dir_step k)
              = Some p'"
      by (rule bp_advance_le_total[OF bp_lt_max[rule_format]
                                       bp_gt_zero[rule_format]])
  qed
  from per_tape_total
  have "∃end_pos_n.
            ∀k. bp_advance_le (le_tm M)
                    (ts_pre k (n_pre k))
                    (end_pos_n' k) (dir_step k)
                  = Some (end_pos_n k)"
    by (rule choice)
  then obtain end_pos_n where
      end_pos_n_eq:
        "∀k. bp_advance_le (le_tm M)
                (ts_pre k (n_pre k))
                (end_pos_n' k) (dir_step k)
              = Some (end_pos_n k)"
    by blast
  ― ‹Ingredient (ii): assemble the buffered last step's
    membership in ‹m_step_buffered M›.  Define the new
    buffer ‹buf_n› as the per-tape write-back of
    ‹buf_n'› at ‹end_pos_n'› with ‹a_step›;
    apply the intro rule ‹m_step_bufferedI› with the four
    ingredients (‹delta_mem›, ‹read_match›'s
    reverse, ‹buf_n›'s definitional read-back, and
    ‹end_pos_n_eq›).›
  define buf_n where
    "buf_n = (λk. write_bp (buf_n' k) (end_pos_n' k) (a_step k))"
  have read_match_sym:
      "∀k. ts_pre k (n_pre k) = read_bp (buf_n' k) (end_pos_n' k)"
    using read_match by auto
  have buf_n_def_forall:
      "∀k. buf_n k = write_bp (buf_n' k) (end_pos_n' k) (a_step k)"
    using buf_n_def by simp
  have m_step_last:
      "((q_pre, buf_n', end_pos_n'),
        (q_post, buf_n, end_pos_n))
            ∈ m_step_buffered M"
    by (rule m_step_bufferedI[OF delta_mem read_match_sym
                                  buf_n_def_forall end_pos_n_eq])
  ― ‹Chain extension: bridge ‹coupled_n'›'s endpoint
    ‹(mt_state cM_n', buf_n', end_pos_n')› through
    ‹st_n'› (‹mt_state cM_n' = q_pre›) to match
    ‹m_step_last›'s start, then compose via
    ‹relpow_Suc_I› for a ‹Suc n'›-step buffered run
    ending at ‹(q_post, buf_n, end_pos_n)›.›
  have coupled_n_pre:
      "((qM, buf_full, λk. (AE_Home, ofs k)),
        (q_pre, buf_n', end_pos_n'))
            ∈ (m_step_buffered M) ^^ n'"
    using coupled_n' st_n' by simp
  have coupled_n:
      "((qM, buf_full, λk. (AE_Home, ofs k)),
        (q_post, buf_n, end_pos_n))
            ∈ (m_step_buffered M) ^^ Suc n'"
    using coupled_n_pre m_step_last by (rule relpow_Suc_I)
  ― ‹Conjunct 5 (‹bp_linear› bound at step Suc n'): apply
    the helper ‹bp_advance_le_lin_bounded› per tape.
    Given the IH's conjunct (‹bp_bound_n'›) plus the
    position bounds (‹bp_gt_zero›) plus the advance
    ‹end_pos_n_eq›, the helper closes both bound
    components.›
  have bp_bound_n:
      "∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos_n k) + Suc n'
            ∧ bp_linear (end_pos_n k)
                  < 2 * card (UNIV :: 'c set) + Suc n'"
  proof (intro allI)
    fix k
    show "card (UNIV :: 'c set) ≤ bp_linear (end_pos_n k) + Suc n'
          ∧ bp_linear (end_pos_n k)
                < 2 * card (UNIV :: 'c set) + Suc n'"
      by (rule bp_advance_le_lin_bounded
                  [OF end_pos_n_eq[rule_format, of k]
                      bp_gt_zero[rule_format, of k]
                      conjunct2[OF bp_bound_n'[rule_format, of k]]
                      conjunct1[OF bp_bound_n'[rule_format, of k]]])
  qed
  ― ‹Conjunct 4 (‹left_not_le_pos0› at step Suc n'):
    in ‹pos k = 0› regime, the window invariant excludes
    ‹fst (end_pos_n' k) = AE_Left›, so ‹write_bp›'s
    update doesn't touch the left slot.  Hence
    ‹fst (buf_n k) = fst (buf_n' k)›, and the IH's
    ‹left_n'› closes the goal.›
  have left_n:
      "∀k<k_tm M. pos k = 0
              ⟶ fst (buf_n k) ≠ LE_block (le_tm M)"
  proof (intro allI impI)
    fix k
    assume klt: "k < k_tm M"
    assume pos_0: "pos k = 0"
    from window_n'[rule_format, OF klt] have wi_k:
        "ae_window_invariant_general (mt_tape cM_n' k) (mt_pos cM_n' k)
            (end_pos_n' k) (buf_n' k) (pos k) (le_tm M)" .
    with pos_0 have wi_le0:
        "ae_window_invariant_le0 (mt_tape cM_n' k) (mt_pos cM_n' k)
            (end_pos_n' k) (buf_n' k) (le_tm M)"
      unfolding ae_window_invariant_general_def by simp
    have fst_bp_not_left: "fst (end_pos_n' k) ≠ AE_Left"
    proof (rule ccontr)
      assume "¬ fst (end_pos_n' k) ≠ AE_Left"
      hence "fst (end_pos_n' k) = AE_Left" by simp
      with wi_le0 show False
        unfolding ae_window_invariant_le0_def by simp
    qed
    have fst_buf_n: "fst (buf_n k) = fst (buf_n' k)"
    proof -
      obtain l h r where blocks_eq: "buf_n' k = (l, h, r)"
        by (cases "buf_n' k") auto
      obtain b off where bp_eq: "end_pos_n' k = (b, off)"
        by (cases "end_pos_n' k") auto
      from fst_bp_not_left bp_eq have "b ≠ AE_Left" by simp
      thus ?thesis
        unfolding buf_n_def
        using blocks_eq bp_eq
        by (cases b) (auto simp: write_bp_def)
    qed
    have "fst (buf_n' k) ≠ LE_block (le_tm M)"
      using left_n' pos_0 klt by blast
    thus "fst (buf_n k) ≠ LE_block (le_tm M)"
      using fst_buf_n by simp
  qed
  ― ‹Conjunct 1 (coupled run with ‹mt_state cM_n›
    witness at step Suc n'): re-express ‹coupled_n›'s
    endpoint state from ‹q_post› to ‹mt_state cM_n›
    via ‹st_n›.›
  have coupled_chain:
      "((qM, buf_full, λk. (AE_Home, ofs k)),
        (mt_state cM_n, buf_n, end_pos_n))
            ∈ (m_step_buffered M) ^^ Suc n'"
    using coupled_n st_n by simp
  ― ‹Contrapositive of the substrate axiom
    ‹valid_mttm_deltaLE_no_write›: if M reads non-LE on tape ‹k›
    cell ‹n_pre k›, then it does not write LE on tape ‹k›.
    This is what powers the ‹j = n_pre k› case of conjunct 3:
    the new tape value at the updated cell is ‹a_step k›, and
    we need to show ‹a_step k ≠ le› when the read value was
    in a no-LE window.›
  have no_le_contra:
      "∀k. ts_pre k (n_pre k) ≠ le_tm M
              ⟶ a_step k ≠ le_tm M"
  proof (intro allI impI)
    fix k
    assume rd_not_le: "ts_pre k (n_pre k) ≠ le_tm M"
    show "a_step k ≠ le_tm M"
    proof
      assume a_le: "a_step k = le_tm M"
      have "(λk. ts_pre k (n_pre k)) k = le_tm M"
        by (rule valid_mttm_deltaLE_no_write[OF lu delta_mem a_le])
      hence "ts_pre k (n_pre k) = le_tm M" by simp
      with rd_not_le show False ..
    qed
  qed
  ― ‹Conjunct 3 regime ‹pos k = 0› (no LE in cells
    ‹Suc 0 .. card UNIV›): for each cell ‹Suc i› in
    the window, case-split on whether the M-step's update site
    ‹n_pre k› coincides with ‹Suc i›.

    ‹∙› If not, the fun-update leaves ‹mt_tape cM_n k (Suc i)›
    equal to ‹ts_pre k (Suc i) = mt_tape cM_n' k (Suc i)›;
    the IH (‹no_le_n'›) closes the goal.

    ‹∙› If yes, the new value is ‹a_step k›; the IH gives
    ‹ts_pre k (n_pre k) = ts_pre k (Suc i) ≠ le_tm M›;
    the contrapositive ‹no_le_contra› gives
    ‹a_step k ≠ le_tm M›.›
  have no_le0_n:
      "∀k. pos k = 0
              ⟶ (∀i. i < card (UNIV :: 'c set)
                        ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M)"
  proof (intro allI impI allI impI)
    fix k i
    assume pos_0: "pos k = 0"
       and i_bd: "i < card (UNIV :: 'c set)"
    have ih_at: "ts_pre k (Suc i) ≠ le_tm M"
    proof -
      from no_le_n' pos_0 i_bd
      have "mt_tape cM_n' k (Suc i) ≠ le_tm M" by blast
      thus ?thesis using tp_n' by simp
    qed
    show "mt_tape cM_n k (Suc i) ≠ le_tm M"
    proof (cases "Suc i = n_pre k")
      case False
      hence "mt_tape cM_n k (Suc i) = ts_pre k (Suc i)"
        using tp_n by simp
      thus ?thesis using ih_at by simp
    next
      case True
      hence tape_eq: "mt_tape cM_n k (Suc i) = a_step k"
        using tp_n by simp
      from True have "ts_pre k (n_pre k) = ts_pre k (Suc i)"
        by simp
      with ih_at have "ts_pre k (n_pre k) ≠ le_tm M" by simp
      hence "a_step k ≠ le_tm M" using no_le_contra by blast
      thus ?thesis using tape_eq by simp
    qed
  qed
  ― ‹Conjunct 3 regime ‹pos k = 1›: same window shape
    ‹Suc i› as ‹pos = 0›, but the bound is doubled to
    ‹2 * card UNIV›.  The proof shape is identical;
    only the bound on ‹i› changes.›
  have no_le1_n:
      "∀k. pos k = 1
              ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                        ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M)"
  proof (intro allI impI allI impI)
    fix k i
    assume pos_1: "pos k = 1"
       and i_bd: "i < 2 * card (UNIV :: 'c set)"
    have ih_at: "ts_pre k (Suc i) ≠ le_tm M"
    proof -
      from no_le_n' pos_1 i_bd
      have "mt_tape cM_n' k (Suc i) ≠ le_tm M" by blast
      thus ?thesis using tp_n' by simp
    qed
    show "mt_tape cM_n k (Suc i) ≠ le_tm M"
    proof (cases "Suc i = n_pre k")
      case False
      hence "mt_tape cM_n k (Suc i) = ts_pre k (Suc i)"
        using tp_n by simp
      thus ?thesis using ih_at by simp
    next
      case True
      hence tape_eq: "mt_tape cM_n k (Suc i) = a_step k"
        using tp_n by simp
      from True have "ts_pre k (n_pre k) = ts_pre k (Suc i)"
        by simp
      with ih_at have "ts_pre k (n_pre k) ≠ le_tm M" by simp
      hence "a_step k ≠ le_tm M" using no_le_contra by blast
      thus ?thesis using tape_eq by simp
    qed
  qed
  ― ‹Conjunct 3 regime ‹pos k ≥ 2› (steady regime): the
    no-LE window spans ‹3 * card UNIV› cells starting at
    offset ‹(pos k - 2) * card UNIV + 1›.  The proof shape
    is identical to the ‹pos = 0›/‹pos = 1› cases; only
    the cell expression changes.›
  have no_le2_n:
      "∀k. pos k ≥ 2
              ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                        ⟶ mt_tape cM_n k
                              ((pos k - 2) * card (UNIV :: 'c set) + 1 + i)
                            ≠ le_tm M)"
  proof (intro allI impI allI impI)
    fix k i
    assume pos_ge: "pos k ≥ 2"
       and i_bd: "i < 3 * card (UNIV :: 'c set)"
    let ?j = "(pos k - 2) * card (UNIV :: 'c set) + 1 + i"
    have ih_at: "ts_pre k ?j ≠ le_tm M"
    proof -
      from no_le_n' pos_ge i_bd
      have "mt_tape cM_n' k ?j ≠ le_tm M" by blast
      thus ?thesis using tp_n' by simp
    qed
    show "mt_tape cM_n k ?j ≠ le_tm M"
    proof (cases "?j = n_pre k")
      case False
      hence "mt_tape cM_n k ?j = ts_pre k ?j"
        using tp_n by simp
      thus ?thesis using ih_at by simp
    next
      case True
      hence tape_eq: "mt_tape cM_n k ?j = a_step k"
        using tp_n by simp
      from True have "ts_pre k (n_pre k) = ts_pre k ?j"
        by simp
      with ih_at have "ts_pre k (n_pre k) ≠ le_tm M" by simp
      hence "a_step k ≠ le_tm M" using no_le_contra by blast
      thus ?thesis using tape_eq by simp
    qed
  qed
  ― ‹Conjunct 3 (no-LE invariant at ‹cM_n›): assemble the
    three regime sub-lemmas ‹no_le0_n›, ‹no_le1_n›,
    ‹no_le2_n› into the dispatch-on-‹pos› shape that
    matches the lemma statement.›
  have no_le_n:
      "∀k. (pos k = 0
              ⟶ (∀i. i < card (UNIV :: 'c set)
                        ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
           ∧ (pos k = 1
                ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                          ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
           ∧ (pos k ≥ 2
                ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                          ⟶ mt_tape cM_n k
                                ((pos k - 2) * card (UNIV :: 'c set)
                                  + 1 + i)
                              ≠ le_tm M))"
    using no_le0_n no_le1_n no_le2_n by blast
  ― ‹Conjunct 2 regime ‹pos k ≥ 2› (steady regime): apply
    ‹ae_window_invariant_step› per tape.  Five ingredients:
    the IH-side invariant from ‹window_n'›; the
    ‹bp_advance_le› step from ‹end_pos_n_eq›; the position
    bounds from ‹bp_lt_max› and ‹bp_gt_zero›; and the
    no-LE-at-head fact derived from the IH's ‹no_le_n'›
    instantiated at the buffered-head's linearised offset
    (which lies inside the regime's no-LE window).›
  have win2_n:
      "∀k<k_tm M. pos k ≥ 2
              ⟶ ae_window_invariant
                    (mt_tape cM_n k) (mt_pos cM_n k)
                    (end_pos_n k) (buf_n k)
                    ((pos k - 2) * card (UNIV :: 'c set) + 1)"
  proof (intro allI impI)
    fix k
    assume klt: "k < k_tm M"
    assume pos_ge: "pos k ≥ 2"
    from window_n'[rule_format, OF klt] pos_ge have wi_k:
        "ae_window_invariant (mt_tape cM_n' k) (mt_pos cM_n' k)
              (end_pos_n' k) (buf_n' k)
              ((pos k - 2) * card (UNIV :: 'c set) + 1)"
      unfolding ae_window_invariant_general_def by simp
    hence wi_k': "ae_window_invariant (ts_pre k) (n_pre k)
                    (end_pos_n' k) (buf_n' k)
                    ((pos k - 2) * card (UNIV :: 'c set) + 1)"
      using tp_n' ps_n' by simp
    have adv_k: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
                    (end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
      using end_pos_n_eq by blast
    have bp_lt_k: "bp_linear (end_pos_n' k)
                      < 3 * card (UNIV :: 'c set) - 1"
      using bp_lt_max by blast
    have bp_pos_k: "0 < bp_linear (end_pos_n' k)"
      using bp_gt_zero by blast
    ― ‹No-LE-at-head: ‹n_pre k = (pos k - 2)*c + 1 + j› where
      ‹j = bp_linear (end_pos_n' k) < 3c›; instantiate the
      IH's no-LE window at this ‹j›.›
    have no_le_k: "ts_pre k (n_pre k) ≠ le_tm M"
    proof -
      let ?j = "bp_linear (end_pos_n' k)"
      from wi_k' have head_corr:
          "n_pre k = (pos k - 2) * card (UNIV :: 'c set) + 1 + ?j"
        unfolding ae_window_invariant_def by simp
      have j_lt: "?j < 3 * card (UNIV :: 'c set)"
        by (rule bp_linear_lt_3c)
      from no_le_n' pos_ge j_lt have
          "mt_tape cM_n' k
              ((pos k - 2) * card (UNIV :: 'c set) + 1 + ?j)
            ≠ le_tm M" by blast
      hence "ts_pre k
              ((pos k - 2) * card (UNIV :: 'c set) + 1 + ?j)
            ≠ le_tm M" using tp_n' by simp
      thus ?thesis using head_corr by simp
    qed
    have wi_step:
        "ae_window_invariant
              ((ts_pre k)(n_pre k := a_step k))
              (go_dir (dir_step k) (n_pre k))
              (end_pos_n k)
              (write_bp (buf_n' k) (end_pos_n' k) (a_step k))
              ((pos k - 2) * card (UNIV :: 'c set) + 1)"
      by (rule ae_window_invariant_step
                [OF wi_k' adv_k bp_lt_k bp_pos_k no_le_k])
    show "ae_window_invariant
              (mt_tape cM_n k) (mt_pos cM_n k)
              (end_pos_n k) (buf_n k)
              ((pos k - 2) * card (UNIV :: 'c set) + 1)"
      using wi_step tp_n ps_n buf_n_def by simp
  qed
  ― ‹Conjunct 2 regime ‹pos k = 1› (LE-edge ‹le1›): apply
    ‹ae_window_invariant_le1_step› per tape.  The two LE-aware
    preconditions:

    ‹∙› ‹a_le_k› (‹tM nM = le ⟹ a_step k = le ∧ dir_step k ∈ {N, R}›):
    derived from ‹valid_mttm_deltaLE› applied to ‹delta_mem› at tape ‹k›.

    ‹∙› ‹a_not_le_k› (‹tM nM ≠ le ⟹ a_step k ≠ le›):
    a per-tape instance of ‹no_le_contra› already in scope.

    The ‹no_le_win_k› precondition (no LE in cells ‹1..2c›)
    follows from ‹no_le_n'›'s ‹pos = 1› branch via ‹tp_n'›.›
  have win1_n:
      "∀k<k_tm M. pos k = 1
              ⟶ ae_window_invariant_le1
                    (mt_tape cM_n k) (mt_pos cM_n k)
                    (end_pos_n k) (buf_n k) (le_tm M)"
  proof (intro allI impI)
    fix k
    assume klt: "k < k_tm M"
    assume pos_1: "pos k = 1"
    from window_n'[rule_format, OF klt] pos_1 have wi_k:
        "ae_window_invariant_le1 (mt_tape cM_n' k) (mt_pos cM_n' k)
              (end_pos_n' k) (buf_n' k) (le_tm M)"
      unfolding ae_window_invariant_general_def by simp
    hence wi_k': "ae_window_invariant_le1 (ts_pre k) (n_pre k)
                    (end_pos_n' k) (buf_n' k) (le_tm M)"
      using tp_n' ps_n' by simp
    have adv_k: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
                    (end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
      using end_pos_n_eq by blast
    have bp_lt_k: "bp_linear (end_pos_n' k)
                      < 3 * card (UNIV :: 'c set) - 1"
      using bp_lt_max by blast
    have bp_pos_k: "0 < bp_linear (end_pos_n' k)"
      using bp_gt_zero by blast
    have a_le_k:
        "ts_pre k (n_pre k) = le_tm M
            ⟹ a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
    proof -
      assume rd_le: "ts_pre k (n_pre k) = le_tm M"
      have "a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
        by (rule valid_mttm_deltaLE[OF vM delta_mem, of k, OF rd_le])
      thus "a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}" .
    qed
    have a_not_le_k:
        "ts_pre k (n_pre k) ≠ le_tm M ⟹ a_step k ≠ le_tm M"
      using no_le_contra by blast
    have no_le_win_k:
        "∀i. 0 < i ∧ i ≤ 2 * card (UNIV :: 'c set)
                  ⟶ ts_pre k i ≠ le_tm M"
    proof (intro allI impI)
      fix i
      assume i_bd: "0 < i ∧ i ≤ 2 * card (UNIV :: 'c set)"
      obtain j where j_eq: "i = Suc j" using i_bd by (cases i) auto
      have j_lt: "j < 2 * card (UNIV :: 'c set)"
        using i_bd j_eq by simp
      from no_le_n' pos_1 j_lt
      have "mt_tape cM_n' k (Suc j) ≠ le_tm M" by blast
      thus "ts_pre k i ≠ le_tm M" using tp_n' j_eq by simp
    qed
    have wi_step:
        "ae_window_invariant_le1
              ((ts_pre k)(n_pre k := a_step k))
              (go_dir (dir_step k) (n_pre k))
              (end_pos_n k)
              (write_bp (buf_n' k) (end_pos_n' k) (a_step k))
              (le_tm M)"
      by (rule ae_window_invariant_le1_step
                [OF wi_k' adv_k bp_lt_k bp_pos_k
                    a_le_k a_not_le_k no_le_win_k])
    show "ae_window_invariant_le1
              (mt_tape cM_n k) (mt_pos cM_n k)
              (end_pos_n k) (buf_n k) (le_tm M)"
      using wi_step tp_n ps_n buf_n_def by simp
  qed
  ― ‹Conjunct 2 regime ‹pos k = 0› (LE-edge ‹le0›): apply
    ‹ae_window_invariant_le0_step› per tape.  Pattern identical
    to the ‹pos = 1› call; only the lemma and the no-LE
    window range (cells ‹1..c›) differ.›
  have win0_n:
      "∀k<k_tm M. pos k = 0
              ⟶ ae_window_invariant_le0
                    (mt_tape cM_n k) (mt_pos cM_n k)
                    (end_pos_n k) (buf_n k) (le_tm M)"
  proof (intro allI impI)
    fix k
    assume klt: "k < k_tm M"
    assume pos_0: "pos k = 0"
    from window_n'[rule_format, OF klt] pos_0 have wi_k:
        "ae_window_invariant_le0 (mt_tape cM_n' k) (mt_pos cM_n' k)
              (end_pos_n' k) (buf_n' k) (le_tm M)"
      unfolding ae_window_invariant_general_def by simp
    hence wi_k': "ae_window_invariant_le0 (ts_pre k) (n_pre k)
                    (end_pos_n' k) (buf_n' k) (le_tm M)"
      using tp_n' ps_n' by simp
    have adv_k: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
                    (end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
      using end_pos_n_eq by blast
    have bp_lt_k: "bp_linear (end_pos_n' k)
                      < 3 * card (UNIV :: 'c set) - 1"
      using bp_lt_max by blast
    have bp_pos_k: "0 < bp_linear (end_pos_n' k)"
      using bp_gt_zero by blast
    have a_le_k:
        "ts_pre k (n_pre k) = le_tm M
            ⟹ a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
    proof -
      assume rd_le: "ts_pre k (n_pre k) = le_tm M"
      show "a_step k = le_tm M ∧ dir_step k ∈ {dir.N, dir.R}"
        by (rule valid_mttm_deltaLE[OF vM delta_mem, of k, OF rd_le])
    qed
    have a_not_le_k:
        "ts_pre k (n_pre k) ≠ le_tm M ⟹ a_step k ≠ le_tm M"
      using no_le_contra by blast
    have no_le_win_k:
        "∀i. 0 < i ∧ i ≤ card (UNIV :: 'c set)
                  ⟶ ts_pre k i ≠ le_tm M"
    proof (intro allI impI)
      fix i
      assume i_bd: "0 < i ∧ i ≤ card (UNIV :: 'c set)"
      obtain j where j_eq: "i = Suc j" using i_bd by (cases i) auto
      have j_lt: "j < card (UNIV :: 'c set)"
        using i_bd j_eq by simp
      from no_le_n' pos_0 j_lt
      have "mt_tape cM_n' k (Suc j) ≠ le_tm M" by blast
      thus "ts_pre k i ≠ le_tm M" using tp_n' j_eq by simp
    qed
    have wi_step:
        "ae_window_invariant_le0
              ((ts_pre k)(n_pre k := a_step k))
              (go_dir (dir_step k) (n_pre k))
              (end_pos_n k)
              (write_bp (buf_n' k) (end_pos_n' k) (a_step k))
              (le_tm M)"
      by (rule ae_window_invariant_le0_step
                [OF wi_k' adv_k bp_lt_k bp_pos_k
                    a_le_k a_not_le_k no_le_win_k])
    show "ae_window_invariant_le0
              (mt_tape cM_n k) (mt_pos cM_n k)
              (end_pos_n k) (buf_n k) (le_tm M)"
      using wi_step tp_n ps_n buf_n_def by simp
  qed
  ― ‹Conjunct 2 (window invariant at ‹cM_n›): assemble the
    three regime sub-lemmas ‹win0_n›, ‹win1_n›,
    ‹win2_n› into the dispatch-on-‹pos› shape that
    matches the lemma statement
    (‹ae_window_invariant_general›).›
  have window_n:
      "∀k<k_tm M. ae_window_invariant_general
              (mt_tape cM_n k) (mt_pos cM_n k)
              (end_pos_n k) (buf_n k) (pos k) (le_tm M)"
  proof (intro allI impI)
    fix k
    assume klt: "k < k_tm M"
    show "ae_window_invariant_general
            (mt_tape cM_n k) (mt_pos cM_n k)
            (end_pos_n k) (buf_n k) (pos k) (le_tm M)"
      unfolding ae_window_invariant_general_def
      using win0_n win1_n win2_n klt by blast
  qed
  ― ‹Padding shadow invariant at step ‹Suc n'›: empty
    tapes ‹k ≥ k_tm M› keep a blank home block and a head
    parked at ‹(AE_Home, ofs k)›.  Preserved from the IH's
    ‹pad_n'› by the M-step's ‹δ›-support (‹read = a' = bl›,
    ‹d = N› past tape count): the head stays put under ‹bp_advance›
    of a ‹dir.N› step, and writing ‹bl› into the blank home
    is idempotent.›
  have pad_n:
      "∀k≥k_tm M. fst (snd (buf_n k)) = bl_block (bl_tm M)
              ∧ end_pos_n k = (AE_Home, ofs k)"
  proof (intro allI impI)
    fix k
    assume kge: "k_tm M ≤ k"
    from pad_n'[rule_format, OF kge]
    have ph: "fst (snd (buf_n' k)) = bl_block (bl_tm M)"
      and ep: "end_pos_n' k = (AE_Home, ofs k)" by simp_all
    from valid_mttm_delta_support[OF vM delta_mem kge]
    have rd: "ts_pre k (n_pre k) = bl_tm M"
      and wr: "a_step k = bl_tm M"
      and dr: "dir_step k = dir.N" by simp_all
    have ep_n: "end_pos_n k = (AE_Home, ofs k)"
    proof -
      have adv: "bp_advance_le (le_tm M) (ts_pre k (n_pre k))
                    (end_pos_n' k) (dir_step k) = Some (end_pos_n k)"
        using end_pos_n_eq by blast
      have "bp_advance_le (le_tm M) (bl_tm M) (AE_Home, ofs k) dir.N
              = Some (AE_Home, ofs k)"
        by (simp add: bp_advance_le_def bp_advance_def)
      thus ?thesis using adv rd ep dr by simp
    qed
    have buf_n_k: "fst (snd (buf_n k)) = bl_block (bl_tm M)"
    proof -
      obtain l h r where blk: "buf_n' k = (l, h, r)"
        by (cases "buf_n' k") auto
      from ph blk have h_eq: "h = bl_block (bl_tm M)" by simp
      have "buf_n k = (l, h(ofs k := bl_tm M), r)"
        using blk ep wr by (simp add: buf_n_def write_bp_def)
      hence "fst (snd (buf_n k)) = h(ofs k := bl_tm M)" by simp
      also have "… = bl_block (bl_tm M)"
        using h_eq by (simp add: bl_block_def fun_eq_iff)
      finally show ?thesis .
    qed
    show "fst (snd (buf_n k)) = bl_block (bl_tm M)
            ∧ end_pos_n k = (AE_Home, ofs k)"
      using buf_n_k ep_n by simp
  qed
  ― ‹Final ‹show ?case› assembly: package the five
    discharged conjuncts (‹coupled_chain›, ‹window_n›,
    ‹no_le_n›, ‹left_n›, ‹bp_bound_n›) into the
    existential output via ‹buf_n› and ‹end_pos_n›.›
  show ?case
  proof (intro exI [where x = buf_n] exI [where x = end_pos_n] conjI)
    show "((qM, buf_full, λk. (AE_Home, ofs k)),
            (mt_state cM_n, buf_n, end_pos_n))
              ∈ (m_step_buffered M) ^^ Suc n'"
      by (rule coupled_chain)
    show "∀k<k_tm M. ae_window_invariant_general
                (mt_tape cM_n k) (mt_pos cM_n k)
                (end_pos_n k) (buf_n k) (pos k) (le_tm M)"
      by (rule window_n)
    show "∀k. (pos k = 0
                ⟶ (∀i. i < card (UNIV :: 'c set)
                          ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
             ∧ (pos k = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_n k (Suc i) ≠ le_tm M))
             ∧ (pos k ≥ 2
                  ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_n k
                                  ((pos k - 2) * card (UNIV :: 'c set)
                                    + 1 + i)
                                ≠ le_tm M))"
      by (rule no_le_n)
    show "∀k<k_tm M. pos k = 0
                ⟶ fst (buf_n k) ≠ LE_block (le_tm M)"
      by (rule left_n)
    show "∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos_n k) + Suc n'
              ∧ bp_linear (end_pos_n k)
                    < 2 * card (UNIV :: 'c set) + Suc n'"
      by (rule bp_bound_n)
    show "∀k≥k_tm M. fst (snd (buf_n k)) = bl_block (bl_tm M)
                ∧ end_pos_n k = (AE_Home, ofs k)"
      by (rule pad_n)
  qed
qed


text ‹Per-tape unified companion of
  ‹ae_m_steps_buffered_correct_trace›, ‹_le0›, and
  ‹_le1›.  A wrapper over
  ‹ae_coupled_run_aux_general›: builds the
  ‹m_steps_buffered› step (= relpow plus
  ‹kM ≤ c› and end-or-halt) and re-packages the aux's
  existential into an ‹obtains›-style witness.

  The hypothesis shape matches the three siblings' wrapper
  pattern: a per-tape regime selector ‹pos›, the per-tape
  hybrid window invariant, the per-tape regime-guarded
  ‹no_le›, and the ‹pos = 0›-conditional left-slot
  guard.  Output conjuncts mirror the input, with the buffered
  config existentially bound.›

lemma ae_m_steps_buffered_correct_trace_general:
  fixes M :: "('q, 'a) mttm"
    and qM :: 'q
    and tsM :: "nat ⇒ nat ⇒ 'a"
    and nM :: "nat ⇒ nat"
    and ofs :: "nat ⇒ ('c :: enum)"
    and buf_full :: "nat ⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))"
    and pos :: "nat ⇒ nat"
    and kM :: nat
    and cM_k :: "('a, 'q) mt_config"
  assumes vM:        "valid_mttm M"
      and lu:        "le_unique M"
      and qM_in:     "qM ∈ Q_tm M"
      and window:    "∀k<k_tm M. ae_window_invariant_general (tsM k) (nM k)
                            (AE_Home, ofs k) (buf_full k) (pos k) (le_tm M)"
      and pad_home:  "∀k≥k_tm M. fst (snd (buf_full k)) = bl_block (bl_tm M)"
      and no_le:
            "∀k. (pos k = 0
                    ⟶ (∀i. i < card (UNIV :: 'c set)
                              ⟶ tsM k (Suc i) ≠ le_tm M))
                 ∧ (pos k = 1
                      ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                                ⟶ tsM k (Suc i) ≠ le_tm M))
                 ∧ (pos k ≥ 2
                      ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                                ⟶ tsM k
                                      ((pos k - 2) * card (UNIV :: 'c set)
                                        + 1 + i)
                                    ≠ le_tm M))"
      and trace:     "(Config⇩M qM tsM nM, cM_k)
                        ∈ mttm_step (delta_tm M) ^^ kM"
      and kM_le:     "kM ≤ card (UNIV :: 'c set)"
      and end_or_halt:
            "kM = card (UNIV :: 'c set)
              ∨ mt_state cM_k ∈ {t_tm M, r_tm M}"
      and left_not_le_pos0:
            "∀k<k_tm M. pos k = 0 ⟶ fst (buf_full k) ≠ LE_block (le_tm M)"
  obtains q_out buf' end_pos where
      "((qM, buf_full, λk. (AE_Home, ofs k)),
         (q_out, buf', end_pos)) ∈ m_steps_buffered M"
    and "q_out = mt_state cM_k"
    and "∀k<k_tm M. ae_window_invariant_general
              (mt_tape cM_k k) (mt_pos cM_k k)
              (end_pos k) (buf' k) (pos k) (le_tm M)"
    and "∀k. (pos k = 0
                ⟶ (∀i. i < card (UNIV :: 'c set)
                          ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
             ∧ (pos k = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
             ∧ (pos k ≥ 2
                  ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k
                                  ((pos k - 2) * card (UNIV :: 'c set)
                                    + 1 + i)
                                ≠ le_tm M))"
    and "∀k<k_tm M. pos k = 0
              ⟶ fst (buf' k) ≠ LE_block (le_tm M)"
proof -
  have ae_result_general:
      "∃buf' end_pos.
          ((qM, buf_full, λk. (AE_Home, ofs k)),
           (mt_state cM_k, buf', end_pos))
              ∈ (m_step_buffered M) ^^ kM
        ∧ (∀k<k_tm M. ae_window_invariant_general
                  (mt_tape cM_k k) (mt_pos cM_k k)
                  (end_pos k) (buf' k) (pos k) (le_tm M))
        ∧ (∀k. (pos k = 0
                  ⟶ (∀i. i < card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
               ∧ (pos k = 1
                    ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                              ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
               ∧ (pos k ≥ 2
                    ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                              ⟶ mt_tape cM_k k
                                    ((pos k - 2) * card (UNIV :: 'c set)
                                      + 1 + i)
                                  ≠ le_tm M)))
        ∧ (∀k<k_tm M. pos k = 0
                  ⟶ fst (buf' k) ≠ LE_block (le_tm M))
        ∧ (∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos k) + kM
                ∧ bp_linear (end_pos k)
                      < 2 * card (UNIV :: 'c set) + kM)
        ∧ (∀k≥k_tm M. fst (snd (buf' k)) = bl_block (bl_tm M)
                ∧ end_pos k = (AE_Home, ofs k))"
    by (rule ae_coupled_run_aux_general[OF vM lu qM_in window pad_home trace kM_le
                                           no_le left_not_le_pos0])
  obtain buf' end_pos where
      coupled: "((qM, buf_full, λk. (AE_Home, ofs k)),
                 (mt_state cM_k, buf', end_pos))
                    ∈ (m_step_buffered M) ^^ kM"
    and new_window:
        "∀k<k_tm M. ae_window_invariant_general
              (mt_tape cM_k k) (mt_pos cM_k k)
              (end_pos k) (buf' k) (pos k) (le_tm M)"
    and post_no_le:
        "∀k. (pos k = 0
                ⟶ (∀i. i < card (UNIV :: 'c set)
                          ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
             ∧ (pos k = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
             ∧ (pos k ≥ 2
                  ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k
                                  ((pos k - 2) * card (UNIV :: 'c set)
                                    + 1 + i)
                                ≠ le_tm M))"
    and post_left_not_le_pos0:
        "∀k<k_tm M. pos k = 0
              ⟶ fst (buf' k) ≠ LE_block (le_tm M)"
    and bp_bound:
        "∀k. card (UNIV :: 'c set) ≤ bp_linear (end_pos k) + kM
              ∧ bp_linear (end_pos k)
                    < 2 * card (UNIV :: 'c set) + kM"
    using ae_result_general by blast
  have buffered_full:
      "((qM, buf_full, λk. (AE_Home, ofs k)),
        (mt_state cM_k, buf', end_pos)) ∈ m_steps_buffered M"
    unfolding m_steps_buffered_def
    using coupled kM_le end_or_halt by auto
  show thesis
  proof (rule that[where q_out = "mt_state cM_k"
                     and buf' = buf' and end_pos = end_pos])
    show "((qM, buf_full, λk. (AE_Home, ofs k)),
           (mt_state cM_k, buf', end_pos)) ∈ m_steps_buffered M"
      using buffered_full .
    show "mt_state cM_k = mt_state cM_k" by (rule refl)
    show "∀k<k_tm M. ae_window_invariant_general
              (mt_tape cM_k k) (mt_pos cM_k k)
              (end_pos k) (buf' k) (pos k) (le_tm M)"
      using new_window .
    show "∀k. (pos k = 0
                ⟶ (∀i. i < card (UNIV :: 'c set)
                          ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
             ∧ (pos k = 1
                  ⟶ (∀i. i < 2 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k (Suc i) ≠ le_tm M))
             ∧ (pos k ≥ 2
                  ⟶ (∀i. i < 3 * card (UNIV :: 'c set)
                            ⟶ mt_tape cM_k k
                                  ((pos k - 2) * card (UNIV :: 'c set)
                                    + 1 + i)
                                ≠ le_tm M))"
      using post_no_le .
    show "∀k<k_tm M. pos k = 0
                ⟶ fst (buf' k) ≠ LE_block (le_tm M)"
      using post_left_not_le_pos0 .
  qed
qed

end