Theory Multitape_Alphabet_Enlargement.AlphabetEnlargement_Substeps
theory AlphabetEnlargement_Substeps
imports AlphabetEnlargement_Defs
begin
subsection ‹Per-substep transition relations›
text ‹‹δ'› is decomposed into named per-substep relations for the
validation and simulation phases. Validation: 8 relations
(forward LE-skip / pure / padded / non-canonical-reject /
end-of-input; padded end-of-input / padded-reject; return
step / return-LE-to-Sim). Simulation: 8 relations
(SS1‹→›SS2, ‹…›, SS7‹→›SS8, SS8‹→›SS1).
Total: 16 relations.
The substrate transition shape is
‹(q, a, q', a', d)› with state ‹'q × ae_stage›, tape
symbol ‹'c ⇒ 'a›. Source-state constraint
‹q ∈ Q ∧ q ≠ t ∧ q ≠ r› matches substrate ‹δ_set›
for VFwd-source relations (whose ‹substep_idx› coincides with
‹t', r'›'s); for the other phases the ‹substep_idx› mismatch
itself rules out source = ‹t'› / ‹r'›.›
text ‹Validation, VFwd, advance: read either ‹LE_block le_M›
(initial step from position 0) or a pure block
(no blanks); R move on tape 0; N moves on other tapes;
phase stays ‹VFwd›. No write change.›
definition ae_delta_val_fwd_advance ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_fwd_advance M =
{((q, ofs, buf, dest, VFwd), a,
(q, ofs, buf, dest, VFwd), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ (a 0 = LE_block (le_tm M)
∨ is_pure_block (bl_tm M) (a 0))
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λk. if k = 0 then dir.R else dir.N)}"
text ‹Validation, VFwd ‹→› VFwdPad: read a trailing-padded
block on tape 0; R move on tape 0; N moves on other
tapes; phase becomes VFwdPad. No write change.›
definition ae_delta_val_fwd_to_padded ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_fwd_to_padded M =
{((q, ofs, buf, dest, VFwd), a,
(q, ofs, buf, dest, VFwdPad), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ is_padded_block (bl_tm M) (a 0)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λk. if k = 0 then dir.R else dir.N)}"
text ‹Validation, VFwd reject: read a non-canonical block
on tape 0 (in ‹Σ'› but neither pure nor padded — blanks in
non-trailing positions); N moves uniformly; transition to
‹r_M'› (= the canonical reject state of ‹M'›).›
definition ae_delta_val_fwd_reject ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_fwd_reject M =
{((q, ofs, buf, dest, VFwd), a,
(r_tm M, init_stage (le_tm M)), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ a 0 ≠ LE_block (le_tm M)
∧ a 0 ≠ bl_block (bl_tm M)
∧ ¬ is_canonical_block (bl_tm M) (a 0)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λ_. dir.N)}"
text ‹Validation, VFwd end-of-input: read ‹bl_block bl_M›
(past the encoded input); N moves; transition to VRet to
begin the return scan.›
definition ae_delta_val_fwd_to_ret ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_fwd_to_ret M =
{((q, ofs, buf, dest, VFwd), a,
(q, ofs, buf, dest, VRet), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ a 0 = bl_block (bl_tm M)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λ_. dir.N)}"
text ‹Validation, VFwdPad end-of-input: read ‹bl_block bl_M›;
N moves; transition to VRet. Same as the VFwd version
except the source phase.›
definition ae_delta_val_pad_to_ret ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_pad_to_ret M =
{((q, ofs, buf, dest, VFwdPad), a,
(q, ofs, buf, dest, VRet), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M
∧ a 0 = bl_block (bl_tm M)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λ_. dir.N)}"
text ‹Validation, VFwdPad reject: read anything on tape 0 other
than ‹bl_block bl_M›. This signals a non-blank block
appearing after the trailing-padded block. N moves;
transition to ‹r_M'›.›
definition ae_delta_val_pad_reject ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_pad_reject M =
{((q, ofs, buf, dest, VFwdPad), a,
(r_tm M, init_stage (le_tm M)), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M
∧ a 0 ≠ bl_block (bl_tm M)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λ_. dir.N)}"
text ‹Validation, VRet step: read a non-LE block on tape 0
(during the return scan); L move on tape 0; N moves on other
tapes; phase stays VRet.›
definition ae_delta_val_ret_step ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_ret_step M =
{((q, ofs, buf, dest, VRet), a,
(q, ofs, buf, dest, VRet), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M
∧ a 0 ≠ LE_block (le_tm M)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λk. if k = 0 then dir.L else dir.N)}"
text ‹Validation, VRet ‹→› Sim: read ‹LE_block le_M› on tape 0
(return scan reached position 0); N moves uniformly (head
stays at position 0, the LE-block); phase becomes Sim with
‹substep_idx› = SS1.
The N move on tape 0 — rather than R — leaves ‹M'›'s head at
block 0 (‹LE_M'›) post-validation, so the simulation
phase's first stage runs in LE-stage mode
(‹home = LE_M'›) and the c-fold compute correctly simulates
‹M›'s first step from ‹(s_M, LE)›. See ‹bp_advance_le›
below for how the c-fold compute handles M's first R-move out
of LE.›
definition ae_delta_val_ret_to_sim ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_val_ret_to_sim M =
{((q, ofs, buf, dest, VRet), a,
(q, ofs, buf, dest, SS1), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M
∧ a 0 = LE_block (le_tm M)
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λ_. dir.N)}"
text ‹SS1 ‹→› SS2: read home into buffer; per-tape move L
(steady-state) or N (LE-stage). No write change
(‹a' = a›); no ‹M›-state advance. Buffer-phase substep 1.›
definition ae_delta_ss1_ss2 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss1_ss2 M =
{((q, ofs, buf, dest, SS1), a,
(q, ofs, buf', dest, SS2), a, d) |
q ofs buf dest a buf' d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ buf' = (λk. if k < k_tm M
then (fst (buf k), a k, snd (snd (buf k)))
else init_buffer (le_tm M) k)
∧ d = (λk. if k < k_tm M
then (if a k = LE_block (le_tm M) then dir.N else dir.L)
else dir.N)}"
text ‹SS2 ‹→› SS3: read left into buffer (or placeholder for
LE-stage); per-tape move R (steady-state, returning to home)
or N (LE-stage, staying at home). Buffer-phase substep 2.
In LE-stage (‹buf k.home = LE_M'›), the read is again
‹LE_M'› (head didn't move at SS1) and ‹buf' k.left› is set to
‹bl_block bl_M› as a semantic placeholder.›
definition ae_delta_ss2_ss3 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss2_ss3 M =
{((q, ofs, buf, dest, SS2), a,
(q, ofs, buf', dest, SS3), a, d) |
q ofs buf dest a buf' d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ buf' = (λk. if k < k_tm M
then (let (l, h, r) = buf k in
(if h = LE_block (le_tm M)
then bl_block (bl_tm M)
else a k,
h, r))
else init_buffer (le_tm M) k)
∧ d = (λk. if k < k_tm M
then (if (fst (snd (buf k))) = LE_block (le_tm M)
then dir.N else dir.R)
else dir.N)}"
text ‹SS3 ‹→› SS4: uniform R move per tape (no buffer update,
no ‹M›-state advance). Both steady-state and LE-stage move
R (steady-state from home to right; LE-stage from home (= LE)
to right neighbour, satisfying ‹δLE› since R is allowed
from LE). Buffer-phase substep 3.›
definition ae_delta_ss3_ss4 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss3_ss4 M =
{((q, ofs, buf, dest, SS3), a,
(q, ofs, buf, dest, SS4), a, d) |
q ofs buf dest a d.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ d = (λk. if k < k_tm M then dir.R else dir.N)}"
text ‹Buffered head position: which buffer slot
(‹AE_Left› / ‹AE_Home› / ‹AE_Right›) and which offset
within that slot. Internal to the compute substep; the
output of ‹m_steps_buffered› projects this onto
‹(nat ⇒ 'c) × (nat ⇒ ae_dest)›.›
type_synonym 'c bp = "ae_dest × 'c"
text ‹Read the symbol at a buffered head position.›
definition read_bp ::
"(('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ 'c bp ⇒ 'a" where
"read_bp blocks p =
(let (b, off) = p; (l, h, r) = blocks in
case b of AE_Left ⇒ l off
| AE_Home ⇒ h off
| AE_Right ⇒ r off)"
text ‹Write a symbol at a buffered head position.›
definition write_bp ::
"(('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ 'c bp ⇒ 'a
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))" where
"write_bp blocks p x =
(let (b, off) = p; (l, h, r) = blocks in
case b of AE_Left ⇒ (l(off := x), h, r)
| AE_Home ⇒ (l, h(off := x), r)
| AE_Right ⇒ (l, h, r(off := x)))"
text ‹Advance a buffered head position by a direction. Returns
‹None› if the head would exit the 3-block buffer (which by the
per-‹c›-step head-displacement bound of Hopcroft--Ullman
\<^cite>‹‹Theorem 12.3› in "Hopcroft1979:introduction"› cannot
happen during a single ‹c›-step compute starting from
‹(AE_Home, ofs)›; relations using ‹bp_advance› filter the
‹None› case as a vacuous side condition).›
definition bp_advance ::
"('c :: enum) bp ⇒ dir ⇒ 'c bp option" where
"bp_advance p d =
(let (b, off) = p in
case d of
dir.N ⇒ Some (b, off)
| dir.R ⇒
(case c_succ off of
Some off' ⇒ Some (b, off')
| None ⇒
(case b of
AE_Left ⇒ Some (AE_Home, c_first)
| AE_Home ⇒ Some (AE_Right, c_first)
| AE_Right ⇒ None))
| dir.L ⇒
(case c_pred off of
Some off' ⇒ Some (b, off')
| None ⇒
(case b of
AE_Right ⇒ Some (AE_Home, c_last)
| AE_Home ⇒ Some (AE_Left, c_last)
| AE_Left ⇒ None)))"
text ‹LE-aware buffered head advance. Wraps ‹bp_advance›
with the substrate-induced LE-skip rule: when the read symbol
is ‹le› (i.e., the head is positioned within an ‹LE_M'›
block) and the move is R, jump to ‹(AE_Right, c_first)›
rather than advancing within the home block. This corresponds
to ‹M›'s actual head crossing from position 0 (LE) to
position 1 (the first input cell), which the simulation
correspondence requires as a single bp-step rather than a
sequence of c within-block bp-steps.
Rationale: the
‹LE_M'› block is a c-tuple but only its slot 0 represents
a real ‹M›-cell; slots 1..c-1 are structural padding.
‹bp_advance›'s standard offset arithmetic would walk through
these padding slots, which doesn't correspond to any
‹M›-step. N stays in place (consistent with ‹M›
staying at LE on N), L is forbidden by ‹δLE› at LE so
the case is unreachable.›
definition bp_advance_le ::
"'a ⇒ 'a ⇒ ('c :: enum) bp ⇒ dir ⇒ 'c bp option" where
"bp_advance_le le a p d =
(if a = le ∧ fst p = AE_Home ∧ d = dir.R
then Some (AE_Right, c_first)
else bp_advance p d)"
text ‹Single buffered ‹M›-step: applies ‹M›'s ‹δ› to the
current per-tape buffered reads, writes the post-symbols
back into the buffer, and advances each per-tape head
position via ‹bp_advance_le› (the LE-aware wrapper around
‹bp_advance›). The relation is empty
for configurations whose source ‹M›-state is halting
(‹M›'s ‹δ› excludes those) or whose head movement would
exit the 3-block buffer on any tape.›
definition m_step_buffered ::
"('q, 'a) mttm
⇒ (('q
× (nat ⇒ ('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
× (nat ⇒ 'c bp))
× ('q
× (nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
× (nat ⇒ 'c bp))) set" where
"m_step_buffered M =
{((q, blocks, pos), (q', blocks', pos')) |
q blocks pos q' blocks' pos' a a' d.
(q, a, q', a', d) ∈ delta_tm M
∧ (∀k. a k = read_bp (blocks k) (pos k))
∧ (∀k. blocks' k = write_bp (blocks k) (pos k) (a' k))
∧ (∀k. bp_advance_le (le_tm M) (a k) (pos k) (d k)
= Some (pos' k))}"
text ‹Introduction rule for ‹m_step_buffered›: package the
four ingredients (‹δ›-tuple, read-from-buffer match,
write-back, head-advance) into the relational membership
claim. Used by the inductive step of
‹ae_m_steps_buffered_correct› (‹AlphabetEnlargement.thy›)
to extend a coupled run by one step.›
lemma m_step_bufferedI:
fixes M :: "('q, 'a) mttm"
and a a' :: "nat ⇒ 'a"
and d :: "nat ⇒ dir"
and blocks blocks' ::
"nat ⇒ (('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))"
and pos pos' :: "nat ⇒ 'c bp"
assumes "(q, a, q', a', d) ∈ delta_tm M"
and "∀k. a k = read_bp (blocks k) (pos k)"
and "∀k. blocks' k = write_bp (blocks k) (pos k) (a' k)"
and "∀k. bp_advance_le (le_tm M) (a k) (pos k) (d k)
= Some (pos' k)"
shows "((q, blocks, pos), (q', blocks', pos')) ∈ m_step_buffered M"
using assms unfolding m_step_buffered_def by blast
text ‹Auxiliary: up-to-‹c›-step composition of ‹M›'s ‹δ› on
the buffered representation. Captures the cumulative effect
of either ‹c› consecutive ‹M›-steps, or fewer if ‹M›
reaches a halting state (‹t_M› / ‹r_M›) earlier.
Defined as the union of ‹n›-fold relational compositions of
‹m_step_buffered M› for ‹n ≤ c = card (UNIV :: 'c set)›,
filtered to enforce the early-stop discipline (the run runs
the full ‹c› steps unless ‹M› halts). This is the
semantic core of the compute substep (SS4‹→›SS5).›
definition m_steps_buffered ::
"('q, 'a) mttm
⇒ (('q
× (nat ⇒ ('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
× (nat ⇒ 'c bp))
× ('q
× (nat ⇒ ('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
× (nat ⇒ 'c bp))) set" where
"m_steps_buffered M =
{(s, s') | s s' n.
n ≤ card (UNIV :: 'c set)
∧ (s, s') ∈ (m_step_buffered M) ^^ n
∧ (n = card (UNIV :: 'c set)
∨ fst s' ∈ {t_tm M, r_tm M})}"
text ‹Functionality of ‹m_step_buffered› under
‹det_mttm M›: a single buffered M-step from a fixed source
determines the target uniquely. Threaded through
‹m_step_buffered_relpow_functional› and
‹m_steps_buffered_functional› below into the
SS4‹→›SS5 compute substep's functionality lemma — the
16th entry in the per-substep functionality cluster, completing
it under ‹det_mttm M›.›
lemma m_step_buffered_functional:
fixes M :: "('q, 'a) mttm"
assumes det: "det_mttm M"
and h1: "((q, blocks, pos), (q1, blocks1, pos1)) ∈ m_step_buffered M"
and h2: "((q, blocks, pos), (q2, blocks2, pos2)) ∈ m_step_buffered M"
shows "(q1, blocks1, pos1) = (q2, blocks2, pos2)"
proof -
from h1 obtain a1 a1' d1 where
t1: "(q, a1, q1, a1', d1) ∈ delta_tm M"
and r1: "∀k. a1 k = read_bp (blocks k) (pos k)"
and w1: "∀k. blocks1 k = write_bp (blocks k) (pos k) (a1' k)"
and p1: "∀k. bp_advance_le (le_tm M) (a1 k) (pos k) (d1 k)
= Some (pos1 k)"
unfolding m_step_buffered_def by blast
from h2 obtain a2 a2' d2 where
t2: "(q, a2, q2, a2', d2) ∈ delta_tm M"
and r2: "∀k. a2 k = read_bp (blocks k) (pos k)"
and w2: "∀k. blocks2 k = write_bp (blocks k) (pos k) (a2' k)"
and p2: "∀k. bp_advance_le (le_tm M) (a2 k) (pos k) (d2 k)
= Some (pos2 k)"
unfolding m_step_buffered_def by blast
have a_eq: "a1 = a2"
using r1 r2 by (intro ext) auto
have t2': "(q, a1, q2, a2', d2) ∈ delta_tm M"
using t2 a_eq by simp
from det t1 t2'
have qad: "(q1, a1', d1) = (q2, a2', d2)"
unfolding det_mttm_def by blast
hence q_eq: "q1 = q2" and a'_eq: "a1' = a2'" and d_eq: "d1 = d2"
by auto
have b_eq: "blocks1 = blocks2"
using w1 w2 a'_eq by (intro ext) auto
have p_eq: "pos1 = pos2"
proof (intro ext)
fix k
have "Some (pos1 k) = Some (pos2 k)"
using p1 p2 a_eq d_eq by metis
thus "pos1 k = pos2 k" by simp
qed
show ?thesis using q_eq b_eq p_eq by simp
qed
text ‹Relational-power lift of ‹m_step_buffered_functional›:
under ‹det_mttm M›, n-fold composition is functional too.
Standard induction-on-n proof using the single-step lemma.›
lemma m_step_buffered_relpow_functional:
fixes M :: "('q, 'a) mttm"
assumes det: "det_mttm M"
and h1: "(s, s1) ∈ (m_step_buffered M) ^^ n"
and h2: "(s, s2) ∈ (m_step_buffered M) ^^ n"
shows "s1 = s2"
using h1 h2
proof (induction n arbitrary: s s1 s2)
case 0
thus ?case by simp
next
case (Suc n)
from Suc.prems(1) obtain s1' where
step1: "(s, s1') ∈ m_step_buffered M"
and rest1: "(s1', s1) ∈ (m_step_buffered M) ^^ n"
by (meson relpow_Suc_D2)
from Suc.prems(2) obtain s2' where
step2: "(s, s2') ∈ m_step_buffered M"
and rest2: "(s2', s2) ∈ (m_step_buffered M) ^^ n"
by (meson relpow_Suc_D2)
obtain q b p where s_eq: "s = (q, b, p)" by (cases s)
obtain q1' b1' p1' where s1'_eq: "s1' = (q1', b1', p1')" by (cases s1')
obtain q2' b2' p2' where s2'_eq: "s2' = (q2', b2', p2')" by (cases s2')
from step1 s_eq s1'_eq
have st1: "((q, b, p), (q1', b1', p1')) ∈ m_step_buffered M"
by simp
from step2 s_eq s2'_eq
have st2: "((q, b, p), (q2', b2', p2')) ∈ m_step_buffered M"
by simp
from m_step_buffered_functional[OF det st1 st2]
have "(q1', b1', p1') = (q2', b2', p2')" .
hence s'_eq: "s1' = s2'" using s1'_eq s2'_eq by simp
show ?case using Suc.IH[OF rest1] rest2 s'_eq by simp
qed
text ‹From a halt state, no buffered M-step is possible. Follows
from ‹valid_mttm M›'s structural constraint that
‹delta_tm M› has no transitions originating in
‹{t_tm M, r_tm M}›. Used below to rule out the case
where the two witnesses of ‹m_steps_buffered›'s
functionality argument use different step counts.›
lemma m_step_buffered_no_halt:
fixes M :: "('q, 'a) mttm"
assumes vM: "valid_mttm M"
and halt: "q ∈ {t_tm M, r_tm M}"
shows "((q, blocks, pos), s') ∉ m_step_buffered M"
proof
assume "((q, blocks, pos), s') ∈ m_step_buffered M"
then obtain a q' a' d where
st: "(q, a, q', a', d) ∈ delta_tm M"
unfolding m_step_buffered_def by blast
from valid_mttm_delta_set[OF vM] st
have "q ∈ Q_tm M - {t_tm M, r_tm M}" by auto
with halt show False by auto
qed
text ‹Functionality of ‹m_steps_buffered› under
‹det_mttm M›: the bounded-and-halt-truncated buffered
M-run is functional in its source.
Argument: from membership we obtain step counts ‹n1, n2›
with ‹n_i ≤ c› and ‹n_i = c ∨ fst s_i ∈ {t, r}›.
First show ‹n1 = n2›: if ‹n1 < n2› the prefix run
determines the n1-step state to be ‹s1› (by
‹m_step_buffered_relpow_functional›), and the
remaining ‹n2 - n1 ≥ 1› steps require a transition
from ‹s1›. The disjunction on ‹s1› forces either
‹n1 = c› (contradicting ‹n1 < n2 ≤ c›) or
‹fst s1 ∈ {t, r}›, the latter ruled out by
‹m_step_buffered_no_halt›. Symmetric for ‹n2 < n1›.
With ‹n1 = n2›, the relpow functional lemma finishes.›
lemma m_steps_buffered_functional:
fixes M :: "('q, 'a) mttm"
and s s1 s2 :: "'q
× (nat ⇒ ('c :: enum ⇒ 'a)
× ('c ⇒ 'a) × ('c ⇒ 'a))
× (nat ⇒ 'c bp)"
assumes vM: "valid_mttm M"
and det: "det_mttm M"
and h1: "(s, s1) ∈ m_steps_buffered M"
and h2: "(s, s2) ∈ m_steps_buffered M"
shows "s1 = s2"
proof -
let ?c = "card (UNIV :: 'c set)"
let ?R = "m_step_buffered M"
from h1 obtain n1 where
n1_bnd: "n1 ≤ ?c"
and n1_run: "(s, s1) ∈ ?R ^^ n1"
and n1_halt: "n1 = ?c ∨ fst s1 ∈ {t_tm M, r_tm M}"
unfolding m_steps_buffered_def by blast
from h2 obtain n2 where
n2_bnd: "n2 ≤ ?c"
and n2_run: "(s, s2) ∈ ?R ^^ n2"
and n2_halt: "n2 = ?c ∨ fst s2 ∈ {t_tm M, r_tm M}"
unfolding m_steps_buffered_def by blast
have no_extend:
"⋀m n s_m s_n.
(s, s_m) ∈ ?R ^^ m
⟹ (s, s_n) ∈ ?R ^^ n
⟹ m < n
⟹ n ≤ ?c
⟹ m = ?c ∨ fst s_m ∈ {t_tm M, r_tm M}
⟹ False"
proof -
fix m n :: nat and s_m s_n
assume rm: "(s, s_m) ∈ ?R ^^ m"
and rn: "(s, s_n) ∈ ?R ^^ n"
and mn: "m < n"
and nc: "n ≤ ?c"
and hl: "m = ?c ∨ fst s_m ∈ {t_tm M, r_tm M}"
define k where "k = n - m - 1"
have k_eq: "n = m + Suc k"
unfolding k_def using mn by simp
from rn k_eq have rn': "(s, s_n) ∈ ?R ^^ (m + Suc k)" by simp
from rn'[unfolded relpow_add]
obtain s' where
rpre: "(s, s') ∈ ?R ^^ m"
and rpost: "(s', s_n) ∈ ?R ^^ Suc k"
by blast
from m_step_buffered_relpow_functional[OF det rm rpre]
have s_eq: "s_m = s'" .
from rpost obtain s'' where step: "(s', s'') ∈ ?R"
by (meson relpow_Suc_D2)
with s_eq have step_sm: "(s_m, s'') ∈ ?R" by simp
from hl show False
proof
assume "m = ?c"
with k_eq nc show False by linarith
next
assume halt: "fst s_m ∈ {t_tm M, r_tm M}"
obtain q b p where sm_eq: "s_m = (q, b, p)" by (cases s_m)
from halt sm_eq have q_halt: "q ∈ {t_tm M, r_tm M}" by simp
from step_sm sm_eq have "((q, b, p), s'') ∈ ?R" by simp
with m_step_buffered_no_halt[OF vM q_halt] show False by blast
qed
qed
have n_eq: "n1 = n2"
proof (rule ccontr)
assume "n1 ≠ n2"
then consider (lt) "n1 < n2" | (gt) "n2 < n1" by linarith
thus False
proof cases
case lt
from no_extend[OF n1_run n2_run lt n2_bnd n1_halt] show False .
next
case gt
from no_extend[OF n2_run n1_run gt n1_bnd n2_halt] show False .
qed
qed
from n1_run n2_run n_eq
show ?thesis
using m_step_buffered_relpow_functional[OF det] by metis
qed
text ‹Linearisation helpers for the 3-block buffer. These map
‹(block, offset)›-pairs to indices in ‹[0, 3c)› and read
the symbol at a linearised buffer index. Used to express the
buffered compute's correctness as a contiguous-tape-window
match.›
definition bp_linear :: "('c :: enum) bp ⇒ nat" where
"bp_linear p =
(case fst p of
AE_Left ⇒ 0
| AE_Home ⇒ card (UNIV :: 'c set)
| AE_Right ⇒ 2 * card (UNIV :: 'c set))
+ c_idx (snd p)"
definition buf_lin_at ::
"(('c :: enum ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ nat ⇒ 'a" where
"buf_lin_at blocks i =
(let c = card (UNIV :: 'c set);
enum_c = (enum_class.enum :: 'c list);
(l, h, r) = blocks in
if i < c then l (enum_c ! i)
else if i < 2 * c then h (enum_c ! (i - c))
else r (enum_c ! (i - 2 * c)))"
text ‹Window invariant on a 3-block buffer plus buffered head:
(1) the buffer's linearisation matches an M-tape window of
3c contiguous positions starting at ‹p_start›; (2) the
buffered head decodes to the actual M-head position via
‹bp_linear›; (3) the entire window lies in the non-LE
region of the M-tape (‹p_start ≥ 1›). The non-LE
precondition keeps the predicate steady-state; the LE-edge
case (window intersects M-position 0) is handled by a
separate lemma at the simulation level.›
definition ae_window_invariant ::
"(nat ⇒ 'a) ⇒ nat
⇒ ('c :: enum) bp
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ nat ⇒ bool" where
"ae_window_invariant tM nM bp blocks p_start ⟷
p_start ≥ 1
∧ nM = p_start + bp_linear bp
∧ (∀i. i < 3 * card (UNIV :: 'c set)
⟶ tM (p_start + i) = buf_lin_at blocks i)"
text ‹LE-edge analogue of ‹ae_window_invariant› for the
‹le1› sub-case: ‹M'›'s head is at block 1 (the first
content block), so the buffer's left slot is
‹LE_block le› (block 0's content under
‹ae_init_config›) and M's tape position lies in
‹{0, …, 2c}›. The home and right buffer slots linearise
to an M-tape window starting at position 1; the left buffer
slot is ‹LE_block› by construction, with no claim about
M-tape positions ‹0, …, c-1› beyond ‹tM 0 = le›. Under
‹δLE› on ‹delta_tm M›, M's buffered trajectory in this
setting visits only ‹(AE_Left, c_last)› within the left
block (when reading LE), never the other left slots, so
the buffer‹↔›tape mismatch there is harmless.
The buffered head ‹bp› decodes to the actual M-tape position
by a three-way case-split (‹AE_Left c_last ↦ 0›,
‹AE_Home ↦ 1 + c_idx ofs›,
‹AE_Right ↦ 1 + c + c_idx ofs›) so the predicate serves
as both SS4 entry condition (‹bp = (AE_Home, ofs)›) and
post-compute condition (‹bp› anywhere in the three-block
buffer except ‹AE_Left› at non-‹c_last› offsets, which the
‹δLE›-respecting buffered trajectory cannot reach).›
definition ae_window_invariant_le1 ::
"(nat ⇒ 'a) ⇒ nat
⇒ ('c :: enum) bp
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ 'a ⇒ bool" where
"ae_window_invariant_le1 tM nM bp blocks le ⟷
fst blocks = LE_block le
∧ tM 0 = le
∧ (case fst bp of
AE_Left ⇒ snd bp = c_last ∧ nM = 0
| AE_Home ⇒ nM = Suc (c_idx (snd bp))
| AE_Right ⇒ nM = Suc (card (UNIV :: 'c set) + c_idx (snd bp)))
∧ (∀i. i < 2 * card (UNIV :: 'c set)
⟶ tM (Suc i)
= buf_lin_at blocks (card (UNIV :: 'c set) + i))"
text ‹LE-edge analogue of ‹ae_window_invariant› for the
‹le0› sub-case: ‹M'›'s head is at block 0 (the LE
block itself). Buffer shape: the home slot is
‹LE_block le› (block 0's content), the right slot is
block 1's content (real input/blank), and the left slot
holds an arbitrary sentinel (SS2 ‹→› SS3 installs
‹bl_block (bl_tm M)›; the predicate doesn't constrain it
because M's buffered trajectory cannot reach the left
block under ‹δLE› — M starts at home reading LE,
can only move N or R, and any R-move from home reading LE
jumps via ‹bp_advance_le›'s special case to
‹(AE_Right, c_first)›, bypassing the rest of home and
never visiting left).
The buffered head ‹bp› decodes:
‹AE_Home ↦ 0› (M sits at LE regardless of
‹snd bp›, since home is all-LE) and
‹AE_Right ↦ 1 + c_idx ofs› (M is in block 1's
range). ‹AE_Left› is excluded.
Only the right slot's linearisation is asserted: the home
slot is fully LE (so linearisation matches ‹tM› only at
position 0, which ‹tM 0 = le› covers; the rest of home's
linearisation is fake but unread).›
definition ae_window_invariant_le0 ::
"(nat ⇒ 'a) ⇒ nat
⇒ ('c :: enum) bp
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ 'a ⇒ bool" where
"ae_window_invariant_le0 tM nM bp blocks le ⟷
fst (snd blocks) = LE_block le
∧ tM 0 = le
∧ (case fst bp of
AE_Home ⇒ nM = 0
| AE_Right ⇒ nM = Suc (c_idx (snd bp))
| AE_Left ⇒ False)
∧ (∀i. i < card (UNIV :: 'c set)
⟶ tM (Suc i)
= buf_lin_at blocks (2 * card (UNIV :: 'c set) + i))"
text ‹Per-tape unified window invariant for the SS4‹→›SS5
trace toolkit. Hybrid encapsulation of the three regime-specific
sibling predicates: one extra parameter ‹pos› (the per-tape
‹mt_pos c' k› at SS4 entry, a frozen value during the
buffered ‹M›-side run) selects which sibling fires. Each
regime is expressed as an implication, so the dispatch is by
partition of ‹pos :: nat› into ‹0› / ‹1› /
‹≥ 2› — exactly one implication is non-vacuous on any
fixed ‹pos›.
Design choice rationale: the conjunction-of-implications form
avoids forcing consumers to disjunction-eliminate before getting
at the relevant conjunct, while the indexing by ‹pos›
(rather than a uniform regime tag) lets the predicate be
instantiated directly from the consumer's per-tape
‹mt_pos c' k› without an extra dispatch parameter. The
fixed-regime-per-tape property — ‹pos› doesn't change
during the buffered run because ‹m_step_buffered› is
parameterised by ‹(q, blocks, pos⇩b⇩p)› with no
‹c'› in scope — makes per-tape regime selection commute
with the induction in ‹ae_coupled_run_aux_general›.›
definition ae_window_invariant_general ::
"(nat ⇒ 'a) ⇒ nat
⇒ ('c :: enum) bp
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ nat ⇒ 'a ⇒ bool" where
"ae_window_invariant_general tM nM bp blocks pos le ⟷
(pos = 0 ⟶ ae_window_invariant_le0 tM nM bp blocks le)
∧ (pos = 1 ⟶ ae_window_invariant_le1 tM nM bp blocks le)
∧ (pos ≥ 2
⟶ ae_window_invariant tM nM bp blocks
((pos - 2) * card (UNIV :: 'c set) + 1))"
text ‹SS4 ‹→› SS5: read right into buffer; apply the compute
(c-fold composition of ‹M›'s ‹δ›) to determine the
post-stage ‹M›-state, the per-tape destination indicator,
the modified buffer slots, and the new per-tape offset; per-tape
move L back to home. Buffer-phase substep 4 (compute folded in).
The substrate write ‹a' = a› is a no-op (SS4 reads the right
block but does not modify the on-tape contents; modifications
are materialised during the write-back phase SS5‹→›SS8).
The compute happens in the state component: ‹m_steps_buffered›
consumes the (fully buffered) blocks plus ‹(AE_Home, ofs)›
starting position and produces the post-compute
‹(q', buf', end_pos)›; the new offset and destination are
projected from ‹end_pos›.›
definition ae_delta_ss4_ss5 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss4_ss5 M =
{((q, ofs, buf, dest_old, SS4), a,
(q', ofs', buf', dest', SS5), a, d) |
q ofs buf dest_old a q' ofs' buf' dest' d
buf_full end_pos bufC.
q ∈ Q_tm M ∧ q ≠ t_tm M ∧ q ≠ r_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ buf_full = (λk. (fst (buf k),
if k < k_tm M then fst (snd (buf k)) else a k,
a k))
∧ ((q, buf_full, λk. (AE_Home, ofs k)),
(q', bufC, end_pos)) ∈ m_steps_buffered M
∧ ofs' = (λk. if k < k_tm M then snd (end_pos k) else init_offset k)
∧ buf' = (λk. if k < k_tm M then bufC k else init_buffer (le_tm M) k)
∧ dest' = (λk. if k < k_tm M then fst (end_pos k) else init_dest k)
∧ d = (λk. if k < k_tm M
then (if a k = LE_block (le_tm M)
then dir.N else dir.L)
else dir.N)}"
text ‹Per-tape (write, move) action helpers for the four
write-back substeps (SS5‹→›SS6, SS6‹→›SS7,
SS7‹→›SS8, SS8‹→›SS1). Each takes
‹(le, a, buf, dest)› and returns ‹(a', d)›: the per-tape
written block and direction.
Convention: ‹buf k = (l, h, r)› is the post-compute buffer.
LE-stage ‹⟷› ‹h = LE_block le›. In steady-state, ‹dest›
ranges over ‹{AE_Left, AE_Home, AE_Right}›; in LE-stage, the
compute restricts ‹dest› to ‹{AE_Home, AE_Right}› but the
helpers handle the ‹AE_Left› branch as a vacuous fall-through
(will never fire under the compute's invariants).›
text ‹**Head trajectory through the writeback chain.** The
direction rules in the action helpers below thread ‹M'›'s
head through a specific sequence of block positions
across SS5 ‹→› SS8. Starting from the SS4
‹→› SS5 transition (which moves L when reading
non-LE, so SS5 entry is at block ‹s›, the original
home), the chain walks:
▪ SS5: at block ‹s›; writes ‹h›; moves L
(‹dest ≠ AE_Left›) or R (‹dest = AE_Left›).
▪ SS6: at block ‹s-1› or ‹s+1›; writes
‹l›/‹r› depending on ‹dest›; moves back toward home.
▪ SS7: at block ‹s›; writes ‹a› (idempotent);
moves L (‹dest = AE_Left›) or R (otherwise).
▪ SS8: at block ‹s+1› (‹dest ∈ {AE_Home,
AE_Right}›) or ‹s-1› (‹dest = AE_Left›); writes
‹r›/‹l›; lands at block ‹s + dest_offset›
for the next stage.
**Why this matters for the LE-edge cases.** For
steady-state (‹s ≥ 2›), the walk stays in data
territory and the LE-guard never fires. For le1
(‹s = 1›), the walk reaches **block 0 — the LE
position** at SS6 entry (when ‹dest ≠ AE_Left›) or
at SS8 entry (when ‹dest = AE_Left›). At those moments
the LE-guard branch fires (head reads ‹LE_block›),
writing ‹LE_block› back idempotently. The
side-band invariant ‹ae_position_link› records that
these LE-guard firings happen at exactly the substeps where
the default branch would otherwise write the buffer's
‹l›-slot (which is ‹LE_block› in le1, having been
loaded from block 0) to a non-LE position — the
pre-emption that keeps the encoding consistent.›
text ‹**LE-guard prefix and ‹δLE› compatibility.**
Each action helper prepends an LE-guard
‹if a = LE_block le then (a, N) else …› for syntactic
‹δLE›-compatibility: the per-substep relations are over
all ‹(state, a, …)› tuples, not just reachable ones, and
the substrate's ‹δLE› well-formedness conjunct (a
‹valid_mttm› clause) is universal.
In reachable executions ‹a = h› at SS5‹→›SS8 (head at
the home position), so the guard agrees with the
‹h = LE_block le› branch; in unreachable tuples
(‹a = LE_block le› but ‹h ≠ LE_block le›), the guard forces
a ‹δLE›-safe ‹(a, N)› output rather than the
buffer-driven ‹(…, L)› that would violate ‹δLE›.
This guard serves a double purpose: substrate compatibility
(the immediate concern above) AND the LE-pre-emption used
by le1/le0. In those regimes the head genuinely reaches
block 0, the LE-guard's ‹a = LE_block›
antecedent is true, and the guard fires the LE-block-write
branch in preference to the default — protecting block
0 from being clobbered by a non-LE buffer slot.›
fun ae_ss5_action ::
"'a ⇒ ('c :: enum ⇒ 'a)
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ ae_dest ⇒ (('c ⇒ 'a) × dir)" where
"ae_ss5_action le a (l, h, r) ds =
(if a = LE_block le then (a, dir.N)
else if h = LE_block le then (a, dir.N)
else (h, if ds = AE_Left then dir.R else dir.L))"
fun ae_ss6_action ::
"'a ⇒ ('c :: enum ⇒ 'a)
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ ae_dest ⇒ (('c ⇒ 'a) × dir)" where
"ae_ss6_action le a (l, h, r) ds =
(if a = LE_block le then (a, dir.R)
else if h = LE_block le then (a, dir.R)
else if ds = AE_Left then (r, dir.L) else (l, dir.R))"
fun ae_ss7_action ::
"'a ⇒ ('c :: enum ⇒ 'a)
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ ae_dest ⇒ (('c ⇒ 'a) × dir)" where
"ae_ss7_action le a (l, h, r) ds =
(if a = LE_block le then (a, dir.N)
else if h = LE_block le
then (r, if ds = AE_Right then dir.N else dir.L)
else (a, if ds = AE_Left then dir.L else dir.R))"
fun ae_ss8_action ::
"'a ⇒ ('c :: enum ⇒ 'a)
⇒ (('c ⇒ 'a) × ('c ⇒ 'a) × ('c ⇒ 'a))
⇒ ae_dest ⇒ (('c ⇒ 'a) × dir)" where
"ae_ss8_action le a (l, h, r) ds =
(if a = LE_block le then (a, dir.N)
else if h = LE_block le
then (if ds = AE_Right then (r, dir.N) else (a, dir.N))
else (case ds of
AE_Left ⇒ (l, dir.N)
| AE_Home ⇒ (r, dir.L)
| AE_Right ⇒ (r, dir.N)))"
text ‹SS5 ‹→› SS6: write home block; per-tape move depends on
‹(stage_kind k, dest k)›. Write-back substep 5.›
definition ae_delta_ss5_ss6 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss5_ss6 M =
{((q, ofs, buf, dest, SS5), a,
(q, ofs, buf, dest, SS6), a', d) |
q ofs buf dest a a' d.
q ∈ Q_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ a' = (λk. if k < k_tm M
then fst (ae_ss5_action (le_tm M) (a k) (buf k) (dest k))
else bl_block (bl_tm M))
∧ d = (λk. if k < k_tm M
then snd (ae_ss5_action (le_tm M) (a k) (buf k) (dest k))
else dir.N)}"
text ‹SS6 ‹→› SS7: write left (steady-state, ‹dest ∈ {AE_Home,
AE_Right}›) or right (steady-state, ‹dest = AE_Left›) or
home (LE-stage); per-tape move per dest. Write-back substep 6.›
definition ae_delta_ss6_ss7 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss6_ss7 M =
{((q, ofs, buf, dest, SS6), a,
(q, ofs, buf, dest, SS7), a', d) |
q ofs buf dest a a' d.
q ∈ Q_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ a' = (λk. if k < k_tm M
then fst (ae_ss6_action (le_tm M) (a k) (buf k) (dest k))
else bl_block (bl_tm M))
∧ d = (λk. if k < k_tm M
then snd (ae_ss6_action (le_tm M) (a k) (buf k) (dest k))
else dir.N)}"
text ‹SS7 ‹→› SS8: idempotent home re-write (steady-state) or
right write (LE-stage); per-tape move per dest. Write-back
substep 7.›
definition ae_delta_ss7_ss8 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss7_ss8 M =
{((q, ofs, buf, dest, SS7), a,
(q, ofs, buf, dest, SS8), a', d) |
q ofs buf dest a a' d.
q ∈ Q_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ a' = (λk. if k < k_tm M
then fst (ae_ss7_action (le_tm M) (a k) (buf k) (dest k))
else bl_block (bl_tm M))
∧ d = (λk. if k < k_tm M
then snd (ae_ss7_action (le_tm M) (a k) (buf k) (dest k))
else dir.N)}"
text ‹SS8 ‹→› SS1: write final block at destination; head ends
at ‹dest› position; substep counter resets to SS1. End of
write-back phase.
Halt-aware destination: if ‹q› reached a halting state
(‹t_tm M› / ‹r_tm M›) during the compute substep, the
end-of-stage state is forced to ‹(q, init_stage le_M)›,
which equals ‹t_M'› / ‹r_M'› by construction. This makes
M' actually reach its canonical accept / reject state when M
halts mid-stage, rather than stalling at SS5. For non-halting
‹q›, the (offset, buffer) pair is preserved for the next
stage; ‹dest› resets to ‹AE_Home›.›
definition ae_delta_ss8_ss1 ::
"('q, 'a) mttm
⇒ (('q × ('a, 'c :: enum) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× ('q × ('a, 'c) ae_stage)
× (nat ⇒ ('c ⇒ 'a))
× (nat ⇒ dir)) set" where
"ae_delta_ss8_ss1 M =
{((q, ofs, buf, dest, SS8), a,
(q, stage'), a', d) |
q ofs buf dest a stage' a' d.
q ∈ Q_tm M
∧ (∀j≥k_tm M. a j = bl_block (bl_tm M))
∧ stage' = (if q ∈ {t_tm M, r_tm M}
then init_stage (le_tm M)
else (ofs, buf, init_dest, SS1))
∧ a' = (λk. if k < k_tm M
then fst (ae_ss8_action (le_tm M) (a k) (buf k) (dest k))
else bl_block (bl_tm M))
∧ d = (λk. if k < k_tm M
then snd (ae_ss8_action (le_tm M) (a k) (buf k) (dest k))
else dir.N)}"
end