Soundness of the TM → Grammar Construction

This file proves that the grammar tmToGrammar constructed from a TM0 machine is sound: it only generates words on which the TM halts.

Proof strategy

We define a "terminal content" function terminalContent that extracts, from each symbol in a sentential form, the original input character it represents. This function is invariant under all simulation and cleanup grammar rules (but increases during generation).

We then define a forward invariant GI with five constructors:

• initial: the start symbol
• generating: generation phase
• simulating: simulation phase (tracks TM configuration correspondence)
• cleanup: post-halt cleanup (tracks terminalContent = w and TM halts on w)
• done: terminal-only form

The key insight is that cleanup uses terminalContent instead of tracking a derivation to a terminal form. This avoids the non-confluence issue in the cleanup phase.

Terminal content

def symbolOriginal {T Λ : Type} : symbol T (TMtoGrammarNT T Λ) → Option T

Extract the "original input character" from a grammar symbol. Terminals contribute their value. Nonterminals contribute their orig field (if some). Boundary markers, start, genMore, and none-orig nonterminals contribute nothing.

Equations

• symbolOriginal (symbol.terminal t) = some t
• symbolOriginal (symbol.nonterminal (TMtoGrammarNT.cell (some t) a)) = some t
• symbolOriginal (symbol.nonterminal (TMtoGrammarNT.headCell a (some t) a_1)) = some t
• symbolOriginal (symbol.nonterminal (TMtoGrammarNT.haltCell (some t))) = some t
• symbolOriginal x✝ = none

def terminalContent {T Λ : Type} (sf : List (symbol T (TMtoGrammarNT T Λ))) : List T

The "terminal content" of a sentential form: the list of original input characters. This is invariant under simulation and cleanup rules.

Equations

• terminalContent sf = List.filterMap symbolOriginal sf

theorem terminalContent_nil {T Λ : Type} : terminalContent [] = []

theorem terminalContent_cons {T Λ : Type} (s : symbol T (TMtoGrammarNT T Λ)) (sf : List (symbol T (TMtoGrammarNT T Λ))) : terminalContent (s :: sf) = (match symbolOriginal s with | some t => [t] | none => []) ++ terminalContent sf

theorem terminalContent_append {T Λ : Type} (sf₁ sf₂ : List (symbol T (TMtoGrammarNT T Λ))) : terminalContent (sf₁ ++ sf₂) = terminalContent sf₁ ++ terminalContent sf₂

theorem terminalContent_terminal_map {T Λ : Type} (w : List T) : terminalContent (List.map symbol.terminal w) = w

theorem terminalContent_rule_preserved {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] {M : Turing.TM0.Machine (Option T) Λ} (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hns : r.input_N ≠ TMtoGrammarNT.start) (hng : r.input_N ≠ TMtoGrammarNT.genMore) : terminalContent (r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R) = terminalContent r.output_string

theorem terminalContent_preserved {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] {M : Turing.TM0.Machine (Option T) Λ} (sf sf' : List (symbol T (TMtoGrammarNT T Λ))) (htrans : grammar_transforms (tmToGrammar T Λ M) sf sf') (hns : ∀ s ∈ sf, s ≠ symbol.nonterminal TMtoGrammarNT.start) (hng : ∀ s ∈ sf, s ≠ symbol.nonterminal TMtoGrammarNT.genMore) : terminalContent sf' = terminalContent sf

Terminal-only forms can't be transformed

theorem no_transform_terminal {T : Type} (g : grammar T) (w : List T) (sf' : List (symbol T g.nt)) : ¬grammar_transforms g (List.map symbol.terminal w) sf'

Terminal-only forms can't be transformed.

theorem derives_terminal_id {T : Type} (g : grammar T) (w : List T) (sf : List (symbol T g.nt)) (h : grammar_derives g (List.map symbol.terminal w) sf) : sf = List.map symbol.terminal w

Derivation from terminal form is trivial.

theorem no_cell_rule {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (orig cur : Option T) (hN : r.input_N = TMtoGrammarNT.cell orig cur) : False

No rule has cell as input_N.

The corrected forward invariant

def isNonterminal {T N : Type} : symbol T N → Prop

Whether a symbol is a nonterminal.

Equations

• isNonterminal (symbol.terminal a) = False
• isNonterminal (symbol.nonterminal a) = True

inductive GI {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) : List (symbol T (TMtoGrammarNT T Λ)) → Prop

The forward invariant for the tmToGrammar construction.

This invariant tracks five phases:

1. initial: The start symbol [S].
2. generating: Building the initial configuration [LB, genMore, cells..., RB].
3. simulating: Simulating TM steps. Tracks correspondence with actual TM configs.
4. cleanup: Post-halt phase. Tracks terminalContent = w where TM halts on w.
5. done: Terminal-only form w.map terminal where TM halts on w.

• initial {T Λ : Type} [Inhabited Λ] {M : Turing.TM0.Machine (Option T) Λ} : GI M [symbol.nonterminal TMtoGrammarNT.start]
• generating {T Λ : Type} [Inhabited Λ] {M : Turing.TM0.Machine (Option T) Λ} (ts : List T) : GI M ([symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal TMtoGrammarNT.genMore] ++ List.map (fun (t : T) => symbol.nonterminal (TMtoGrammarNT.cell (some t) (some t))) ts ++ [symbol.nonterminal TMtoGrammarNT.rightBound])
• simulating {T Λ : Type} [Inhabited Λ] {M : Turing.TM0.Machine (Option T) Λ} (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (hreach : Turing.Reaches (Turing.TM0.step M) (Turing.TM0.init (List.map some (extractInput (twoTrackOriginals tc)))) tmCfg) : GI M (encodeTwoTrack tc)
• cleanup {T Λ : Type} [Inhabited Λ] {M : Turing.TM0.Machine (Option T) Λ} (sf : List (symbol T (TMtoGrammarNT T Λ))) (w : List T) (hhalt : (Turing.TM0.eval M (List.map some w)).Dom) (hcontent : terminalContent sf = w) (hhas_nt : ∃ s ∈ sf, isNonterminal s) (hno_start : ∀ s ∈ sf, s ≠ symbol.nonterminal TMtoGrammarNT.start) (hno_genMore : ∀ s ∈ sf, s ≠ symbol.nonterminal TMtoGrammarNT.genMore) (hno_headCell : ∀ s ∈ sf, ∀ (q : Λ) (orig cur : Option T), s ≠ symbol.nonterminal (TMtoGrammarNT.headCell q orig cur)) : GI M sf
• done {T Λ : Type} [Inhabited Λ] {M : Turing.TM0.Machine (Option T) Λ} (w : List T) (hhalt : (Turing.TM0.eval M (List.map some w)).Dom) : GI M (List.map symbol.terminal w)

Terminal halts

theorem GI_terminal_halts {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (w : List T) (h : GI M (List.map symbol.terminal w)) : (Turing.TM0.eval M (List.map some w)).Dom

Preservation lemmas

theorem GI_preserved_initial {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (sf' : List (symbol T (TMtoGrammarNT T Λ))) (htrans : grammar_transforms (tmToGrammar T Λ M) [symbol.nonterminal TMtoGrammarNT.start] sf') : GI M sf'

theorem no_leftBound_rule_genMore_context {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.leftBound) : r.input_L = [] ∧ (r.input_R = [symbol.nonterminal TMtoGrammarNT.rightBound] ∨ ∃ (orig : Option T), r.input_R = [symbol.nonterminal (TMtoGrammarNT.haltCell orig)])

theorem no_rightBound_rule_cell_context {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.rightBound) : ∃ (orig : Option T), r.input_L = [symbol.nonterminal (TMtoGrammarNT.haltCell orig)]

theorem genMore_rules_classification {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.genMore) : (r.input_L = [] ∧ r.input_R = [] ∧ ∃ (t : T), r.output_string = [symbol.nonterminal TMtoGrammarNT.genMore, symbol.nonterminal (TMtoGrammarNT.cell (some t) (some t))]) ∨ (r.input_L = [] ∧ r.input_R = [] ∧ ∃ (t : T), r.output_string = [symbol.nonterminal (TMtoGrammarNT.headCell default (some t) (some t))]) ∨ r.input_L = [] ∧ r.input_R = [symbol.nonterminal TMtoGrammarNT.rightBound] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.headCell default none none), symbol.nonterminal TMtoGrammarNT.rightBound]

theorem gen_form_no_start_head_halt {T Λ : Type} (ts : List T) (s : symbol T (TMtoGrammarNT T Λ)) (hs : s ∈ [symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal TMtoGrammarNT.genMore] ++ List.map (fun (t : T) => symbol.nonterminal (TMtoGrammarNT.cell (some t) (some t))) ts ++ [symbol.nonterminal TMtoGrammarNT.rightBound]) : s = symbol.nonterminal TMtoGrammarNT.leftBound ∨ s = symbol.nonterminal TMtoGrammarNT.genMore ∨ (∃ (t : T), s = symbol.nonterminal (TMtoGrammarNT.cell (some t) (some t))) ∨ s = symbol.nonterminal TMtoGrammarNT.rightBound

theorem GI_preserved_generating {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (ts : List T) (sf' : List (symbol T (TMtoGrammarNT T Λ))) (htrans : grammar_transforms (tmToGrammar T Λ M) ([symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal TMtoGrammarNT.genMore] ++ List.map (fun (t : T) => symbol.nonterminal (TMtoGrammarNT.cell (some t) (some t))) ts ++ [symbol.nonterminal TMtoGrammarNT.rightBound]) sf') : GI M sf'

theorem encodeTwoTrack_mem_classification {T Λ : Type} (tc : TwoTrackConfig) (s : symbol T (TMtoGrammarNT T Λ)) (hs : s ∈ encodeTwoTrack tc) : s = symbol.nonterminal TMtoGrammarNT.leftBound ∨ (∃ (orig : Option T) (cur : Option T), s = symbol.nonterminal (TMtoGrammarNT.cell orig cur)) ∨ s = symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur) ∨ s = symbol.nonterminal TMtoGrammarNT.rightBound

theorem encodeTwoTrack_second_not_rightBound {T Λ : Type} (tc : TwoTrackConfig) : ¬∃ (v : List (symbol T (TMtoGrammarNT T Λ))), encodeTwoTrack tc = [symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal TMtoGrammarNT.rightBound] ++ v

theorem no_leftBound_on_encodeTwoTrack {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.leftBound) (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) : False

theorem no_rightBound_on_encodeTwoTrack {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.rightBound) (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) : False

theorem headCell_rule_classification {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (q : Λ) (orig cur : Option T) (hN : r.input_N = TMtoGrammarNT.headCell q orig cur) : (∃ (q' : Λ) (action : Turing.TM0.Stmt (Option T)), M q cur = some (q', action)) ∨ M q cur = none ∧ r.input_L = [] ∧ r.input_R = [] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.haltCell orig)]

theorem sim_rule_detailed_classification {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (q : Λ) (orig cur : Option T) (hN : r.input_N = TMtoGrammarNT.headCell q orig cur) (q' : Λ) (action : Turing.TM0.Stmt (Option T)) (hMqa : M q cur = some (q', action)) : (∃ (γ' : Option T), action = Turing.TM0.Stmt.write γ' ∧ r.input_L = [] ∧ r.input_R = [] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.headCell q' orig γ')]) ∨ (action = Turing.TM0.Stmt.move Turing.Dir.right ∧ ∃ (o' : Option T) (c' : Option T), r.input_L = [] ∧ r.input_R = [symbol.nonterminal (TMtoGrammarNT.cell o' c')] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.cell orig cur), symbol.nonterminal (TMtoGrammarNT.headCell q' o' c')]) ∨ action = Turing.TM0.Stmt.move Turing.Dir.right ∧ r.input_L = [] ∧ r.input_R = [symbol.nonterminal TMtoGrammarNT.rightBound] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.cell orig cur), symbol.nonterminal (TMtoGrammarNT.headCell q' none none), symbol.nonterminal TMtoGrammarNT.rightBound] ∨ (action = Turing.TM0.Stmt.move Turing.Dir.left ∧ ∃ (o'' : Option T) (c'' : Option T), r.input_L = [symbol.nonterminal (TMtoGrammarNT.cell o'' c'')] ∧ r.input_R = [] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.headCell q' o'' c''), symbol.nonterminal (TMtoGrammarNT.cell orig cur)]) ∨ action = Turing.TM0.Stmt.move Turing.Dir.left ∧ r.input_L = [symbol.nonterminal TMtoGrammarNT.leftBound] ∧ r.input_R = [] ∧ r.output_string = [symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal (TMtoGrammarNT.headCell q' none none), symbol.nonterminal (TMtoGrammarNT.cell orig cur)]

Detailed classification of simulation rules matching headCell q orig cur when M q cur = some (q', action).

theorem encodeTwoTrack_no_headCell_outside_head {T Λ : Type} (tc : TwoTrackConfig) (s : symbol T (TMtoGrammarNT T Λ)) (hs : s ∈ [symbol.nonterminal TMtoGrammarNT.leftBound] ++ List.map (fun (p : Option T × Option T) => symbol.nonterminal (TMtoGrammarNT.cell p.1 p.2)) tc.leftCells ++ List.map (fun (p : Option T × Option T) => symbol.nonterminal (TMtoGrammarNT.cell p.1 p.2)) tc.rightCells ++ [symbol.nonterminal TMtoGrammarNT.rightBound]) (q : Λ) (orig cur : Option T) : s ≠ symbol.nonterminal (TMtoGrammarNT.headCell q orig cur)

theorem encodeTwoTrack_unique_split {T Λ : Type} (tc : TwoTrackConfig) (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ v) : u = [symbol.nonterminal TMtoGrammarNT.leftBound] ++ List.map (fun (p : Option T × Option T) => symbol.nonterminal (TMtoGrammarNT.cell p.1 p.2)) tc.leftCells ∧ v = List.map (fun (p : Option T × Option T) => symbol.nonterminal (TMtoGrammarNT.cell p.1 p.2)) tc.rightCells ++ [symbol.nonterminal TMtoGrammarNT.rightBound]

theorem sim_rule_write_case {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc tc' : TwoTrackConfig) (q' : Λ) (γ' : Option T) (hMqa : M tc.headState tc.headCur = some (q', Turing.TM0.Stmt.write γ')) (h_step : stepTwoTrack M tc = some tc') (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [] ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ [] ++ v) : u ++ [symbol.nonterminal (TMtoGrammarNT.headCell q' tc.headOrig γ')] ++ v = encodeTwoTrack tc'

theorem sim_rule_move_right_case {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc tc' : TwoTrackConfig) (q' : Λ) (o' c' : Option T) (hMqa : M tc.headState tc.headCur = some (q', Turing.TM0.Stmt.move Turing.Dir.right)) (h_step : stepTwoTrack M tc = some tc') (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [] ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ [symbol.nonterminal (TMtoGrammarNT.cell o' c')] ++ v) : u ++ [symbol.nonterminal (TMtoGrammarNT.cell tc.headOrig tc.headCur), symbol.nonterminal (TMtoGrammarNT.headCell q' o' c')] ++ v = encodeTwoTrack tc'

theorem sim_rule_move_right_boundary_case {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc tc' : TwoTrackConfig) (q' : Λ) (hMqa : M tc.headState tc.headCur = some (q', Turing.TM0.Stmt.move Turing.Dir.right)) (h_step : stepTwoTrack M tc = some tc') (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [] ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ [symbol.nonterminal TMtoGrammarNT.rightBound] ++ v) : u ++ [symbol.nonterminal (TMtoGrammarNT.cell tc.headOrig tc.headCur), symbol.nonterminal (TMtoGrammarNT.headCell q' none none), symbol.nonterminal TMtoGrammarNT.rightBound] ++ v = encodeTwoTrack tc'

theorem sim_rule_move_left_case {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc tc' : TwoTrackConfig) (q' : Λ) (o'' c'' : Option T) (hMqa : M tc.headState tc.headCur = some (q', Turing.TM0.Stmt.move Turing.Dir.left)) (h_step : stepTwoTrack M tc = some tc') (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [symbol.nonterminal (TMtoGrammarNT.cell o'' c'')] ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ [] ++ v) : u ++ [symbol.nonterminal (TMtoGrammarNT.headCell q' o'' c''), symbol.nonterminal (TMtoGrammarNT.cell tc.headOrig tc.headCur)] ++ v = encodeTwoTrack tc'

theorem sim_rule_move_left_boundary_case {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc tc' : TwoTrackConfig) (q' : Λ) (hMqa : M tc.headState tc.headCur = some (q', Turing.TM0.Stmt.move Turing.Dir.left)) (h_step : stepTwoTrack M tc = some tc') (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [symbol.nonterminal TMtoGrammarNT.leftBound] ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ [] ++ v) : u ++ [symbol.nonterminal TMtoGrammarNT.leftBound, symbol.nonterminal (TMtoGrammarNT.headCell q' none none), symbol.nonterminal (TMtoGrammarNT.cell tc.headOrig tc.headCur)] ++ v = encodeTwoTrack tc'

theorem sim_rule_gives_encodeTwoTrack {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur) (hM : ∃ (q' : Λ) (action : Turing.TM0.Stmt (Option T)), M tc.headState tc.headCur = some (q', action)) (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) : ∃ (tc' : TwoTrackConfig), stepTwoTrack M tc = some tc' ∧ u ++ r.output_string ++ v = encodeTwoTrack tc'

When a simulation rule fires on encodeTwoTrack tc, the result is encodeTwoTrack tc' for some tc' with stepTwoTrack M tc = some tc'.

theorem halt_rule_gives_cleanup {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (r : grule T (TMtoGrammarNT T Λ)) (hr : r ∈ (tmToGrammar T Λ M).rules) (hN : r.input_N = TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur) (hM : M tc.headState tc.headCur = none) (u v : List (symbol T (TMtoGrammarNT T Λ))) (_heq : encodeTwoTrack tc = u ++ r.input_L ++ [symbol.nonterminal r.input_N] ++ r.input_R ++ v) : r.input_L = [] ∧ r.input_R = [] ∧ r.output_string = [symbol.nonterminal (TMtoGrammarNT.haltCell tc.headOrig)]

theorem tm_eval_dom_of_reaches_halt {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (l : List (Option T)) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hreach : Turing.Reaches (Turing.TM0.step M) (Turing.TM0.init l) tmCfg) (hhalt : Turing.TM0.step M tmCfg = none) : (Turing.TM0.eval M l).Dom

theorem terminalContent_encodeTwoTrack {T Λ : Type} (tc : TwoTrackConfig) : terminalContent (encodeTwoTrack tc) = extractInput (twoTrackOriginals tc)

theorem encodeTwoTrack_no_start {T Λ : Type} (tc : TwoTrackConfig) (s : symbol T (TMtoGrammarNT T Λ)) (hs : s ∈ encodeTwoTrack tc) : s ≠ symbol.nonterminal TMtoGrammarNT.start

theorem encodeTwoTrack_no_genMore {T Λ : Type} (tc : TwoTrackConfig) (s : symbol T (TMtoGrammarNT T Λ)) (hs : s ∈ encodeTwoTrack tc) : s ≠ symbol.nonterminal TMtoGrammarNT.genMore

theorem tm_step_of_corresponds {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (h_Mqc : M tc.headState tc.headCur = none) : Turing.TM0.step M tmCfg = none

theorem encodeTwoTrack_no_headCell_in_parts {T Λ : Type} (tc : TwoTrackConfig) (u v : List (symbol T (TMtoGrammarNT T Λ))) (heq : encodeTwoTrack tc = u ++ [symbol.nonterminal (TMtoGrammarNT.headCell tc.headState tc.headOrig tc.headCur)] ++ v) (s : symbol T (TMtoGrammarNT T Λ)) (hs : s ∈ u ∨ s ∈ v) (q : Λ) (orig cur : Option T) : s ≠ symbol.nonterminal (TMtoGrammarNT.headCell q orig cur)

theorem tm_step_some_of_corresponds {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (q' : Λ) (action : Turing.TM0.Stmt (Option T)) (h_Mqc : M tc.headState tc.headCur = some (q', action)) : ∃ (tmCfg' : Turing.TM0.Cfg (Option T) Λ), Turing.TM0.step M tmCfg = some tmCfg'

theorem GI_preserved_simulating {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (tc : TwoTrackConfig) (tmCfg : Turing.TM0.Cfg (Option T) Λ) (hcorr : TMCorresponds tc tmCfg) (hreach : Turing.Reaches (Turing.TM0.step M) (Turing.TM0.init (List.map some (extractInput (twoTrackOriginals tc)))) tmCfg) (sf' : List (symbol T (TMtoGrammarNT T Λ))) (htrans : grammar_transforms (tmToGrammar T Λ M) (encodeTwoTrack tc) sf') : GI M sf'

Invariant preserved from simulating state.

theorem GI_preserved_cleanup {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (sf sf' : List (symbol T (TMtoGrammarNT T Λ))) (w : List T) (hhalt : (Turing.TM0.eval M (List.map some w)).Dom) (hcontent : terminalContent sf = w) (hhas_nt : ∃ s ∈ sf, isNonterminal s) (hno_start : ∀ s ∈ sf, s ≠ symbol.nonterminal TMtoGrammarNT.start) (hno_genMore : ∀ s ∈ sf, s ≠ symbol.nonterminal TMtoGrammarNT.genMore) (hno_headCell : ∀ s ∈ sf, ∀ (q : Λ) (orig cur : Option T), s ≠ symbol.nonterminal (TMtoGrammarNT.headCell q orig cur)) (htrans : grammar_transforms (tmToGrammar T Λ M) sf sf') : GI M sf'

theorem GI_preserved_done {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (w : List T) (_hhalt : (Turing.TM0.eval M (List.map some w)).Dom) (sf' : List (symbol T (TMtoGrammarNT T Λ))) (htrans : grammar_transforms (tmToGrammar T Λ M) (List.map symbol.terminal w) sf') : GI M sf'

Invariant preserved from done state (vacuously true).

theorem GI_preserved {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (sf sf' : List (symbol T (TMtoGrammarNT T Λ))) (hinv : GI M sf) (htrans : grammar_transforms (tmToGrammar T Λ M) sf sf') : GI M sf'

The invariant is preserved by grammar transforms.

theorem GI_reachable {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (sf : List (symbol T (TMtoGrammarNT T Λ))) (h : grammar_derives (tmToGrammar T Λ M) [symbol.nonterminal TMtoGrammarNT.start] sf) : GI M sf

Every reachable form satisfies the invariant.

Main soundness theorem

theorem tmToGrammar_halts_of_generates {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (w : List T) (h : grammar_generates (tmToGrammar T Λ M) w) : (Turing.TM0.eval M (List.map some w)).Dom

Soundness: If the grammar generates w, then TM halts on w.

theorem tmToGrammar_correct {T : Type} [Fintype T] {Λ : Type} [Inhabited Λ] [Fintype Λ] (M : Turing.TM0.Machine (Option T) Λ) (w : List T) : w ∈ grammar_language (tmToGrammar T Λ M) ↔ (Turing.TM0.eval M (List.map some w)).Dom

The grammar constructed from a TM generates exactly the TM's language.