Rewinding a parsed finite-alphabet input

Rewinding crosses one source cell for each closing delimiter. The parity of the delimiter count identifies closing delimiters while reading backwards. Initialization takes twice the binary input length plus two transitions.

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

Rewind the input and its decoded symbol tracks together.

Equations

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

noncomputable def Complexity.MathlibTM0.AlphabetMachine.readyCfg {Input Output : Type} (M : AlphabetMachine Input Output) (w : List Bool) (xs : List Input) : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Control M.State) w

The existing simulator with the complete decoded source input already loaded.

Equations

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

theorem Complexity.MathlibTM0.AlphabetMachine.endCfg_eq_rewind {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (xs : List Input) : M.endCfg ci co (ci.encode xs) xs = M.rewindCfg ci co (ci.encode xs) xs (ci.encode xs).length ⋯

theorem Complexity.MathlibTM0.AlphabetMachine.rewindCfg_zero {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) (xs : List Input) : Turing.MultiTapeTM.step (M.rewindCfg ci co w xs 0 ⋯) = M.liftCfg ci co (M.readyCfg w xs)

theorem Complexity.MathlibTM0.AlphabetMachine.ready_sim {Input Output : Type} (M : AlphabetMachine Input Output) (w : List Bool) (xs : List Input) : Sim M.simulatorSource.binary (M.simulatorSource.sourceCfg (Turing.TM0.init (M.inputCells true xs))) (M.readyCfg w xs)

theorem Complexity.MathlibTM0.AlphabetMachine.rewindCfg_step {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) (xs : List Input) (t : ℕ) (ht : t + 1 ≤ w.length) : Turing.MultiTapeTM.step (M.rewindCfg ci co w xs (t + 1) ht) = M.rewindCfg ci co w xs t ⋯

theorem Complexity.MathlibTM0.AlphabetMachine.run_rewind {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) (w : List Bool) (xs : List Input) (t : ℕ) (ht : t ≤ w.length) : Turing.MultiTapeTM.runFrom (M.rewindCfg ci co w xs t ht) t = M.rewindCfg ci co w xs 0 ⋯

theorem Complexity.MathlibTM0.AlphabetMachine.init_ready {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)) (2 * (ci.encode xs).length + 2) = M.liftCfg ci co (M.readyCfg (ci.encode xs) xs)