Reusing source-step simulation with finite-alphabet endpoints

During source execution, the new machine embeds the existing simulator without changing its work tapes, input position, output, or transition count.

def Complexity.MathlibTM0.AlphabetMachine.liftCfg {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 (Control M.State) w) : Turing.Cfg (Fintype.card M.simulatorSource.binary.Alphabet) Bool (Phase ci.size co.size M.State) w

Embed existing source-execution or emission control.

Equations

• M.liftCfg ci co d = Turing.Cfg.mapState (Option.map Complexity.MathlibTM0.AlphabetMachine.Phase.source) d

theorem Complexity.MathlibTM0.AlphabetMachine.lift_step_of_run {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 (Control M.State) w) (q : M.State) (hq : d.state = some (Control.run q)) : Turing.MultiTapeTM.step (M.liftCfg ci co d) = M.liftCfg ci co (Turing.MultiTapeTM.step d)

theorem Complexity.MathlibTM0.AlphabetMachine.lift_source_run {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 (Control M.State) w} {c c' : M.simulatorSource.binary.Config} (h : Sim M.simulatorSource.binary c d) (t : ℕ) (hr : M.simulatorSource.binary.run t c = some c') : Turing.MultiTapeTM.runFrom (M.liftCfg ci co d) t = M.liftCfg ci co (Turing.MultiTapeTM.runFrom d t)