Language equivalence for Aho's bounded simulation

This module isolates the final grammar/machine language argument. Soundness is unconditional; the completeness hypothesis is precisely the uniform twenty-one-slots-per-terminal theorem supplied by the parse-directed scheduler.

theorem IndexedGrammar.Aho.language_eq_paddedReachLanguage_of_bounded_complete {T : Type} {g : IndexedGrammar T} [Fintype g.nt] [DecidableEq g.nt] (hNF : g.IsNormalForm) (hcomplete : ∀ {input : List T} (a : g.NFParse g.initial [] input), BoundedReaches g input (21 * input.length) (initialConfig g) (finalConfig g input.length)) : g.Language = paddedReachLanguage g

Once every concrete normal-form parse has a twenty-one-linear bounded run, semantic padded-row reachability recognizes exactly the language of the grammar.