Theory AlphabetReduction_ForwardSubsteps
theory AlphabetReduction_ForwardSubsteps
imports AlphabetReduction_Simulation
begin
subsection ‹Per-substep simulation steps›
text ‹The compute substep: one ‹M'›-step from an
‹AR_SimCompute› stage whose ‹buf› field matches an
‹M›-‹δ›-tuple's read vector fires that tuple,
landing at the ‹AR_SimWrite› stage with ‹M›'s
post-step state ‹q'›, write vector ‹m_a'›, and
direction vector ‹m_d› threaded into the stage. No tape
cell changes and no head moves (the substrate write is the read
symbol back, direction ‹N›); the per-tape ‹posk›
carries through. The two global ‹δLE› filters are
discharged reflexively (write equals read, move ‹N›); the
target-stage validity rests on ‹valid_mttm›'s
‹δ›-range typing (‹m_a' k ∈ Γ_tm M›).
Throughout, ‹b› abbreviates ‹block_width Γ› (the per-symbol cell width).›
lemma ar_compute_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimCompute, tk, i, buf, dvec, posk)"
and mdelta: "(q, buf, q', m_a', m_d) ∈ delta_tm M"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimCompute, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimCompute, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q', AR_SimWrite, 0, 0, m_a', m_d, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = mt_pos c'"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimCompute, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?s = "(q, AR_SimCompute, tk, i, buf, dvec, posk)"
let ?s' = "(q', AR_SimWrite, 0, 0, m_a', m_d, posk)"
have rel_in: "(?s, ?a, ?s', ?a, (λ_. dir.N)) ∈ ar_delta_compute M"
unfolding ar_delta_compute_def using mdelta by auto
have ma'_gamma: "∀k. m_a' k ∈ Γ_tm M"
using valid_mttm_delta(4)[OF vM mdelta] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using ma'_gamma block_width_pos[of "Γ_tm M"]
by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have dsupp: "∀j ≥ k_tm M. m_a' j = bl_tm M ∧ m_d j = dir.N"
using valid_mttm_delta_support[OF vM mdelta] by blast
have src_posk: "∀j ≥ k_tm M. posk j = AR_AtLE"
using src_bounded by (simp add: ar_stage_bounded_def)
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4
∧ (λ_. dir.N) j = dir.N"
using pad_a by simp
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using dsupp src_posk kpos_tm by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a, (λ_. dir.N))
∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_unchanged: "(λk. go_dir ((λ_. dir.N) k) (n k)) = n"
by (rule ext) auto
let ?c'' = "Config⇩M ?s' ts n"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir ((λ_. dir.N) k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, (λ_. dir.N))
∈ alphabet_reduce_delta M"
by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_unchanged by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹Displacement bound: an ‹AR_SimAdvance› walk on one tape
is at most ‹2b› cells (the ‹L›-from-‹AR_AtFurtherProper›
worst case). The ‹0 < b› hypothesis is needed: the
‹N›-from-‹AR_AtLE› displacement is the constant ‹1›,
which exceeds ‹2b = 0›. Used to discharge target-stage validity
(‹Suc i < 2 * b›) for the walk and boundary arms, whose
reached bit-counter is bounded by the displacement.›
lemma ar_disp_le_2k:
assumes "0 < k"
shows "ar_disp k d pk ≤ 2 * k"
using assms by (cases d; cases pk) auto
text ‹The advance walk substep: from an ‹AR_SimAdvance› stage with
the bit-counter strictly below the per-tape displacement, one
‹M'›-step moves the active tape ‹tk›'s head one cell
‹L› (‹N› elsewhere) and stays in ‹AR_SimAdvance› at
‹Suc i›; the tape contents and all other heads are unchanged.
The ‹a tk ≠ LE4› hypothesis is load-bearing: it both selects
this arm (‹δ›'s stepping arm forbids an ‹L›-walk off
‹LE4›) and discharges the backward-‹δLE› filter, which
would otherwise reject the ‹L›-move on a tape reading ‹LE4›.
Target-stage validity rests on the displacement bound
‹ar_disp_le_2k›.›
lemma ar_advance_walk_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimAdvance, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and step_lt: "Suc i < ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimAdvance, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := mt_pos c' tk - 1)"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimAdvance, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.L else dir.N"
let ?s = "(q, AR_SimAdvance, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimAdvance, tk, Suc i, buf, dvec, posk)"
have aTk: "?a tk ≠ LE4" using notLE c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_advance M"
unfolding ar_delta_advance_def
using qQ aTk step_lt by (intro UnI1) blast
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have suc_i_lt: "Suc i < 2 * block_width (Γ_tm M)"
using step_lt ar_disp_le_2k[OF kpos, of "dvec tk" "posk tk"] by linarith
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using suc_i_lt buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid aTk pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := n tk - 1)"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := n tk - 1))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The advance boundary substep, non-last tape: the final
‹M'›-step of tape ‹tk›'s walk, handing off to the next
tape ‹k_succ tk› (bit-counter reset to ‹0›, position-kind
updated by ‹ar_newpos›, other tapes' ‹posk› preserved).
A single hypothesis covers both firing sub-cases via the arm's own
disjunction: the ‹R›-sub-case (‹dvec tk = R›, zero
displacement, no head move) and the non-‹R› sub-case
(‹dvec tk ≠ R›, the read not ‹LE4›, counter at
‹Suc i = displacement›, one last ‹L›-move). The head
conclusion is therefore conditional on ‹dvec tk›.›
lemma ar_advance_boundary_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimAdvance, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notlast: "¬ is_last_k M tk"
and fire: "(dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R
∧ mt_tape c' tk (mt_pos c' tk) ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimAdvance, k_succ tk, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (if dvec tk = dir.R then mt_pos c'
else (mt_pos c')(tk := mt_pos c' tk - 1))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimAdvance, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk ∧ dvec tk ≠ dir.R then dir.L else dir.N"
let ?s = "(q, AR_SimAdvance, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimAdvance, k_succ tk, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))"
have fire': "(dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R ∧ ?a tk ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))"
using fire c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_advance M"
unfolding ar_delta_advance_def
by (rule UnI1, rule UnI2) (use qQ notlast fire' in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have ksucc_lt: "k_succ tk < k_tm M"
proof -
have ne: "Suc tk ≠ k_tm M" using notlast by (simp add: is_last_k_def)
have le: "Suc tk ≤ k_tm M" using tk_lt by simp
show ?thesis unfolding k_succ_def using le_neq_implies_less[OF le ne] .
qed
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have pk: "∀j≥k_tm M. (posk(tk := ar_newpos (dvec tk) (posk tk))) j = AR_AtLE"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(posk(tk := ar_newpos (dvec tk) (posk tk))) j = AR_AtLE"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded ksucc_lt pk by (simp add: ar_stage_bounded_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid fire' pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k))
= (if dvec tk = dir.R then n else n(tk := n tk - 1))"
by (rule ext) (auto split: if_splits)
let ?c'' = "Config⇩M ?s' ts (if dvec tk = dir.R then n else n(tk := n tk - 1))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The advance boundary substep, last tape: as
‹ar_advance_boundary_step› but ‹tk› is the last tape in
the enumeration, so the hand-off goes to ‹AR_SimNext› (with the
current-tape field reset to ‹k_unidx 0›) instead of advancing to
‹k_succ tk›. Same two firing sub-cases and the same conditional
head conclusion; the arm-selection move is the single ‹rule UnI2›
(the third, rightmost arm of ‹ar_delta_advance›).›
lemma ar_advance_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimAdvance, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and last: "is_last_k M tk"
and fire: "(dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R
∧ mt_tape c' tk (mt_pos c' tk) ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimAdvance, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimNext, k_unidx 0, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (if dvec tk = dir.R then mt_pos c'
else (mt_pos c')(tk := mt_pos c' tk - 1))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimAdvance, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk ∧ dvec tk ≠ dir.R then dir.L else dir.N"
let ?s = "(q, AR_SimAdvance, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimNext, k_unidx 0, 0, buf, dvec,
posk(tk := ar_newpos (dvec tk) (posk tk)))"
have fire': "(dvec tk = dir.R ∧ i = 0)
∨ (dvec tk ≠ dir.R ∧ ?a tk ≠ LE4
∧ Suc i = ar_disp (block_width (Γ_tm M)) (dvec tk) (posk tk))"
using fire c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_advance M"
unfolding ar_delta_advance_def
by (rule UnI2) (use qQ last fire' in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have pk: "∀j≥k_tm M. (posk(tk := ar_newpos (dvec tk) (posk tk))) j = AR_AtLE"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(posk(tk := ar_newpos (dvec tk) (posk tk))) j = AR_AtLE"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded kpos_tm pk
by (simp add: ar_stage_bounded_def k_unidx_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid fire' pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k))
= (if dvec tk = dir.R then n else n(tk := n tk - 1))"
by (rule ext) (auto split: if_splits)
let ?c'' = "Config⇩M ?s' ts (if dvec tk = dir.R then n else n(tk := n tk - 1))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The write LE-skip substep, non-last tape: when ‹buf tk›
is the left-end marker, the cell at ‹sim_pos 0 = 0› is already
‹LE4› and need not be rewritten, so the per-tape write phase is
skipped — a single all-‹N› substep handing off to the next tape
‹k_succ tk› with the bit-counter still ‹0›. Tape and
heads unchanged (the compute-step shape).›
lemma ar_write_le_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskLE: "posk tk = AR_AtLE"
and notlast: "¬ is_last_k M tk"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = mt_pos c'"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimWrite, tk, 0, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λ_. dir.N"
let ?s = "(q, AR_SimWrite, tk, 0, buf, dvec, posk)"
let ?s' = "(q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_write M"
unfolding ar_delta_write_def
using qQ poskLE notlast by (intro UnI1) blast
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have ksucc_lt: "k_succ tk < k_tm M"
proof -
have ne: "Suc tk ≠ k_tm M" using notlast by (simp add: is_last_k_def)
have le: "Suc tk ≤ k_tm M" using tk_lt by simp
show ?thesis unfolding k_succ_def using le_neq_implies_less[OF le ne] .
qed
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a by simp
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded ksucc_lt by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_unchanged: "(λk. go_dir (?d k) (n k)) = n" by (rule ext) auto
let ?c'' = "Config⇩M ?s' ts n"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_unchanged by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The write LE-skip substep, last tape: as ‹ar_write_le_step›
but ‹tk› is the last tape, so the hand-off goes to
‹AR_SimAdvance› (current-tape field reset to ‹k_unidx 0›).
Arm 2 of the six-arm ‹ar_delta_write› union.›
lemma ar_write_le_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskLE: "posk tk = AR_AtLE"
and last: "is_last_k M tk"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = mt_pos c'"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimWrite, tk, 0, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λ_. dir.N"
let ?s = "(q, AR_SimWrite, tk, 0, buf, dvec, posk)"
let ?s' = "(q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_write M"
unfolding ar_delta_write_def
by (rule UnI1, rule UnI1, rule UnI1, rule UnI1, rule UnI2)
(use qQ poskLE last in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a by simp
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded kpos_tm by (simp add: ar_stage_bounded_def k_unidx_def)
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd by auto
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_unchanged: "(λk. go_dir (?d k) (n k)) = n" by (rule ext) auto
let ?c'' = "Config⇩M ?s' ts n"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_unchanged by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The write back-walk substep (proper region,
‹Suc i ≤ b›): with ‹buf tk› a proper symbol, the head
first walks ‹L› back across the ‹b›-cell block before the
forward-write phase; one ‹L›-move on ‹tk› (‹N›
elsewhere), no writes, staying in ‹AR_SimWrite› at ‹Suc i›.
Structurally the ‹ar_advance_walk_step› shape; arm 3 of the
union. As there, ‹a tk ≠ LE4› selects the arm and discharges
the backward-‹δLE› filter.›
lemma ar_write_walk_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and step_le: "Suc i ≤ block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimWrite, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := mt_pos c' tk - 1)"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimWrite, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.L else dir.N"
let ?s = "(q, AR_SimWrite, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimWrite, tk, Suc i, buf, dvec, posk)"
have aTk: "?a tk ≠ LE4" using notLE c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_write M"
unfolding ar_delta_write_def
by (rule UnI1, rule UnI1, rule UnI1, rule UnI2)
(use qQ poskproper aTk step_le in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have suc_i_lt: "Suc i < 2 * block_width (Γ_tm M)"
using step_le kpos by linarith
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using suc_i_lt buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid aTk pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := n tk - 1)"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := n tk - 1))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The forward-write image is never the left-end marker: it is
‹BLANK4› (blank symbol) or a bit cell of ‹encode_symbol›
(‹BIT0›/‹BIT1› only, by ‹encode_symbol_cell_domain›),
in range ‹j < b›. This is what makes the forward-write arms
legal under both ‹δLE› filters.›
lemma write_bit_not_LE4:
assumes "j < block_width Γ"
shows "write_bit Γ bl x j ≠ LE4"
proof (cases "x = bl")
case True
thus ?thesis by (simp add: write_bit_def)
next
case False
have jl: "j < length (encode_symbol Γ bl x)"
using assms by (simp add: encode_symbol_def)
have "encode_symbol Γ bl x ! j ∈ {BIT0, BIT1}"
using nth_mem[OF jl] encode_symbol_cell_domain[of Γ bl x] by blast
thus ?thesis using False by (auto simp: write_bit_def)
qed
text ‹The ‹j›-th cell of a block's ‹cell_repr› is the
‹j›-th ‹write_bit› image (‹j < b›), uniformly
across the blank and proper branches. This is the bridge from the
tape-correspondence cell value (‹cell_repr … ! j›) to the
‹write_bit› image that the write phase produces, and to the
‹≠ LE4› fact the back-walk / bit-write guards need.›
lemma cell_repr_nth_write_bit:
assumes "j < block_width Γ"
shows "cell_repr Γ bl x ! j = write_bit Γ bl x j"
using assms by (cases "x = bl")
(simp_all add: cell_repr_def write_bit_def length_encode_symbol)
lemma cell_repr_nth_not_LE4:
assumes "j < block_width Γ"
shows "cell_repr Γ bl x ! j ≠ LE4"
using cell_repr_nth_write_bit[OF assms] write_bit_not_LE4[OF assms] by simp
text ‹Under the encoding, the only ‹LE4› cell of the simulated
tape is at position ‹0›: every position ‹≥ 1› lies in
some proper block ‹[sim_pos b p, sim_pos b p + b)› (the
‹div›/‹mod› decomposition of ‹pos - 1›) and so
carries a ‹cell_repr› cell, which is never ‹LE4›. The
fact the advance back-walk's ‹notLE› guard rests on: a head
walking through proper cells never reads the left-end marker.›
lemma ar_tape_correspondence_not_LE4:
assumes corr: "ar_tape_correspondence Γ le bl tM tM'"
and pos1: "1 ≤ pos"
shows "tM' pos ≠ LE4"
proof -
let ?K = "block_width Γ"
have K1: "1 ≤ ?K" using block_width_pos .
have jK: "(pos - 1) mod ?K < ?K" using K1 by simp
have p1: "1 ≤ (pos - 1) div ?K + 1" by simp
have pe: "pos = sim_pos ?K ((pos - 1) div ?K + 1) + (pos - 1) mod ?K"
proof -
have "sim_pos ?K ((pos - 1) div ?K + 1) + (pos - 1) mod ?K
= (pos - 1) div ?K * ?K + (pos - 1) mod ?K + 1"
by (simp add: sim_pos_def)
also have "… = (pos - 1) + 1" by (simp add: div_mult_mod_eq)
also have "… = pos" using pos1 by simp
finally show ?thesis by simp
qed
have corrprop: "tM' (sim_pos ?K p + j) = cell_repr Γ bl (tM p) ! j"
if "1 ≤ p" and "j < ?K" for p j
using corr that unfolding ar_tape_correspondence_def by blast
have "tM' pos
= cell_repr Γ bl (tM ((pos - 1) div ?K + 1)) ! ((pos - 1) mod ?K)"
using corrprop[OF p1 jK] pe by simp
thus ?thesis using cell_repr_nth_not_LE4[OF jK] by simp
qed
text ‹The forward-write stepping substep (proper region,
‹b ≤ i›, ‹Suc i < 2b›): the ‹(i-b)›-th cell of
‹cell_repr (buf tk)› is written at ‹tk›, the head moves
‹R› on ‹tk› (‹N› elsewhere), staying in
‹AR_SimWrite› at ‹Suc i›. First per-substep lemma that
mutates the tape: the conclusion's ‹mt_tape› is a nested
‹fun_upd› writing ‹write_bit Γ bl (buf tk) (i-b)› at
‹tk›'s head cell. The read precondition ‹a tk ≠ LE4›
(proper region is past ‹LE4›) discharges the backward-‹δLE›
filter; ‹write_bit_not_LE4› discharges the forward filter.›
lemma ar_write_bit_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and ilo: "block_width (Γ_tm M) ≤ i"
and ihi: "Suc i < 2 * block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimWrite, tk, Suc i, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk :=
(mt_tape c' tk)(mt_pos c' tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimWrite, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?wb = "write_bit (Γ_tm M) (bl_tm M) (buf tk) (i - block_width (Γ_tm M))"
let ?a = "λk. ts k (n k)"
let ?a' = "λkk. if kk = tk then ?wb else ?a kk"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimWrite, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimWrite, tk, Suc i, buf, dvec, posk)"
have aTk: "?a tk ≠ LE4" using notLE c'_eq by simp
have jlt: "i - block_width (Γ_tm M) < block_width (Γ_tm M)" using ilo ihi by linarith
have wb_not_LE: "?wb ≠ LE4" using write_bit_not_LE4[OF jlt] .
have rel_in: "(?s, ?a, ?s', ?a', ?d) ∈ ar_delta_write M"
unfolding ar_delta_write_def
by (rule UnI1, rule UnI1, rule UnI2)
(use qQ poskproper ilo ihi in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using ihi buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a' j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a' j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a', ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid aTk wb_not_LE pad_read src_bounded dst_bd
by (auto split: if_splits)
have tape_new: "(λk. (ts k)(n k := ?a' k))
= ts(tk := (ts tk)(n tk := ?wb))"
by (rule ext) (auto simp: fun_upd_triv)
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' (ts(tk := (ts tk)(n tk := ?wb))) (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a' k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a', ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq tape_new pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The forward-write boundary substep, non-last tape
(‹Suc i = 2b›): the last cell of ‹cell_repr (buf tk)› is
written (‹j = i - b = b - 1›), the head moves ‹R›, and the
phase hands off to the next tape ‹k_succ tk› with the bit-counter
reset to ‹0›. The ‹ar_write_bit_step› tape-change shape;
arm 5 of the union.›
lemma ar_write_bit_boundary_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and notlast: "¬ is_last_k M tk"
and ihi: "Suc i = 2 * block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk :=
(mt_tape c' tk)(mt_pos c' tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimWrite, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?wb = "write_bit (Γ_tm M) (bl_tm M) (buf tk) (i - block_width (Γ_tm M))"
let ?a = "λk. ts k (n k)"
let ?a' = "λkk. if kk = tk then ?wb else ?a kk"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimWrite, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimWrite, k_succ tk, 0, buf, dvec, posk)"
have aTk: "?a tk ≠ LE4" using notLE c'_eq by simp
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have jlt: "i - block_width (Γ_tm M) < block_width (Γ_tm M)" using ihi kpos by linarith
have wb_not_LE: "?wb ≠ LE4" using write_bit_not_LE4[OF jlt] .
have rel_in: "(?s, ?a, ?s', ?a', ?d) ∈ ar_delta_write M"
unfolding ar_delta_write_def
by (rule UnI1, rule UnI2) (use qQ poskproper notlast ihi in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have ksucc_lt: "k_succ tk < k_tm M"
proof -
have ne: "Suc tk ≠ k_tm M" using notlast by (simp add: is_last_k_def)
have le: "Suc tk ≤ k_tm M" using tk_lt by simp
show ?thesis unfolding k_succ_def using le_neq_implies_less[OF le ne] .
qed
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a' j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a' j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded ksucc_lt by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a', ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid aTk wb_not_LE pad_read src_bounded dst_bd
by (auto split: if_splits)
have tape_new: "(λk. (ts k)(n k := ?a' k))
= ts(tk := (ts tk)(n tk := ?wb))"
by (rule ext) (auto simp: fun_upd_triv)
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' (ts(tk := (ts tk)(n tk := ?wb))) (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a' k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a', ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq tape_new pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The forward-write boundary substep, last tape: as
‹ar_write_bit_boundary_step› but ‹tk› is the last tape, so
after the last-cell write the phase transitions to ‹AR_SimAdvance›
(current-tape field reset to ‹k_unidx 0›). Arm 6 (rightmost) of
the union.›
lemma ar_write_bit_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimWrite, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and poskproper: "posk tk ≠ AR_AtLE"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and last: "is_last_k M tk"
and ihi: "Suc i = 2 * block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimWrite, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)
∧ mt_tape c'' = (mt_tape c')(tk :=
(mt_tape c' tk)(mt_pos c' tk :=
write_bit (Γ_tm M) (bl_tm M) (buf tk)
(i - block_width (Γ_tm M))))
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimWrite, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?wb = "write_bit (Γ_tm M) (bl_tm M) (buf tk) (i - block_width (Γ_tm M))"
let ?a = "λk. ts k (n k)"
let ?a' = "λkk. if kk = tk then ?wb else ?a kk"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimWrite, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimAdvance, k_unidx 0, 0, buf, dvec, posk)"
have aTk: "?a tk ≠ LE4" using notLE c'_eq by simp
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have jlt: "i - block_width (Γ_tm M) < block_width (Γ_tm M)" using ihi kpos by linarith
have wb_not_LE: "?wb ≠ LE4" using write_bit_not_LE4[OF jlt] .
have rel_in: "(?s, ?a, ?s', ?a', ?d) ∈ ar_delta_write M"
unfolding ar_delta_write_def
by (rule UnI2) (use qQ poskproper last ihi in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a' j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a' j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded kpos_tm by (simp add: ar_stage_bounded_def k_unidx_def)
have ard_in: "(?s, ?a, ?s', ?a', ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid aTk wb_not_LE pad_read src_bounded dst_bd
by (auto split: if_splits)
have tape_new: "(λk. (ts k)(n k := ?a' k))
= ts(tk := (ts tk)(n tk := ?wb))"
by (rule ext) (auto simp: fun_upd_triv)
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' (ts(tk := (ts tk)(n tk := ?wb))) (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a' k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a', ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq tape_new pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The read LE substep, non-last tape: at position ‹0› the
head reads ‹LE4›, sets ‹buf tk := le_tm M› directly (the
single LE-cell needs no accumulator), moves ‹R› on ‹tk›
to position ‹1›, and hands off to the next tape's read. Tape
unchanged. Target-stage validity uses ‹valid_mttm_LE_in_Gamma›
for the ‹buf tk := le_tm M› entry.›
lemma ar_read_le_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notlast: "¬ is_last_k M tk"
and posk_le: "posk tk = AR_AtLE"
and aLE: "mt_tape c' tk (mt_pos c' tk) = LE4"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimRead, k_succ tk, 0,
buf(tk := le_tm M), dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, 0, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimRead, tk, 0, buf, dvec, posk)"
let ?s' = "(q, AR_SimRead, k_succ tk, 0, buf(tk := le_tm M), dvec, posk)"
have aTk: "?a tk = LE4" using aLE c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
using qQ notlast posk_le aTk by (intro UnI1) blast
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using buf_valid valid_mttm_LE_in_Gamma[OF vM] kpos
by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have ksucc_lt: "k_succ tk < k_tm M"
proof -
have ne: "Suc tk ≠ k_tm M" using notlast by (simp add: is_last_k_def)
have le: "Suc tk ≤ k_tm M" using tk_lt by simp
show ?thesis unfolding k_succ_def using le_neq_implies_less[OF le ne] .
qed
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have bt: "∀j≥k_tm M. (buf(tk := le_tm M)) j = bl_tm M"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(buf(tk := le_tm M)) j = bl_tm M"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded ksucc_lt bt by (simp add: ar_stage_bounded_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The read LE substep, last tape: as ‹ar_read_le_step› but
‹tk› is the last tape, so the hand-off goes to
‹AR_SimCompute› (current-tape field reset to ‹k_unidx 0›),
beginning the compute substep. Arm 2 of the seven-arm
‹ar_delta_read› union.›
lemma ar_read_le_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and last: "is_last_k M tk"
and posk_le: "posk tk = AR_AtLE"
and aLE: "mt_tape c' tk (mt_pos c' tk) = LE4"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimCompute, k_unidx 0, 0,
buf(tk := le_tm M), dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, 0, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimRead, tk, 0, buf, dvec, posk)"
let ?s' = "(q, AR_SimCompute, k_unidx 0, 0, buf(tk := le_tm M), dvec, posk)"
have aTk: "?a tk = LE4" using aLE c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
by (rule UnI1, rule UnI1, rule UnI1, rule UnI1, rule UnI1, rule UnI2)
(use qQ last posk_le aTk in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using buf_valid valid_mttm_LE_in_Gamma[OF vM] kpos
by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have bt: "∀j≥k_tm M. (buf(tk := le_tm M)) j = bl_tm M"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(buf(tk := le_tm M)) j = bl_tm M"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded kpos_tm bt
by (simp add: ar_stage_bounded_def k_unidx_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The decoder image always lies in ‹Γ ∪ {bl}›: for
‹n < card Γ› it is ‹inv_into Γ (gamma_enum Γ bl) n›,
which is in ‹Γ› since ‹gamma_enum› is onto
‹{..< card Γ}› (bijection); the out-of-range fallback is
‹bl›. Totality here means the read arms' ‹buf›-update
validity holds for any accumulator value without per-arm range
reasoning.›
lemma gamma_unenum_mem:
assumes "finite Γ"
shows "gamma_unenum Γ bl n ∈ Γ ∪ {bl}"
proof (cases "n < card Γ")
case True
have "n ∈ gamma_enum Γ bl ` Γ"
using True gamma_enum_bij[OF assms] by (auto simp: bij_betw_def)
hence "inv_into Γ (gamma_enum Γ bl) n ∈ Γ" by (rule inv_into_into)
thus ?thesis using True by (simp add: gamma_unenum_def)
next
case False
thus ?thesis by (simp add: gamma_unenum_def)
qed
text ‹The read proper-arm look-back step 1 (‹i = 0›): with the
position-kind already in the proper region, the head moves ‹L›
from ‹sim_pos(p)› to ‹sim_pos(p) - 1› (the cell to
inspect for refining the position-kind), no buf change, transitioning
to ‹i = 1›. Tape unchanged; ‹a tk ≠ LE4› selects the
arm and discharges the backward-‹δLE› filter. Arm 3 of the
seven-arm union.›
lemma ar_read_lookback1_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and notLE: "mt_tape c' tk (mt_pos c' tk) ≠ LE4"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimRead, tk, Suc 0, buf, dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := mt_pos c' tk - 1)"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, 0, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.L else dir.N"
let ?s = "(q, AR_SimRead, tk, 0, buf, dvec, posk)"
let ?s' = "(q, AR_SimRead, tk, Suc 0, buf, dvec, posk)"
have aTk: "?a tk ≠ LE4" using notLE c'_eq by simp
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
by (rule UnI1, rule UnI1, rule UnI1, rule UnI1, rule UnI2)
(use qQ posk_proper aTk in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid by (simp add: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
using src_bounded by (simp add: ar_stage_bounded_def)
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid aTk pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := n tk - 1)"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := n tk - 1))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The read proper-arm look-back step 2 (‹i = 1›): at
‹sim_pos(p) - 1› the head reads the cell, refines the
position-kind (‹AR_AtFirstProper› if that cell is ‹LE4›,
i.e. the head was at ‹sim_pos 1›, else ‹AR_AtFurtherProper›),
resets ‹buf tk› to the zero-bits partial decode, and moves
‹R› back to ‹sim_pos(p)›, transitioning to ‹i = 2›.
The ‹R›-move makes ‹δLE› trivial even when reading
‹LE4›. Needs ‹2 ≤ b› for target validity
(‹i = 2›). Arm 4 of the union.›
lemma ar_read_lookback2_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, Suc 0, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and kge2: "2 ≤ block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, Suc 0, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, Suc 0, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimRead, tk, Suc (Suc 0),
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M) 0), dvec,
posk(tk := if mt_tape c' tk (mt_pos c' tk) = LE4
then AR_AtFirstProper else AR_AtFurtherProper))
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, Suc 0, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimRead, tk, Suc 0, buf, dvec, posk)"
let ?s' = "(q, AR_SimRead, tk, Suc (Suc 0),
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M) 0), dvec,
posk(tk := if ?a tk = LE4
then AR_AtFirstProper else AR_AtFurtherProper))"
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
by (rule UnI1, rule UnI1, rule UnI1, rule UnI2)
(use qQ posk_proper in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have gu_mem: "gamma_unenum (Γ_tm M) (bl_tm M) 0 ∈ Γ_tm M ∪ {bl_tm M}"
using gamma_unenum_mem[OF valid_mttm_finite_Gamma[OF vM]] .
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kge2 buf_valid gu_mem by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have bt: "∀j≥k_tm M.
(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M) 0)) j = bl_tm M"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M) 0)) j = bl_tm M"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
have pt: "∀j≥k_tm M. (posk(tk := if ?a tk = LE4
then AR_AtFirstProper else AR_AtFurtherProper)) j = AR_AtLE"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(posk(tk := if ?a tk = LE4
then AR_AtFirstProper else AR_AtFurtherProper)) j = AR_AtLE"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded tk_lt bt pt
by (simp add: ar_stage_bounded_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The read proper-arm per-bit stepping substep
(‹2 ≤ i›, ‹Suc i ≤ Suc b›): at
‹sim_pos(p) + (i-2)› the head reads a bit cell and folds it
into the partial decode via the ‹gamma_enum›/‹gamma_unenum›
roundtrip ‹partial' = 2 ⋅ gamma_enum (buf tk) + bit_value (a tk)›,
moves ‹R›, and continues to ‹i + 1›. Tape unchanged. Needs
‹2 ≤ b› for target validity at the upper end
(‹Suc i = Suc b›). Arm 5 of the union.›
lemma ar_read_bit_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and ilo: "2 ≤ i"
and ihi: "Suc i ≤ Suc (block_width (Γ_tm M))"
and kge2: "2 ≤ block_width (Γ_tm M)"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimRead, tk, Suc i,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (mt_tape c' tk (mt_pos c' tk)))),
dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimRead, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimRead, tk, Suc i,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk) + bit_value (?a tk))),
dvec, posk)"
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
by (rule UnI1, rule UnI1, rule UnI2)
(use qQ posk_proper ilo ihi in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have gu_mem: "gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk) + bit_value (?a tk))
∈ Γ_tm M ∪ {bl_tm M}"
using gamma_unenum_mem[OF valid_mttm_finite_Gamma[OF vM]] .
have suc_i_lt: "Suc i < 2 * block_width (Γ_tm M)"
using ihi kge2 by linarith
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using suc_i_lt buf_valid gu_mem by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have bt: "∀j≥k_tm M.
(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (?a tk)))) j = bl_tm M"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (?a tk)))) j = bl_tm M"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded tk_lt bt by (simp add: ar_stage_bounded_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The read proper-arm per-bit boundary substep
(‹i = Suc b›), non-last tape: the last-bit accumulator step (as
‹ar_read_bit_step›) leaving ‹buf tk› the fully-decoded
‹M›-symbol, then ‹R›-move and hand-off to the next tape
‹k_succ tk› with the bit-counter reset. Arm 6 of the union.›
lemma ar_read_bit_boundary_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and notlast: "¬ is_last_k M tk"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and ieq: "i = Suc (block_width (Γ_tm M))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimRead, k_succ tk, 0,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (mt_tape c' tk (mt_pos c' tk)))),
dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimRead, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimRead, k_succ tk, 0,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk) + bit_value (?a tk))),
dvec, posk)"
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
by (rule UnI1, rule UnI2) (use qQ notlast posk_proper ieq in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have gu_mem: "gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk) + bit_value (?a tk))
∈ Γ_tm M ∪ {bl_tm M}"
using gamma_unenum_mem[OF valid_mttm_finite_Gamma[OF vM]] .
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid gu_mem by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have ksucc_lt: "k_succ tk < k_tm M"
proof -
have ne: "Suc tk ≠ k_tm M" using notlast by (simp add: is_last_k_def)
have le: "Suc tk ≤ k_tm M" using tk_lt by simp
show ?thesis unfolding k_succ_def using le_neq_implies_less[OF le ne] .
qed
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have bt: "∀j≥k_tm M.
(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (?a tk)))) j = bl_tm M"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (?a tk)))) j = bl_tm M"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded ksucc_lt bt by (simp add: ar_stage_bounded_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
text ‹The read proper-arm per-bit boundary substep, last tape: same
last-bit accumulator step, transitioning to ‹AR_SimCompute› with
the current-tape field reset to ‹k_unidx 0› (all tapes decoded,
begin the compute substep). Arm 7 (rightmost) of the union.›
lemma ar_read_bit_finish_step:
fixes M :: "('q, 'a) mttm"
and c' :: "(sym4, 'q × 'a ar_stage) mt_config"
assumes vM: "valid_mttm M"
and stg: "mt_state c' = (q, AR_SimRead, tk, i, buf, dvec, posk)"
and qQ: "q ∈ Q_tm M"
and last: "is_last_k M tk"
and posk_proper: "posk tk ∈ {AR_AtFirstProper, AR_AtFurtherProper}"
and ieq: "i = Suc (block_width (Γ_tm M))"
and vsrc: "ar_valid_stage (Γ_tm M) (bl_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
and pad_blank: "∀j ≥ k_tm M. mt_tape c' j (mt_pos c' j) = BLANK4"
and src_bounded: "ar_stage_bounded (bl_tm M) (k_tm M)
(AR_SimRead, tk, i, buf, dvec, posk)"
shows "∃c''. (c', c'') ∈ mttm_step (alphabet_reduce_delta M)
∧ mt_state c'' = (q, AR_SimCompute, k_unidx 0, 0,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (mt_tape c' tk (mt_pos c' tk)))),
dvec, posk)
∧ mt_tape c'' = mt_tape c'
∧ mt_pos c'' = (mt_pos c')(tk := Suc (mt_pos c' tk))"
proof -
obtain ts n where c'_eq:
"c' = Config⇩M (q, AR_SimRead, tk, i, buf, dvec, posk) ts n"
using stg by (cases c') auto
let ?a = "λk. ts k (n k)"
let ?d = "λkk. if kk = tk then dir.R else dir.N"
let ?s = "(q, AR_SimRead, tk, i, buf, dvec, posk)"
let ?s' = "(q, AR_SimCompute, k_unidx 0, 0,
buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk) + bit_value (?a tk))),
dvec, posk)"
have rel_in: "(?s, ?a, ?s', ?a, ?d) ∈ ar_delta_read M"
unfolding ar_delta_read_def
by (rule UnI2) (use qQ last posk_proper ieq in blast)
have buf_valid: "∀k. buf k ∈ Γ_tm M ∪ {bl_tm M}"
using vsrc by (simp add: ar_valid_stage_def)
have gu_mem: "gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk) + bit_value (?a tk))
∈ Γ_tm M ∪ {bl_tm M}"
using gamma_unenum_mem[OF valid_mttm_finite_Gamma[OF vM]] .
have kpos: "0 < block_width (Γ_tm M)" using block_width_pos[of "Γ_tm M"] by simp
have dst_valid: "ar_valid_stage (Γ_tm M) (bl_tm M) (snd ?s')"
using kpos buf_valid gu_mem by (auto simp: ar_valid_stage_def)
have pad_a: "∀j ≥ k_tm M. ?a j = BLANK4" using pad_blank c'_eq by simp
have tk_lt: "tk < k_tm M" using src_bounded by (simp add: ar_stage_bounded_def)
have kpos_tm: "0 < k_tm M" using vM by (cases M) auto
have pad_read: "∀j ≥ k_tm M. ?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have jne: "j ≠ tk" using tk_lt jge by linarith
show "?a j = BLANK4 ∧ ?a j = BLANK4 ∧ ?d j = dir.N"
using pad_a jge jne by simp
qed
have dst_bd: "ar_stage_bounded (bl_tm M) (k_tm M) (snd ?s')"
proof -
have bt: "∀j≥k_tm M.
(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (?a tk)))) j = bl_tm M"
proof (intro allI impI)
fix j assume jge: "k_tm M ≤ j"
have "j ≠ tk" using tk_lt jge by linarith
thus "(buf(tk := gamma_unenum (Γ_tm M) (bl_tm M)
(2 * gamma_enum (Γ_tm M) (bl_tm M) (buf tk)
+ bit_value (?a tk)))) j = bl_tm M"
using src_bounded jge by (simp add: ar_stage_bounded_def)
qed
show ?thesis using src_bounded kpos_tm bt
by (simp add: ar_stage_bounded_def k_unidx_def)
qed
have ard_in: "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M"
unfolding alphabet_reduce_delta_def
using rel_in vsrc dst_valid pad_read src_bounded dst_bd
by (auto split: if_splits)
have ts_unchanged: "(λk. (ts k)(n k := ?a k)) = ts" by (rule ext) auto
have pos_new: "(λk. go_dir (?d k) (n k)) = n(tk := Suc (n tk))"
by (rule ext) simp
let ?c'' = "Config⇩M ?s' ts (n(tk := Suc (n tk)))"
have "(Config⇩M ?s ts n,
Config⇩M ?s' (λk. (ts k)(n k := ?a k))
(λk. go_dir (?d k) (n k)))
∈ mttm_step (alphabet_reduce_delta M)"
proof (rule mttm_step.intros)
show "(?s, ?a, ?s', ?a, ?d) ∈ alphabet_reduce_delta M" by (rule ard_in)
qed
hence step: "(c', ?c'') ∈ mttm_step (alphabet_reduce_delta M)"
using c'_eq ts_unchanged pos_new by simp
show ?thesis
using step by (intro exI[where x = ?c'']) (simp add: c'_eq)
qed
end