TM0PostAdapter

Part of the dependency closure of the small undecidable group constructions.

inductive Undecidability.TM0PostAdapter.Phase (Q : Type u_1) : Type u_1

A write instruction of TM0 is simulated by writing while moving right, then returning left.

• normal {Q : Type u_1} (q : Q) : Phase Q
• returnLeft {Q : Type u_1} (q : Q) : Phase Q

instance Undecidability.TM0PostAdapter.instFinitePhase {Q : Type u_1} [Finite Q] : Finite (Phase Q)

def Undecidability.TM0PostAdapter.machine {Q : Type u_1} [Inhabited Q] (M : Turing.TM0.Machine Bool Q) : PostMachine.Machine (Phase Q)

Convert Mathlib's atomic move-or-write TM0 into the combined write-and-move binary machine used by Post's rewriting construction.

Equations

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

def Undecidability.TM0PostAdapter.init {Q : Type u_1} [Inhabited Q] (input : List Bool) : PostMachine.Config (Phase Q)

Finite-list initial configuration corresponding to TM0.init.

Equations

• Undecidability.TM0PostAdapter.init [] = { state := Undecidability.TM0PostAdapter.Phase.normal default, left := [], head := false, right := [] }
• Undecidability.TM0PostAdapter.init (a :: right) = { state := Undecidability.TM0PostAdapter.Phase.normal default, left := [], head := a, right := right }

def Undecidability.TM0PostAdapter.Represents {Q : Type u_1} (c : Turing.TM0.Cfg Bool Q) (d : PostMachine.Config (Phase Q)) : Prop

The finite-list tape represents Mathlib's quotient tape; trailing blank cells are therefore harmless.

Equations

• Undecidability.TM0PostAdapter.Represents c d = ∃ (q : Q), d.state = Undecidability.TM0PostAdapter.Phase.normal q ∧ c.q = q ∧ c.Tape = Turing.Tape.mk₂ d.left (d.head :: d.right)

theorem Undecidability.TM0PostAdapter.respects {Q : Type u_1} [Inhabited Q] (M : Turing.TM0.Machine Bool Q) : StateTransition.Respects (Turing.TM0.step M) (PostMachine.step (machine M)) Represents

One atomic TM0 step is simulated by one combined step for a move and by two combined steps for a write.

theorem Undecidability.TM0PostAdapter.eval_dom_iff {Q : Type u_1} [Inhabited Q] (M : Turing.TM0.Machine Bool Q) (input : List Bool) : (StateTransition.eval (PostMachine.step (machine M)) (init input)).Dom ↔ (Turing.TM0.eval M input).Dom

The combined machine has the same halting domain as the Mathlib machine.

theorem Undecidability.TM0PostAdapter.terminates_iff_tm0_eval_dom {Q : Type u_1} [Inhabited Q] (M : Turing.TM0.Machine Bool Q) (input : List Bool) : MachineThue.Terminates (PostMachine.step (machine M)) (init input) ↔ (Turing.TM0.eval M input).Dom

theorem Undecidability.TM0PostAdapter.thue_iff_tm0_eval_dom {Q : Type u_1} [Inhabited Q] (M : Turing.TM0.Machine Bool Q) (input : List Bool) : ThueEq (PostMachine.system (machine M)) (PostMachine.encode (init input)) PostMachine.target ↔ (Turing.TM0.eval M input).Dom

Direct fixed-target Thue characterization of Mathlib TM0 halting.

theorem Undecidability.TM0PostAdapter.thue_system_finite {Q : Type u_1} [Inhabited Q] [Finite Q] (M : Turing.TM0.Machine Bool Q) : Set.Finite (PostMachine.system (machine M))