Reducing indexed-to-CS inclusion to the finite normal-form core

The remaining constructive part of the inclusion Indexed ⊆ CS is the finite-alphabet, finite-support, normal-form indexed grammar simulation. This file keeps the class-level reduction explicit while the normal-form infrastructure is developed in the grammar modules.

theorem finite_normalForm_CS_core_of_LBA_core (hcore : ∀ {A : Type} [inst : Fintype A] [inst_1 : DecidableEq A] [Inhabited A] (g : IndexedGrammar A) [Fintype g.nt] [Fintype g.flag] [inst_5 : DecidableEq g.nt], g.IsNormalForm → is_LBA_pos g.Language) {A : Type} [Fintype A] [DecidableEq A] [Inhabited A] (g : IndexedGrammar A) [Fintype g.nt] [Fintype g.flag] [DecidableEq g.nt] : g.IsNormalForm → is_CS g.Language

The LBA finite-normal-form core implies the context-sensitive finite-normal-form core.

theorem is_CS_of_is_Indexed_of_finite_normalForm_core {T : Type} (hcore : ∀ {A : Type} [Fintype A] [DecidableEq A] [Inhabited A] (g : IndexedGrammar A) [Fintype g.nt] [Fintype g.flag] [inst : DecidableEq g.nt], g.IsNormalForm → is_CS g.Language) {L : Language T} (hL : is_Indexed L) : is_CS L

With epsilon elimination discharged, the remaining class-level indexed-to-CS reduction only needs the finite normal-form core. No inhabitedness assumption on the terminal alphabet is needed: over an empty alphabet every language is a subset of the singleton language {ε} and is finite.

theorem is_CS_of_is_Indexed_of_finite_normalForm_LBA_core {T : Type} (hcore : ∀ {A : Type} [inst : Fintype A] [inst_1 : DecidableEq A] [Inhabited A] (g : IndexedGrammar A) [Fintype g.nt] [Fintype g.flag] [inst_5 : DecidableEq g.nt], g.IsNormalForm → is_LBA_pos g.Language) {L : Language T} (hL : is_Indexed L) : is_CS L

LBA-core variant of is_CS_of_is_Indexed_of_finite_normalForm_core.

theorem finite_normalForm_indexed_language_is_LBA_pos {A : Type} [Fintype A] [DecidableEq A] [Inhabited A] (g : IndexedGrammar A) [Fintype g.nt] [Fintype g.flag] [DecidableEq g.nt] (hNF : g.IsNormalForm) : is_LBA_pos g.Language

The completed Aho simulation supplies the finite normal-form LBA core used by the class-level reduction.

theorem is_CS_of_is_Indexed {T : Type} {L : Language T} (hL : is_Indexed L) : is_CS L

Every indexed language is context-sensitive.

theorem Indexed_subclass_CS {T : Type} : Indexed ⊆ CS

Class-level capstone: the finite normal-form Aho LBA core, together with the preceding finite-support normalization and empty-word reduction, places every indexed language in CS.