Parsing finite-alphabet inputs onto source symbol tracks

The parser's finite control records an opening delimiter and a bounded unary index. Each completed codeword writes one marked source cell. Invalid codes halt with empty output before the source is started.

def Complexity.MathlibTM0.AlphabetMachine.prefixCells {Input Output : Type} (M : AlphabetMachine Input Output) : List Input → List M.Alphabet

Source cells written before the final empty-input check.

Equations

• M.prefixCells [] = []
• M.prefixCells (a :: xs) = M.inputSymbol true a :: List.map (M.inputSymbol false) xs

theorem Complexity.MathlibTM0.AlphabetMachine.prefixCells_length {Input Output : Type} (M : AlphabetMachine Input Output) (xs : List Input) : (M.prefixCells xs).length = xs.length

theorem Complexity.MathlibTM0.AlphabetMachine.prefixCells_append {Input Output : Type} (M : AlphabetMachine Input Output) (xs : List Input) (a : Input) : M.prefixCells (xs ++ [a]) = M.prefixCells xs ++ [M.inputSymbol xs.isEmpty a]

theorem Complexity.MathlibTM0.AlphabetMachine.inputCells_false {Input Output : Type} (M : AlphabetMachine Input Output) (xs : List Input) : M.inputCells false xs = List.map (M.inputSymbol false) xs

theorem Complexity.MathlibTM0.AlphabetMachine.inputCells_true {Input Output : Type} (M : AlphabetMachine Input Output) (xs : List Input) : M.inputCells true xs = if xs.isEmpty = true then [M.empty] else M.prefixCells xs

def Complexity.MathlibTM0.AlphabetMachine.copyPrefix {Input : Type} (ci : FiniteAlphabetCode Input) (xs : List Input) (count : Option (Fin (ci.size + 1))) : List Bool

Number of input bits already consumed by a partial parse.

Equations

• Complexity.MathlibTM0.AlphabetMachine.copyPrefix ci xs count = ci.encode xs ++ Complexity.FiniteAlphabetCode.pendingPrefix (Option.map Fin.val count)

noncomputable def Complexity.MathlibTM0.AlphabetMachine.copyCfg {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) (xs : List Input) (count : Option (Fin (ci.size + 1))) (h : (copyPrefix ci xs count).length ≤ w.length) : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w

State after writing xs and reading the indicated prefix of the next codeword.

Equations

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

noncomputable def Complexity.MathlibTM0.AlphabetMachine.endCfg {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) (xs : List Input) : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w

End-of-input configuration before rewinding the parsed input.

Equations

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

theorem Complexity.MathlibTM0.AlphabetMachine.copyCfg_read {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (xs : List Input) (count : Option (Fin (ci.size + 1))) (h : (copyPrefix ci xs count).length ≤ w.length) (rest : List Bool) (hw : w = copyPrefix ci xs count ++ rest) : (M.copyCfg ci co w xs count h).inputSymbol = rest.head?

theorem Complexity.MathlibTM0.AlphabetMachine.copyCfg_zero {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) : M.copyCfg ci co w [] none ⋯ = Turing.MultiTapeTM.initCfg w

theorem Complexity.MathlibTM0.AlphabetMachine.run_add {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w) (s t : ℕ) : Turing.MultiTapeTM.runFrom d (s + t) = Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.runFrom d s) t

theorem Complexity.MathlibTM0.AlphabetMachine.copy_open {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (xs : List Input) (rest : List Bool) (hw : w = copyPrefix ci xs none ++ false :: rest) (h : (copyPrefix ci xs none).length ≤ w.length) (h' : (copyPrefix ci xs (some 0)).length ≤ w.length) : Turing.MultiTapeTM.step (M.copyCfg ci co w xs none h) = M.copyCfg ci co w xs (some 0) h'

theorem Complexity.MathlibTM0.AlphabetMachine.copy_true {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (xs : List Input) (i : Fin (ci.size + 1)) (rest : List Bool) (hw : w = copyPrefix ci xs (some i) ++ true :: rest) (hi : ↑i + 1 < ci.size) (h : (copyPrefix ci xs (some i)).length ≤ w.length) (h' : (copyPrefix ci xs (some ⟨↑i + 1, ⋯⟩)).length ≤ w.length) : Turing.MultiTapeTM.step (M.copyCfg ci co w xs (some i) h) = M.copyCfg ci co w xs (some ⟨↑i + 1, ⋯⟩) h'

theorem Complexity.MathlibTM0.AlphabetMachine.copy_close_prefix {Input : Type} (ci : FiniteAlphabetCode Input) (xs : List Input) (i : Fin (ci.size + 1)) (hi : ↑i < ci.size) : copyPrefix ci (xs ++ [ci.index.symm ⟨↑i, hi⟩]) none = copyPrefix ci xs (some i) ++ [false]

theorem Complexity.MathlibTM0.AlphabetMachine.copy_close {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (xs : List Input) (i : Fin (ci.size + 1)) (rest : List Bool) (hw : w = copyPrefix ci xs (some i) ++ false :: rest) (hi : ↑i < ci.size) (h : (copyPrefix ci xs (some i)).length ≤ w.length) (h' : (copyPrefix ci (xs ++ [ci.index.symm ⟨↑i, hi⟩]) none).length ≤ w.length) : Turing.MultiTapeTM.step (M.copyCfg ci co w xs (some i) h) = M.copyCfg ci co w (xs ++ [ci.index.symm ⟨↑i, hi⟩]) none h'

theorem Complexity.MathlibTM0.AlphabetMachine.copy_end {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (xs : List Input) (hw : w = ci.encode xs) (h : (copyPrefix ci xs none).length ≤ w.length) : Turing.MultiTapeTM.step (M.copyCfg ci co w xs none h) = M.endCfg ci co w xs

theorem Complexity.MathlibTM0.AlphabetMachine.run_rejected {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w) (t : ℕ) (h : (Turing.MultiTapeTM.step d).state = none ∧ (Turing.MultiTapeTM.step d).output = []) : (Turing.MultiTapeTM.runFrom d (t + 1)).state = none ∧ (Turing.MultiTapeTM.runFrom d (t + 1)).output = []