The binary input parser implements the finite-alphabet decoder

An induction on the unread suffix proves both successful copying and early rejection. All inputs finish this phase within their length plus one step.

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

Successful parsing loads the complete input; failed parsing halts with empty output.

Equations

• M.Parsed ci co w xs none d = (d.state = none ∧ d.output = [])
• M.Parsed ci co w xs (some ys) d = (d = M.endCfg ci co w (xs ++ ys))

theorem Complexity.MathlibTM0.AlphabetMachine.parsed_cons {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {w : List Bool} (xs : List Input) (a : Input) (result : Option (List Input)) (d : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w) : M.Parsed ci co w (xs ++ [a]) result d ↔ M.Parsed ci co w xs (Option.map (fun (x : List Input) => a :: x) result) d

theorem Complexity.MathlibTM0.AlphabetMachine.run_succ_first {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 : ℕ) : Turing.MultiTapeTM.runFrom d (t + 1) = Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.step d) t

theorem Complexity.MathlibTM0.AlphabetMachine.run_succ_last {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 : ℕ) : Turing.MultiTapeTM.runFrom d (t + 1) = Turing.MultiTapeTM.step (Turing.MultiTapeTM.runFrom d t)

theorem Complexity.MathlibTM0.AlphabetMachine.run_copy_decode {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w bits : List Bool) (xs : List Input) (count : Option (Fin (ci.size + 1))) (hw : w = copyPrefix ci xs count ++ bits) (h : (copyPrefix ci xs count).length ≤ w.length) : M.Parsed ci co w xs (ci.decodeFrom (Option.map Fin.val count) bits) (Turing.MultiTapeTM.runFrom (M.copyCfg ci co w xs count h) (bits.length + 1))

theorem Complexity.MathlibTM0.AlphabetMachine.copy_encoded {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (xs : List Input) : Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg (ci.encode xs)) ((ci.encode xs).length + 1) = M.endCfg ci co (ci.encode xs) xs

theorem Complexity.MathlibTM0.AlphabetMachine.copy_invalid {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) (hw : ci.decode w = none) : (Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (w.length + 1)).state = none ∧ (Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (w.length + 1)).output = []