Simulating an endmarker LBA on the bounded |w|-cell tape (the LBA ⊆ CS half)

This is the converse simulation to Equivalence/EndmarkerTape.lean: an endmarker LBA M' on the |w|+2-cell bracketed tape ⊢ w ⊣ is simulated by a marker-free machine flagMachine M' on the |w| input cells. The deliverable is language_flagMachine_eq: LanguageRecognized (flagMachine M') (some ∘ inl) (decide (M' accepts ⊢⊣)) = LanguageEnd M'. Equivalence/ContextSensitive.lean combines it with the Myhill grammar to assemble LBA ⊆ CS, hence the headline CS = LBA (CS_eq_LBA).

Construction (the "fold")

M' uses |w|+2 cells; M has only |w|. We keep M''s interior cells 1 … |w| on M's cells 0 … |w|-1 (cell i ↔ interior cell i+1), and fold the two read-only-position marker cells into the boundary cells: cell 0 additionally stores M'-cell 0's content (the ⊢ cell) and the last cell additionally stores M'-cell |w|+1's content (the ⊣ cell). A work cell is therefore a FoldCell = (cur, leftEnd?, rightEnd?): the interior content cur, plus an optional ⊢-cell content (present only at cell 0) and optional ⊣-cell content (present only at the last cell).

M's head is always on the cell holding the content M' reads; a finite FMode records whether M''s head is on the folded ⊢ (onLeft), the interior (mid), or the folded ⊣ (onRight). Because the markers are folded into the same boundary cell as the adjacent interior cell, mode switches at the boundary keep M's head stationary — so one M'-step is exactly one M-step (no bounce). Boundary clamping of M' is reproduced by the onLeft/onRight transitions staying put.

Init phase (setup/scan/verify/rewind)

M starts at cell 0, which it knows is the left end, and marks it (leftEnd := some ⊢). It then scans right and nondeterministically guesses the last cell, marking it (rightEnd := some ⊣); moving right off that cell clamps iff the guess was correct, so re-reading a rightEnd-marked cell verifies the guess (a wrong guess reads an unmarked cell and dies). It then rewinds left to the leftEnd-marked cell 0 and enters the simulation at M'.initial with the head on ⊢ (onLeft).

The bisimulation (init reaches the encoded M' start config; simulation mirrors M' steps; a backward invariant rules out wrong-guess branches reaching acceptance) is the remaining work.

@[reducible, inline]

abbrev LBA.FoldCell (T : Type u_4) (Γ : Type u_5) : Type (max u_5 u_4)

A folded work cell of the simulating flag machine: the interior content cur of the corresponding M'-interior cell, plus the ⊢-cell content (Some only at cell 0) and the ⊣-cell content (Some only at the last cell).

Equations

• LBA.FoldCell T Γ = (LBA.EndAlpha T Γ × Option (LBA.EndAlpha T Γ) × Option (LBA.EndAlpha T Γ))

@[reducible, inline]

abbrev LBA.FAlpha (T : Type u_4) (Γ : Type u_5) : Type (max u_5 u_4)

Tape alphabet of the simulating flag machine: canonical marker-free alphabet with work alphabet FoldCell T Γ.

Equations

• LBA.FAlpha T Γ = Option (T ⊕ LBA.FoldCell T Γ)

inductive LBA.FMode : Type

Where M''s head sits relative to the cell M is currently on: on the folded left marker ⊢, in the interior, or on the folded right marker ⊣.

• onLeft : FMode
• mid : FMode
• onRight : FMode

@[instance_reducible]

instance LBA.instDecidableEqFMode : DecidableEq FMode

Equations

• LBA.instDecidableEqFMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LBA.instFintypeFMode : Fintype FMode

Equations

• LBA.instFintypeFMode = { elems := {LBA.FMode.onLeft, LBA.FMode.mid, LBA.FMode.onRight}, complete := ⋯ }

inductive LBA.FState (Λ : Type u_4) : Type u_4

States of the simulating flag machine: the four init-phase states and the simulation states sim q mode carrying the simulated M'-state q and the head mode.

• setup {Λ : Type u_4} : FState Λ
• scan {Λ : Type u_4} : FState Λ
• verify {Λ : Type u_4} : FState Λ
• rewind {Λ : Type u_4} : FState Λ
• sim {Λ : Type u_4} (q : Λ) (mode : FMode) : FState Λ

def LBA.instDecidableEqFState.decEq {Λ✝ : Type u_4} [DecidableEq Λ✝] (x✝ x✝¹ : FState Λ✝) : Decidable (x✝ = x✝¹)

Equations

• LBA.instDecidableEqFState.decEq LBA.FState.setup LBA.FState.setup = isTrue ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.setup LBA.FState.scan = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.setup LBA.FState.verify = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.setup LBA.FState.rewind = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.setup (LBA.FState.sim q mode) = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.scan LBA.FState.setup = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.scan LBA.FState.scan = isTrue ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.scan LBA.FState.verify = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.scan LBA.FState.rewind = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.scan (LBA.FState.sim q mode) = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.verify LBA.FState.setup = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.verify LBA.FState.scan = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.verify LBA.FState.verify = isTrue ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.verify LBA.FState.rewind = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.verify (LBA.FState.sim q mode) = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.rewind LBA.FState.setup = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.rewind LBA.FState.scan = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.rewind LBA.FState.verify = isFalse ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.rewind LBA.FState.rewind = isTrue ⋯
• LBA.instDecidableEqFState.decEq LBA.FState.rewind (LBA.FState.sim q mode) = isFalse ⋯
• LBA.instDecidableEqFState.decEq (LBA.FState.sim q mode) LBA.FState.setup = isFalse ⋯
• LBA.instDecidableEqFState.decEq (LBA.FState.sim q mode) LBA.FState.scan = isFalse ⋯
• LBA.instDecidableEqFState.decEq (LBA.FState.sim q mode) LBA.FState.verify = isFalse ⋯
• LBA.instDecidableEqFState.decEq (LBA.FState.sim q mode) LBA.FState.rewind = isFalse ⋯
• LBA.instDecidableEqFState.decEq (LBA.FState.sim a a_1) (LBA.FState.sim b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance LBA.instDecidableEqFState {Λ✝ : Type u_4} [DecidableEq Λ✝] : DecidableEq (FState Λ✝)

Equations

• LBA.instDecidableEqFState = LBA.instDecidableEqFState.decEq

@[instance_reducible]

noncomputable instance LBA.instFintypeFState {Λ : Type u_3} [Fintype Λ] : Fintype (FState Λ)

Equations

• One or more equations did not get rendered due to their size.

def LBA.cellCur {T : Type u_1} {Γ : Type u_2} : FAlpha T Γ → EndAlpha T Γ

The interior content M' would see at this cell: an input cell reads as interior input, a work cell reads its stored cur, a blank reads as interior blank.

Equations

• LBA.cellCur (some (Sum.inl t)) = Sum.inl (some (Sum.inl t))
• LBA.cellCur (some (Sum.inr fc)) = fc.1
• LBA.cellCur none = Sum.inl none

def LBA.cellLeft {T : Type u_1} {Γ : Type u_2} : FAlpha T Γ → Option (EndAlpha T Γ)

The folded ⊢-cell content, present only at cell 0.

Equations

• LBA.cellLeft (some (Sum.inr fc)) = fc.2.1
• LBA.cellLeft x✝ = none

def LBA.cellRight {T : Type u_1} {Γ : Type u_2} : FAlpha T Γ → Option (EndAlpha T Γ)

The folded ⊣-cell content, present only at the last cell.

Equations

• LBA.cellRight (some (Sum.inr fc)) = fc.2.2
• LBA.cellRight x✝ = none

def LBA.flagTransition {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) : FState Λ → FAlpha T Γ → Set (FState Λ × FAlpha T Γ × DLBA.Dir)

Transition of the simulating flag machine. Init phase: setup marks cell 0 (and may mark it as the last cell too, for |w|=1); scan moves right, nondeterministically marking the guessed last cell; verify accepts the guess iff the right move clamped back onto the marked cell; rewind returns left to cell 0. Simulation phase: replay M' on the folded tape, switching FMode at the boundaries with the head stationary.

Equations

• One or more equations did not get rendered due to their size.
• LBA.flagTransition M' LBA.FState.setup r = {(LBA.FState.scan, some (Sum.inr (LBA.cellCur r, some LBA.leftMark, none)), DLBA.Dir.right)}
• LBA.flagTransition M' LBA.FState.verify r = if (LBA.cellRight r).isSome = true then {(LBA.FState.rewind, r, DLBA.Dir.left)} else ∅
• LBA.flagTransition M' LBA.FState.rewind r = if (LBA.cellLeft r).isSome = true then {(LBA.FState.sim M'.initial LBA.FMode.onLeft, r, DLBA.Dir.stay)} else {(LBA.FState.rewind, r, DLBA.Dir.left)}

def LBA.flagMachine {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) : Machine (FAlpha T Γ) (FState Λ)

The marker-free flag machine simulating the endmarker machine M' (work alphabet FoldCell T Γ). It accepts exactly when the simulated M'-state is accepting.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LBA.flagMachine_accept_sim {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) (q : Λ) (mode : FMode) : (flagMachine M').accept (FState.sim q mode) = M'.accept q

The fold encoding of an M'-configuration.

def LBA.foldContents {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 3) → EndAlpha T Γ) : Fin (m + 1) → FAlpha T Γ

The folded contents: cell i holds the interior cell i+1, with the ⊢/⊣ cells folded into cells 0/m.

Equations

• LBA.foldContents c i = some (Sum.inr (c ⟨↑i + 1, ⋯⟩, if ↑i = 0 then some (c ⟨0, ⋯⟩) else none, if ↑i = m then some (c ⟨m + 2, ⋯⟩) else none))

def LBA.foldHead {m : ℕ} (p : Fin (m + 3)) : Fin (m + 1)

The folded head position: ⊢→cell 0, interior cell p→cell p-1, ⊣→cell m.

Equations

• LBA.foldHead p = if h0 : ↑p = 0 then ⟨0, ⋯⟩ else if h2 : ↑p = m + 2 then ⟨m, ⋯⟩ else ⟨↑p - 1, ⋯⟩

def LBA.foldMode {m : ℕ} (p : Fin (m + 3)) : FMode

The head mode determined by where M''s head sits.

Equations

• LBA.foldMode p = if ↑p = 0 then LBA.FMode.onLeft else if ↑p = m + 2 then LBA.FMode.onRight else LBA.FMode.mid

def LBA.fold {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} {m : ℕ} (cfg : DLBA.Cfg (EndAlpha T Γ) Λ (m + 2)) : DLBA.Cfg (FAlpha T Γ) (FState Λ) m

Encode an M'-configuration (on m+2 dim, m+3 cells) as the corresponding flagMachine configuration (on m dim, m+1 cells) in the simulation phase.

Equations

• LBA.fold cfg = { state := LBA.FState.sim cfg.state (LBA.foldMode cfg.tape.head), tape := { contents := LBA.foldContents cfg.tape.contents, head := LBA.foldHead cfg.tape.head } }

@[simp]

theorem LBA.cellCur_foldContents {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 3) → EndAlpha T Γ) (i : Fin (m + 1)) : cellCur (foldContents c i) = c ⟨↑i + 1, ⋯⟩

@[simp]

theorem LBA.cellLeft_foldContents {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 3) → EndAlpha T Γ) (i : Fin (m + 1)) : cellLeft (foldContents c i) = if ↑i = 0 then some (c ⟨0, ⋯⟩) else none

@[simp]

theorem LBA.cellRight_foldContents {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 3) → EndAlpha T Γ) (i : Fin (m + 1)) : cellRight (foldContents c i) = if ↑i = m then some (c ⟨m + 2, ⋯⟩) else none

theorem LBA.cfg_ext' {Γ' : Type u_4} {Λ' : Type u_5} {N : ℕ} {X Y : DLBA.Cfg Γ' Λ' N} (hs : X.state = Y.state) (hc : X.tape.contents = Y.tape.contents) (hh : X.tape.head = Y.tape.head) : X = Y

theorem LBA.foldHead_val {m : ℕ} (p : Fin (m + 3)) : ↑(foldHead p) = if ↑p = 0 then 0 else if ↑p = m + 2 then m else ↑p - 1

Writing M''s symbol at its head cell p only changes the folded cell at foldHead p; every other folded cell is unaffected (its cur/leftEnd/rightEnd all read c away from p).

theorem LBA.foldContents_off {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 3) → EndAlpha T Γ) (p : Fin (m + 3)) (a' : EndAlpha T Γ) (j : Fin (m + 1)) (hj : j ≠ foldHead p) : foldContents (Function.update c p a') j = foldContents c j

theorem LBA.foldContents_update {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 3) → EndAlpha T Γ) (p : Fin (m + 3)) (a' : EndAlpha T Γ) : Function.update (foldContents c) (foldHead p) (foldContents (Function.update c p a') (foldHead p)) = foldContents (Function.update c p a')

Writing at the head cell only affects the folded cell at foldHead p.

@[simp]

theorem LBA.foldMode_zero {m : ℕ} {p : Fin (m + 3)} (h : ↑p = 0) : foldMode p = FMode.onLeft

@[simp]

theorem LBA.foldMode_last {m : ℕ} {p : Fin (m + 3)} (h : ↑p = m + 2) : foldMode p = FMode.onRight

theorem LBA.foldMode_mid {m : ℕ} {p : Fin (m + 3)} (h0 : ↑p ≠ 0) (h2 : ↑p ≠ m + 2) : foldMode p = FMode.mid

Head-projection lemmas (definitional).

@[simp]

theorem LBA.write_head {Γ' : Type u_4} {N : ℕ} (t : DLBA.BoundedTape Γ' N) (a : Γ') : (t.write a).head = t.head

@[simp]

theorem LBA.moveHead_stay_head {Γ' : Type u_4} {N : ℕ} (t : DLBA.BoundedTape Γ' N) : (t.moveHead DLBA.Dir.stay).head = t.head

theorem LBA.moveHead_left_head {Γ' : Type u_4} {N : ℕ} (t : DLBA.BoundedTape Γ' N) : (t.moveHead DLBA.Dir.left).head = if h : 0 < ↑t.head then ⟨↑t.head - 1, ⋯⟩ else t.head

theorem LBA.moveHead_right_head {Γ' : Type u_4} {N : ℕ} (t : DLBA.BoundedTape Γ' N) : (t.moveHead DLBA.Dir.right).head = if h : ↑t.head < N then ⟨↑t.head + 1, ⋯⟩ else t.head

theorem LBA.moveHead_left_head_val {Γ' : Type u_4} {N : ℕ} (t : DLBA.BoundedTape Γ' N) : ↑(t.moveHead DLBA.Dir.left).head = if 0 < ↑t.head then ↑t.head - 1 else ↑t.head

theorem LBA.moveHead_right_head_val {Γ' : Type u_4} {N : ℕ} (t : DLBA.BoundedTape Γ' N) : ↑(t.moveHead DLBA.Dir.right).head = if ↑t.head < N then ↑t.head + 1 else ↑t.head

Simulation-phase single-step correctness (one M'-step = one flagMachine-step).

theorem LBA.fold_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} {cfg cfg' : DLBA.Cfg (EndAlpha T Γ) Λ (m + 2)} (h : Step M' cfg cfg') : Step (flagMachine M') (fold cfg) (fold cfg')

One M'-step is matched by exactly one flagMachine-step on the folded configuration.

theorem LBA.fold_reaches {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} {cfg cfg' : DLBA.Cfg (EndAlpha T Γ) Λ (m + 2)} (h : Reaches M' cfg cfg') : Reaches (flagMachine M') (fold cfg) (fold cfg')

The simulation extends to whole M'-computations.

theorem LBA.sim_step_inv {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} {cfg : DLBA.Cfg (EndAlpha T Γ) Λ (m + 2)} {X : DLBA.Cfg (FAlpha T Γ) (FState Λ) m} (h : Step (flagMachine M') (fold cfg) X) : ∃ (cfg' : DLBA.Cfg (EndAlpha T Γ) Λ (m + 2)), Step M' cfg cfg' ∧ X = fold cfg'

Backward simulation. Every flagMachine step out of a folded configuration fold cfg decodes to a genuine M'-step: it lands on fold cfg' for some cfg' with Step M' cfg cfg'.

Init phase: the flag machine sets up the folded tape.

From the input tape c, M converts each cell to its folded form (foldedTape), marking cell 0 with ⊢ and the last cell with ⊣, then rewinds to cell 0 and enters the simulation.

def LBA.foldedTape {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) : Fin (m + 1) → FAlpha T Γ

The fully folded tape obtained from an input tape c: each cell carries its interior content cellCur (c i) plus the boundary marks at cells 0 and m.

Equations

• LBA.foldedTape c i = some (Sum.inr (LBA.cellCur (c i), if ↑i = 0 then some LBA.leftMark else none, if ↑i = m then some LBA.rightMark else none))

def LBA.partialTape {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (k : ℕ) : Fin (m + 1) → FAlpha T Γ

The tape with cells < k folded and cells ≥ k still raw input.

Equations

• LBA.partialTape c k i = if ↑i < k then LBA.foldedTape c i else c i

def LBA.scanLast {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) : Fin (m + 1) → FAlpha T Γ

The over-scanned tape: every cell folded, the ⊢ mark on cell 0, but no ⊣ mark (the right-end guess has not yet been committed). Reached when scan keeps moving at the clamped last cell.

Equations

• LBA.scanLast c i = some (Sum.inr (LBA.cellCur (c i), if ↑i = 0 then some LBA.leftMark else none, none))

theorem LBA.scan_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (hraw : ∀ (i : Fin (m + 1)), cellLeft (c i) = none) (k : ℕ) (hk1 : 1 ≤ k) (hk2 : k < m) : Step (flagMachine M') { state := FState.scan, tape := { contents := partialTape c k, head := ⟨k, ⋯⟩ } } { state := FState.scan, tape := { contents := partialTape c (k + 1), head := ⟨k + 1, ⋯⟩ } }

One scan step converts the cell at an interior position k and moves right.

theorem LBA.partialTape_full {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) : partialTape c (m + 1) = foldedTape c

theorem LBA.scan_reach {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (hraw : ∀ (i : Fin (m + 1)), cellLeft (c i) = none) (j : ℕ) (hj : 1 ≤ j) (hjm : j ≤ m) : Reaches (flagMachine M') { state := FState.scan, tape := { contents := partialTape c 1, head := ⟨1, ⋯⟩ } } { state := FState.scan, tape := { contents := partialTape c j, head := ⟨j, ⋯⟩ } }

The scan phase: from cell 1 to the last cell m, converting each interior cell.

theorem LBA.setup_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (hm : 1 ≤ m) : Step (flagMachine M') { state := FState.setup, tape := { contents := c, head := ⟨0, ⋯⟩ } } { state := FState.scan, tape := { contents := partialTape c 1, head := ⟨1, ⋯⟩ } }

setup: mark cell 0 with ⊢ and step right (case m ≥ 1, so cell 0 is not the last).

theorem LBA.lastscan_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (hraw : ∀ (i : Fin (m + 1)), cellLeft (c i) = none) (hm : 1 ≤ m) : Step (flagMachine M') { state := FState.scan, tape := { contents := partialTape c m, head := ⟨m, ⋯⟩ } } { state := FState.verify, tape := { contents := foldedTape c, head := ⟨m, ⋯⟩ } }

The last scan step (at cell m): mark it ⊣ and clamp, entering verify.

theorem LBA.verify_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (hm : 1 ≤ m) : Step (flagMachine M') { state := FState.verify, tape := { contents := foldedTape c, head := ⟨m, ⋯⟩ } } { state := FState.rewind, tape := { contents := foldedTape c, head := ⟨m - 1, ⋯⟩ } }

verify confirms the guess (the right move clamped back onto the ⊣-marked cell).

theorem LBA.rewind_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (k : ℕ) (hk1 : 1 ≤ k) (hkm : k ≤ m) : Step (flagMachine M') { state := FState.rewind, tape := { contents := foldedTape c, head := ⟨k, ⋯⟩ } } { state := FState.rewind, tape := { contents := foldedTape c, head := ⟨k - 1, ⋯⟩ } }

One rewind step at an interior cell k ≥ 1 (no left marker): move left.

theorem LBA.rewind_reach {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (j : ℕ) (hjm : j ≤ m) : Reaches (flagMachine M') { state := FState.rewind, tape := { contents := foldedTape c, head := ⟨j, ⋯⟩ } } { state := FState.rewind, tape := { contents := foldedTape c, head := ⟨0, ⋯⟩ } }

The rewind phase: from cell j back down to cell 0.

theorem LBA.rewind0_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) : Step (flagMachine M') { state := FState.rewind, tape := { contents := foldedTape c, head := ⟨0, ⋯⟩ } } { state := FState.sim M'.initial FMode.onLeft, tape := { contents := foldedTape c, head := ⟨0, ⋯⟩ } }

The final rewind step at cell 0: the ⊢ mark is found, entering the simulation.

theorem LBA.init_reach {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) (hraw : ∀ (i : Fin (m + 1)), cellLeft (c i) = none) : Reaches (flagMachine M') { state := FState.setup, tape := { contents := c, head := ⟨0, ⋯⟩ } } { state := FState.sim M'.initial FMode.onLeft, tape := { contents := foldedTape c, head := ⟨0, ⋯⟩ } }

The whole init phase: from the input tape c, reach the simulation start at M'.initial on the head (⊢), with the tape fully folded.

Backward invariant: every reachable flagMachine configuration is sound.

GoodF enumerates the configurations reachable from the start ⟨setup, c₀⟩: the init-phase configurations (all non-accepting — setup, the partial/over scans, the dead and successful verify, the rewind), and the simulation-phase configurations, which are exactly fold-images of M'-configurations reachable from M''s start on e₀.

def LBA.GoodF {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (e₀ : Fin (m + 3) → EndAlpha T Γ) (c₀ : Fin (m + 1) → FAlpha T Γ) (X : DLBA.Cfg (FAlpha T Γ) (FState Λ) m) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem LBA.goodF_init {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (e₀ : Fin (m + 3) → EndAlpha T Γ) (c₀ : Fin (m + 1) → FAlpha T Γ) : GoodF M' e₀ c₀ { state := FState.setup, tape := { contents := c₀, head := ⟨0, ⋯⟩ } }

The start configuration satisfies the invariant.

theorem LBA.goodF_accepts {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (e₀ : Fin (m + 3) → EndAlpha T Γ) (c₀ : Fin (m + 1) → FAlpha T Γ) {X : DLBA.Cfg (FAlpha T Γ) (FState Λ) m} (hg : GoodF M' e₀ c₀ X) (hacc : (flagMachine M').accept X.state = true) : Accepts M' { state := M'.initial, tape := { contents := e₀, head := ⟨0, ⋯⟩ } }

An accepting GoodF configuration yields an accepting M'-run from M''s start on e₀.

theorem LBA.goodF_step {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (e₀ : Fin (m + 3) → EndAlpha T Γ) (c₀ : Fin (m + 1) → FAlpha T Γ) (hbridge : foldedTape c₀ = foldContents e₀) (hrawL : ∀ (i : Fin (m + 1)), cellLeft (c₀ i) = none) (hrawR : ∀ (i : Fin (m + 1)), cellRight (c₀ i) = none) {X X' : DLBA.Cfg (FAlpha T Γ) (FState Λ) m} (hg : GoodF M' e₀ c₀ X) (hstep : Step (flagMachine M') X X') : GoodF M' e₀ c₀ X'

The invariant is preserved by a flagMachine step.

theorem LBA.goodF_reaches {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (e₀ : Fin (m + 3) → EndAlpha T Γ) (c₀ : Fin (m + 1) → FAlpha T Γ) (hbridge : foldedTape c₀ = foldContents e₀) (hrawL : ∀ (i : Fin (m + 1)), cellLeft (c₀ i) = none) (hrawR : ∀ (i : Fin (m + 1)), cellRight (c₀ i) = none) {X : DLBA.Cfg (FAlpha T Γ) (FState Λ) m} (h : Reaches (flagMachine M') { state := FState.setup, tape := { contents := c₀, head := ⟨0, ⋯⟩ } } X) : GoodF M' e₀ c₀ X

Every configuration reachable from the start satisfies the invariant.

Assembly: the flag machine recognizes the same language.

def LBA.expand {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) : Fin (m + 3) → EndAlpha T Γ

The endmarker tape ⊢ (interior of c) ⊣ that the flag input c decodes to.

Equations

• LBA.expand c k = if ↑k = 0 then LBA.leftMark else if h : ↑k - 1 < m + 1 then LBA.cellCur (c ⟨↑k - 1, h⟩) else LBA.rightMark

theorem LBA.foldedTape_eq_foldContents_expand {T : Type u_1} {Γ : Type u_2} {m : ℕ} (c : Fin (m + 1) → FAlpha T Γ) : foldedTape c = foldContents (expand c)

The folded input tape equals the fold of its endmarker expansion — so init_reach lands exactly on fold of the M'-start configuration on ⊢ w ⊣.

theorem LBA.flag_accepts_iff {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) {m : ℕ} (c₀ : Fin (m + 1) → FAlpha T Γ) (hrawL : ∀ (i : Fin (m + 1)), cellLeft (c₀ i) = none) (hrawR : ∀ (i : Fin (m + 1)), cellRight (c₀ i) = none) : Accepts (flagMachine M') { state := FState.setup, tape := { contents := c₀, head := ⟨0, ⋯⟩ } } ↔ Accepts M' { state := M'.initial, tape := { contents := expand c₀, head := ⟨0, ⋯⟩ } }

Bisimulation (abstract). On the raw input tape c₀, the flag machine accepts iff M' accepts on the endmarker expansion ⊢ c₀ ⊣.

theorem LBA.flag_accepts_input {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) (w : List T) (hv : List.map (fun (t : T) => some (Sum.inl t)) w ≠ []) : Accepts (flagMachine M') (initCfgList (flagMachine M') (List.map (fun (t : T) => some (Sum.inl t)) w) hv) ↔ Accepts M' (initCfgEnd M' w)

Bisimulation (canonical). On a non-empty input w, the flag machine on the canonically loaded w accepts iff M' accepts on ⊢ w ⊣.

theorem LBA.language_flagMachine_eq {T : Type u_1} {Γ : Type u_2} {Λ : Type u_3} (M' : Machine (EndAlpha T Γ) Λ) (b : Bool) (hb : b = true ↔ Accepts M' (initCfgEnd M' [])) : LanguageRecognized (flagMachine M') (fun (t : T) => some (Sum.inl t)) b = LanguageEnd M'

The flag machine flagMachine M' (with empty-word flag b) recognizes exactly LanguageEnd M', provided b decides membership of ε.