Context-Sensitive Closure Under Reversal

This file proves that context-sensitive languages are closed under word reversal.

theorem CS_of_reverse_CS {T : Type} (L : Language T) : is_CS L → is_CS L.reverse

The class of context-sensitive languages is closed under reversal.

theorem CS_of_reverse_CS_rev {T : Type} (L : Language T) : is_CS L.reverse → is_CS L

The converse direction: if the reversal is context-sensitive then so is the original.

@[simp]

theorem CS_reverse_iff_CS {T : Type} (L : Language T) : is_CS L.reverse ↔ is_CS L

A language is context-sensitive iff its reversal is.

theorem CS_closedUnderReverse {T : Type} : ClosedUnderReverse is_CS

The class of context-sensitive languages is closed under reversal.