Equivalence between SingleTapeTM and Mathlib's TM0 and TM1

This file bridges CSLib's single-tape Turing machine model (Cslib.Turing.SingleTapeTM) with Mathlib's Post–Turing and Wang B-machine models (_root_.Turing.TM0 and _root_.Turing.TM1) as well as StateTransition.eval and StateTransition.EvalsToInTime.

Main definitions

• Cslib.Turing.SingleTapeTM.toTM1: step-exact embedding of a SingleTapeTM Symbol into _root_.Turing.TM1.
• Cslib.Turing.SingleTapeTM.toTM0: compilation of a SingleTapeTM Symbol into _root_.Turing.TM0 via _root_.Turing.TM1to0.tr.
• Cslib.Turing.SingleTapeTM.ofTM0: compilation of a finitely supported _root_.Turing.TM0.Machine (Option Symbol) Λ into a SingleTapeTM Symbol.
• Cslib.Turing.SingleTapeTM.ofTM1: compilation of a finitely supported _root_.Turing.TM1 machine into a SingleTapeTM Symbol.

Main results

• Cslib.Turing.SingleTapeTM.outputs_iff_mem_eval: tm.Outputs l l' holds if and only if tm.haltCfg l' ∈ StateTransition.eval tm.step (tm.initCfg l).
• Cslib.Turing.SingleTapeTM.outputsWithinTime_iff_evalsToInTime: tm.OutputsWithinTime l l' m holds if and only if StateTransition.EvalsToInTime tm.step (tm.initCfg l) (some (tm.haltCfg l')) m is nonempty.
• Cslib.Turing.SingleTapeTM.map_ofTM1Cfg_step, eval_toTM1, eval_toTM0_eq_eval_toTM1: toTM1 is a step-for-step simulation of tm, and toTM0 preserves eval.
• Cslib.Turing.SingleTapeTM.outputsWithinTime_ofTM0_iff, outputs_ofTM0_iff, eval_ofTM0, eval_ofTM1: ofTM0 preserves step counts, up to one final halting step, and terminal tape evaluations; ofTM1 preserves terminal tape evaluations.

References

• M. Sipser, Introduction to the Theory of Computation

Connection with StateTransition

theorem Cslib.Turing.SingleTapeTM.flip_bind_iterate_eq_some_iff {σ : Type u_1} (f : σ → Option σ) (a b : σ) (n : ℕ) : (flip bind f)^[n] (some a) = some b ↔ Relation.RelatesInSteps (fun (x y : σ) => y ∈ f x) a b n

theorem Cslib.Turing.SingleTapeTM.evalsTo_some_iff_relatesInSteps {σ : Type u_1} (f : σ → Option σ) (a b : σ) : Nonempty (StateTransition.EvalsTo f a (some b)) ↔ ∃ (n : ℕ), Relation.RelatesInSteps (fun (x y : σ) => y ∈ f x) a b n

theorem Cslib.Turing.SingleTapeTM.evalsToInTime_some_iff_relatesWithinSteps {σ : Type u_1} (f : σ → Option σ) (a b : σ) (m : ℕ) : Nonempty (StateTransition.EvalsToInTime f a (some b) m) ↔ Relation.RelatesWithinSteps (fun (x y : σ) => y ∈ f x) a b m

@[simp]

theorem Cslib.Turing.SingleTapeTM.step_haltCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) : tm.step (tm.haltCfg l) = none

theorem Cslib.Turing.SingleTapeTM.step_some {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (q : tm.State) (t : BiTape Symbol) : tm.step { state := some q, BiTape := t } = some { state := (tm.tr q t.head).2, BiTape := (t.write (tm.tr q t.head).1.symbol).optionMove (tm.tr q t.head).1.movement }

theorem Cslib.Turing.SingleTapeTM.outputs_iff_mem_eval {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) : tm.Outputs l l' ↔ tm.haltCfg l' ∈ StateTransition.eval tm.step (tm.initCfg l)

tm.Outputs l l' holds if and only if StateTransition.eval tm.step (tm.initCfg l) evaluates to tm.haltCfg l'.

theorem Cslib.Turing.SingleTapeTM.outputsWithinTime_iff_evalsToInTime {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) : tm.OutputsWithinTime l l' m ↔ Nonempty (StateTransition.EvalsToInTime tm.step (tm.initCfg l) (some (tm.haltCfg l')) m)

tm.OutputsWithinTime l l' m holds if and only if StateTransition.EvalsToInTime reaches some (tm.haltCfg l') in at most m steps.

Embedding SingleTapeTM into Mathlib's TM1 and TM0

def Cslib.Turing.SingleTapeTM.moveStmt {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (q : tm.State) (next : Turing.TM1.Stmt (Option Symbol) tm.State (Option Symbol)) : Turing.TM1.Stmt (Option Symbol) tm.State (Option Symbol)

Branching helper for optional head movement in TM1 using the stored head symbol.

def Cslib.Turing.SingleTapeTM.nextStmt {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (q : tm.State) : Turing.TM1.Stmt (Option Symbol) tm.State (Option Symbol)

Next-state helper in TM1 using the stored head symbol.

def Cslib.Turing.SingleTapeTM.toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (q : tm.State) : Turing.TM1.Stmt (Option Symbol) tm.State (Option Symbol)

Step-exact embedding of a SingleTapeTM Symbol into Mathlib's _root_.Turing.TM1. Each step loads the current tape head into the local store Option Symbol, writes the new symbol, performs the optional move, and transitions to the next state (or halts), all in a single TM1 step.

def Cslib.Turing.SingleTapeTM.ofTM1Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) : tm.Cfg

Forgetful projection from TM1 configurations to SingleTapeTM configurations.

def Cslib.Turing.SingleTapeTM.toTM1Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : tm.Cfg) (v : Option Symbol := none) : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)

Lift a SingleTapeTM configuration to a TM1 configuration with local variable v.

@[simp]

theorem Cslib.Turing.SingleTapeTM.ofTM1Cfg_toTM1Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : tm.Cfg) (v : Option Symbol) : tm.ofTM1Cfg (tm.toTM1Cfg c v) = c

@[simp]

theorem Cslib.Turing.SingleTapeTM.toTM1Cfg_initCfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) : tm.toTM1Cfg (tm.initCfg l) = Turing.TM1.init (List.map some l)

@[simp]

theorem Cslib.Turing.SingleTapeTM.ofTM1Cfg_init {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) : tm.ofTM1Cfg (Turing.TM1.init (List.map some l)) = tm.initCfg l

theorem Cslib.Turing.SingleTapeTM.stepAux_nextStmt {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (q : tm.State) (v : Option Symbol) (T : Turing.Tape (Option Symbol)) : Turing.TM1.stepAux (tm.nextStmt q) v T = { l := (tm.tr q v).2, var := v, Tape := T }

theorem Cslib.Turing.SingleTapeTM.stepAux_moveStmt {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (q : tm.State) (v : Option Symbol) (T : Turing.Tape (Option Symbol)) : Turing.TM1.stepAux (tm.moveStmt q (tm.nextStmt q)) v T = { l := (tm.tr q v).2, var := v, Tape := (tm.tr q v).1.movement.elim T fun (d : Turing.Dir) => Turing.Tape.move d T }

theorem Cslib.Turing.SingleTapeTM.step_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) : Turing.TM1.step tm.toTM1 c = Option.map (fun (c' : tm.Cfg) => tm.toTM1Cfg c' c.Tape.head) (tm.step (tm.ofTM1Cfg c))

One step of tm.toTM1 on a lifted configuration tm.toTM1Cfg c v takes exactly one step of tm and updates the local store to c.BiTape.head.

@[simp]

theorem Cslib.Turing.SingleTapeTM.map_ofTM1Cfg_step {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) : Option.map tm.ofTM1Cfg (Turing.TM1.step tm.toTM1 c) = tm.step (tm.ofTM1Cfg c)

ofTM1Cfg commutes with a single step of TM1.step tm.toTM1 and tm.step.

theorem Cslib.Turing.SingleTapeTM.respects_toTM1_ofTM1Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : StateTransition.Respects (Turing.TM1.step tm.toTM1) tm.step fun (c₁ : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) (c₂ : tm.Cfg) => tm.ofTM1Cfg c₁ = c₂

theorem Cslib.Turing.SingleTapeTM.eval_ofTM1Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (c : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) : StateTransition.eval tm.step (tm.ofTM1Cfg c) = tm.ofTM1Cfg <$> StateTransition.eval (Turing.TM1.step tm.toTM1) c

theorem Cslib.Turing.SingleTapeTM.eval_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List Symbol) : tm.ofTM1Cfg <$> StateTransition.eval (Turing.TM1.step tm.toTM1) (Turing.TM1.init (List.map some l)) = StateTransition.eval tm.step (tm.initCfg l)

Running tm.toTM1 from TM1.init (l.map some) and projecting via ofTM1Cfg agrees with StateTransition.eval tm.step (tm.initCfg l).

theorem Cslib.Turing.SingleTapeTM.outputs_imp_mem_eval_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {l l' : List Symbol} (h : tm.Outputs l l') : Turing.ListBlank.mk (List.map some l') ∈ Turing.TM1.eval tm.toTM1 (List.map some l)

If tm outputs l' on input l, then tm.toTM1 evaluates (l.map some) to ListBlank.mk (l'.map some).

theorem Cslib.Turing.SingleTapeTM.relatesInSteps_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {c₁ c₂ : tm.Cfg} {n : ℕ} (h : Relation.RelatesInSteps tm.TransitionRelation c₁ c₂ n) (v : Option Symbol) : ∃ (v' : Option Symbol), Relation.RelatesInSteps (fun (a b : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) => b ∈ Turing.TM1.step tm.toTM1 a) (tm.toTM1Cfg c₁ v) (tm.toTM1Cfg c₂ v') n

theorem Cslib.Turing.SingleTapeTM.relatesInSteps_of_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {c₁ c₂ : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)} {n : ℕ} (h : Relation.RelatesInSteps (fun (a b : Turing.TM1.Cfg (Option Symbol) tm.State (Option Symbol)) => b ∈ Turing.TM1.step tm.toTM1 a) c₁ c₂ n) : Relation.RelatesInSteps tm.TransitionRelation (tm.ofTM1Cfg c₁) (tm.ofTM1Cfg c₂) n

theorem Cslib.Turing.SingleTapeTM.outputsWithinTime_iff_evalsToInTime_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) : tm.OutputsWithinTime l l' m ↔ ∃ (v : Option Symbol), Nonempty (StateTransition.EvalsToInTime (Turing.TM1.step tm.toTM1) (Turing.TM1.init (List.map some l)) (some (tm.toTM1Cfg (tm.haltCfg l') v)) m)

tm.OutputsWithinTime l l' m is equivalent to tm.toTM1 reaching the halted configuration tm.toTM1Cfg (tm.haltCfg l') v in at most m steps.

theorem Cslib.Turing.SingleTapeTM.toTM1_supports {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Turing.TM1.Supports tm.toTM1 Finset.univ

def Cslib.Turing.SingleTapeTM.toTM0 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Turing.TM0.Machine (Option Symbol) (Turing.TM1to0.Λ' tm.toTM1)

Compilation of tm : SingleTapeTM Symbol into a Mathlib _root_.Turing.TM0.Machine via _root_.Turing.TM1to0.tr.

noncomputable def Cslib.Turing.SingleTapeTM.toTM0Stmts {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Finset (Turing.TM1to0.Λ' tm.toTM1)

Finite state set supporting tm.toTM0.

theorem Cslib.Turing.SingleTapeTM.toTM0_supports {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) : Turing.TM0.Supports tm.toTM0 ↑tm.toTM0Stmts

@[simp]

theorem Cslib.Turing.SingleTapeTM.eval_toTM0_eq_eval_toTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) (l : List (Option Symbol)) : Turing.TM0.eval tm.toTM0 l = Turing.TM1.eval tm.toTM1 l

theorem Cslib.Turing.SingleTapeTM.outputs_imp_mem_eval_toTM0 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] (tm : SingleTapeTM Symbol) {l l' : List Symbol} (h : tm.Outputs l l') : Turing.ListBlank.mk (List.map some l') ∈ Turing.TM0.eval tm.toTM0 (List.map some l)

If tm outputs l' on input l, then tm.toTM0 evaluates (l.map some) to ListBlank.mk (l'.map some).

Compiling Mathlib's TM0 and TM1 to SingleTapeTM

def Cslib.Turing.SingleTapeTM.ofTM0 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) : SingleTapeTM Symbol

Compile a Mathlib _root_.Turing.TM0.Machine (Option Symbol) Λ supported on a finite state set S : Finset Λ into a SingleTapeTM Symbol. Each non-halting TM0 transition (move d or write a') executes in 1 SingleTapeTM step, and halting (M q a = none) transitions to none in 1 step while leaving the tape unchanged.

def Cslib.Turing.SingleTapeTM.ofTM0Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) (c : Turing.TM0.Cfg (Option Symbol) Λ) (hq : c.q ∈ S) : (ofTM0 M S hs).Cfg

Translate a TM0 configuration with state in S to an active (ofTM0 M S hs).Cfg.

@[simp]

theorem Cslib.Turing.SingleTapeTM.ofTM0Cfg_init {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) (l : List Symbol) : ofTM0Cfg M S hs (Turing.TM0.init (List.map some l)) ⋯ = (ofTM0 M S hs).initCfg l

theorem Cslib.Turing.SingleTapeTM.step_ofTM0Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) (c : Turing.TM0.Cfg (Option Symbol) Λ) (hq : c.q ∈ S) : (ofTM0 M S hs).step (ofTM0Cfg M S hs c hq) = some { state := ((ofTM0 M S hs).tr ⟨c.q, hq⟩ c.Tape.head).2, BiTape := ((BiTape.equivTape.symm c.Tape).write ((ofTM0 M S hs).tr ⟨c.q, hq⟩ c.Tape.head).1.symbol).optionMove ((ofTM0 M S hs).tr ⟨c.q, hq⟩ c.Tape.head).1.movement }

theorem Cslib.Turing.SingleTapeTM.step_ofTM0Cfg_of_some {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) {c c' : Turing.TM0.Cfg (Option Symbol) Λ} (hq : c.q ∈ S) (hstep : Turing.TM0.step M c = some c') : (ofTM0 M S hs).step (ofTM0Cfg M S hs c hq) = some (ofTM0Cfg M S hs c' ⋯)

theorem Cslib.Turing.SingleTapeTM.step_ofTM0Cfg_of_none {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) {c : Turing.TM0.Cfg (Option Symbol) Λ} (hq : c.q ∈ S) (hstep : Turing.TM0.step M c = none) : (ofTM0 M S hs).step (ofTM0Cfg M S hs c hq) = some { state := none, BiTape := BiTape.equivTape.symm c.Tape }

theorem Cslib.Turing.SingleTapeTM.relatesInSteps_ofTM0Cfg {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) {c₁ c₂ : Turing.TM0.Cfg (Option Symbol) Λ} (hq₁ : c₁.q ∈ S) (n : ℕ) : Relation.RelatesInSteps (fun (a b : Turing.TM0.Cfg (Option Symbol) Λ) => b ∈ Turing.TM0.step M a) c₁ c₂ n ↔ ∃ (hq₂ : c₂.q ∈ S), Relation.RelatesInSteps (ofTM0 M S hs).TransitionRelation (ofTM0Cfg M S hs c₁ hq₁) (ofTM0Cfg M S hs c₂ hq₂) n

theorem Cslib.Turing.SingleTapeTM.relatesInSteps_ofTM0Cfg_none {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) {c₁ : Turing.TM0.Cfg (Option Symbol) Λ} (hq₁ : c₁.q ∈ S) (t_f : BiTape Symbol) (m : ℕ) : Relation.RelatesInSteps (ofTM0 M S hs).TransitionRelation (ofTM0Cfg M S hs c₁ hq₁) { state := none, BiTape := t_f } m ↔ ∃ (n : ℕ) (q_f : Λ), m = n + 1 ∧ Relation.RelatesInSteps (fun (a b : Turing.TM0.Cfg (Option Symbol) Λ) => b ∈ Turing.TM0.step M a) c₁ { q := q_f, Tape := BiTape.equivTape t_f } n ∧ Turing.TM0.step M { q := q_f, Tape := BiTape.equivTape t_f } = none

theorem Cslib.Turing.SingleTapeTM.outputsWithinTime_ofTM0_iff {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) (l l' : List Symbol) (t : ℕ) : (ofTM0 M S hs).OutputsWithinTime l l' (t + 1) ↔ ∃ (q_f : Λ), Relation.RelatesWithinSteps (fun (a b : Turing.TM0.Cfg (Option Symbol) Λ) => b ∈ Turing.TM0.step M a) (Turing.TM0.init (List.map some l)) { q := q_f, Tape := BiTape.equivTape (BiTape.mk₁ l') } t ∧ Turing.TM0.step M { q := q_f, Tape := BiTape.equivTape (BiTape.mk₁ l') } = none

(ofTM0 M S hs).OutputsWithinTime l l' (t + 1) holds if and only if M reaches a halting configuration with tape BiTape.equivTape (BiTape.mk₁ l') in at most t steps.

theorem Cslib.Turing.SingleTapeTM.outputs_ofTM0_iff {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) (l l' : List Symbol) : (ofTM0 M S hs).Outputs l l' ↔ ∃ (q_f : Λ), { q := q_f, Tape := BiTape.equivTape (BiTape.mk₁ l') } ∈ StateTransition.eval (Turing.TM0.step M) (Turing.TM0.init (List.map some l))

(ofTM0 M S hs).Outputs l l' holds if and only if StateTransition.eval (TM0.step M) on TM0.init (l.map some) halts with tape BiTape.equivTape (BiTape.mk₁ l').

theorem Cslib.Turing.SingleTapeTM.eval_ofTM0 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) (l : List Symbol) : Part.map (fun (c : (ofTM0 M S hs).Cfg) => (BiTape.equivTape c.BiTape).right₀) (StateTransition.eval (ofTM0 M S hs).step ((ofTM0 M S hs).initCfg l)) = Turing.TM0.eval M (List.map some l)

Evaluating ofTM0 M S hs on l and reading right₀ of the final tape produces the exact same partial result as _root_.Turing.TM0.eval M (l.map some).

theorem Cslib.Turing.SingleTapeTM.outputs_ofTM0_imp_mem_eval {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option Symbol) Λ) (S : Finset Λ) [DecidablePred fun (x : Λ) => x ∈ S] (hs : Turing.TM0.Supports M ↑S) {l l' : List Symbol} (h : (ofTM0 M S hs).Outputs l l') : Turing.ListBlank.mk (List.map some l') ∈ Turing.TM0.eval M (List.map some l)

If ofTM0 M S hs outputs l' on input l, then _root_.Turing.TM0.eval M (l.map some) evaluates to ListBlank.mk (l'.map some).

noncomputable def Cslib.Turing.SingleTapeTM.ofTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ σ : Type} [Inhabited Λ] [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM1.Stmt (Option Symbol) Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) : SingleTapeTM Symbol

Compile a finitely supported Mathlib _root_.Turing.TM1 machine into a SingleTapeTM Symbol by composing _root_.Turing.TM1to0.tr with SingleTapeTM.ofTM0.

theorem Cslib.Turing.SingleTapeTM.eval_ofTM1 {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ σ : Type} [Inhabited Λ] [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM1.Stmt (Option Symbol) Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) (l : List Symbol) : Part.map (fun (c : (ofTM1 M S hs).Cfg) => (BiTape.equivTape c.BiTape).right₀) (StateTransition.eval (ofTM1 M S hs).step ((ofTM1 M S hs).initCfg l)) = Turing.TM1.eval M (List.map some l)

Evaluating ofTM1 M S hs on l and reading right₀ of the final tape produces the exact same partial result as _root_.Turing.TM1.eval M (l.map some).

theorem Cslib.Turing.SingleTapeTM.outputs_ofTM1_imp_mem_eval {Symbol : Type} [Inhabited Symbol] [Fintype Symbol] {Λ σ : Type} [Inhabited Λ] [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM1.Stmt (Option Symbol) Λ σ) (S : Finset Λ) (hs : Turing.TM1.Supports M S) {l l' : List Symbol} (h : (ofTM1 M S hs).Outputs l l') : Turing.ListBlank.mk (List.map some l') ∈ Turing.TM1.eval M (List.map some l)

If ofTM1 M S hs outputs l' on input l, then _root_.Turing.TM1.eval M (l.map some) evaluates to ListBlank.mk (l'.map some).