DropUntilFirstSep is Block-Realizable

We prove dropUntilFirstSep sep is block-realizable via a simple TM0 machine that scans right, erasing cells until it finds sep, erases sep, and halts.

The machine has four states:

• erase (initial): If current cell is sep, write default → wSep. If current cell is default, halt. Otherwise, write default → wOther.
• wSep: move right → done.
• wOther: move right → erase.
• done: halt.

Key results

• dufsM: the drop-until-first-separator TM0 machine.
• dufs_reaches_halts: exact reaching behavior on separator-containing blocks.
• tm0_dropUntilFirstSep_blockSepAnySuffix: separator-delimited block realizability for dropUntilFirstSep.

Machine definition

inductive DUFSState : Type

State type for the dropUntilFirstSep TM0 machine.

• erase : DUFSState
• wSep : DUFSState
• wOther : DUFSState
• done : DUFSState

instance instDecidableEqDUFSState : DecidableEq DUFSState

Equations

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

instance instInhabitedDUFSState : Inhabited DUFSState

Equations

• instInhabitedDUFSState = { default := DUFSState.erase }

instance instFintypeDUFSState : Fintype DUFSState

Equations

• instFintypeDUFSState = { elems := {DUFSState.erase, DUFSState.wSep, DUFSState.wOther, DUFSState.done}, complete := instFintypeDUFSState._proof_1 }

noncomputable def dufsM {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) : Turing.TM0.Machine Γ DUFSState

The dropUntilFirstSep TM0 machine.

Equations

• dufsM sep DUFSState.erase a = if a = sep then some (DUFSState.wSep, Turing.TM0.Stmt.write default) else if a = default then none else some (DUFSState.wOther, Turing.TM0.Stmt.write default)
• dufsM sep DUFSState.wSep a = some (DUFSState.done, Turing.TM0.Stmt.move Turing.Dir.right)
• dufsM sep DUFSState.wOther a = some (DUFSState.erase, Turing.TM0.Stmt.move Turing.Dir.right)
• dufsM sep DUFSState.done a = none

Correctness

theorem dufs_reaches_halts {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (hsep : sep ≠ default) (block suffix : List Γ) (hblock : ∀ g ∈ block, g ≠ default) : ∃ (q : DUFSState), Turing.Reaches (Turing.TM0.step (dufsM sep)) (Turing.TM0.init (block ++ default :: suffix)) { q := q, Tape := Turing.Tape.mk₁ (dropUntilFirstSep sep block ++ default :: suffix) } ∧ Turing.TM0.step (dufsM sep) { q := q, Tape := Turing.Tape.mk₁ (dropUntilFirstSep sep block ++ default :: suffix) } = none

Main result

theorem tm0_dropUntilFirstSep_block {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (sep : Γ) (hsep : sep ≠ default) : TM0RealizesBlock Γ (dropUntilFirstSep sep)

dropUntilFirstSep sep is block-realizable for any sep ≠ default.

theorem tm0_dropUntilFirstSep_blockAnySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (sep : Γ) (hsep : sep ≠ default) : TM0RealizesBlockAnySuffix Γ (dropUntilFirstSep sep)

dropUntilFirstSep sep is strong blank-delimited block-realizable: the machine halts as soon as it reaches sep or the boundary blank, so it never needs any invariant on the suffix after that boundary.

theorem tm0_dropUntilFirstSep_blockSepAnySuffix {Γ : Type} [Inhabited Γ] [DecidableEq Γ] [Fintype Γ] (sep outerSep : Γ) (hsep : sep ≠ default) : TM0RealizesBlockSepAnySuffix Γ outerSep (dropUntilFirstSep sep)

Separator-bounded dropUntilFirstSep, with an unrestricted suffix after the outer separator.