Context-Sensitive Languages Are Closed Under Intersection

We run two nondeterministic endmarker LBAs sequentially. The product machine stores, in each tape cell, one symbol for each source tape. While the first machine runs it changes only the first component. Once it reaches an accepting state, the product machine rewinds and runs the second machine on the still-untouched second component.

The construction is uniform in the finite input alphabet: it does not choose or require any distinguished input letters.

theorem CS_closedUnderIntersection {T : Type} [Fintype T] [DecidableEq T] : ClosedUnderIntersection is_CS

Context-sensitive languages are closed under intersection over every finite terminal alphabet. In particular, the theorem has no lower-bound or distinguished-letter hypothesis on the alphabet.