Context-Sensitive Closure Under Terminal Bijections

This file proves that context-sensitive languages are preserved under bijective renaming of terminals.

theorem CS_of_bijemap_CS {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_CS L → is_CS (L.bijemapLang π)

The class of context-sensitive languages is closed under bijection between terminal alphabets.

theorem CS_of_bijemap_CS_rev {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_CS (L.bijemapLang π) → is_CS L

The converse direction.

@[simp]

theorem CS_bijemap_iff_CS {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_CS (L.bijemapLang π) ↔ is_CS L

A language is context-sensitive iff its image under a terminal bijection is.