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 for is_TM

The is_TM definition fixes the input embedding into the tape alphabet: input symbols are written as some (Sum.inl t), while the recognizer may use additional work symbols from an existential finite alphabet Γ.

To reduce to the existing tmToGrammar construction (which works with Option Δ for any Δ), we:

1. Apply tmToGrammar (T ⊕ Γ) Λ M to get a grammar over all tape symbols.
2. Apply pullbackGrammar to convert from grammar over T ⊕ Γ to grammar over T via the fixed Sum.inl inclusion.
3. Use pullbackGrammar_language and tmToGrammar_correct to establish the language correspondence.

theorem tm_recognizable_implies_re {T : Type} [DecidableEq T] [Fintype T] (L : Language T) : is_TM L → is_RE L

Every TM-recognizable language over a finite alphabet is generated by an unrestricted grammar.

theorem TM_subset_RE {T : Type} [DecidableEq T] [Fintype T] : TM ⊆ RE