Context-sensitive languages are closed under complement

The automaton-level inductive-counting theorem complements the nonempty part of a language. For a context-sensitive language L, we first remove ε, complement that positive LBA language, and then use the existing empty-word closure theorem to recover the ordinary complement Lᶜ.

This is the Immerman–Szelepcsényi theorem specialized to nondeterministic linear space.

theorem is_CS_complement {T : Type} [Fintype T] {L : Language T} (hL : is_CS L) : is_CS Lᶜ

The complement of a context-sensitive language over a finite alphabet is context-sensitive.

@[simp]

theorem CS_complement_iff {T : Type} [Fintype T] {L : Language T} : is_CS Lᶜ ↔ is_CS L

A language is context-sensitive if and only if its complement is.

theorem CS_closedUnderComplement {T : Type} [Fintype T] : ClosedUnderComplement is_CS

Context-sensitive languages over a finite alphabet are closed under complement.