Finite context-sensitive languages

Every finite language is context-sensitive. The proof uses an explicit empty grammar for the empty language, singleton-word context-sensitivity, and binary union closure.

theorem emptyLanguage_is_CS (T : Type) : is_CS ⊥

The empty language is context-sensitive.

theorem finsetLanguage_is_CS {T : Type} [Fintype T] (s : Finset (List T)) : is_CS fun (w : List T) => w ∈ s

The language represented by a finite set of words is context-sensitive.

theorem is_CS_of_finite_language {T : Type} [Fintype T] {L : Language T} (hfin : Set.Finite L) : is_CS L

Every finite language over a finite alphabet is context-sensitive.