TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Regular languages are closed under left and right quotient with regular languages

Statement

Let $L, K \subseteq Σ^{*}$ be regular languages. Then the right quotient $L / K : = {x \in Σ^{*} : \exists y \in K, x y \in L}$ and the left quotient $K^{- 1} L : = {y \in Σ^{*} : \exists x \in K, x y \in L}$ are regular.

Facts & Assumptions

Given: Regular languages $L, K \subseteq Σ^{*}$ , together with DFA's $D_{L} = (Q_{L}, Σ, δ_{L}, q_{L}, F_{L})$ and $D_{K} = (Q_{K}, Σ, δ_{K}, q_{K}, F_{K})$ recognizing them.

[L1]

By Acceptance of a word by a DFA and the recognized language, a word is in the language of a DFA exactly when its run from the start state finishes in an accepting state.

[L2]

By Acceptance of a word by an NFA and the recognized language, an epsilon-NFA accepts exactly when some computation reaches an accepting state after the whole input is read.

[L3]

By DFAs and NFAs recognize the same languages, every language recognized by an NFA is regular.

[L4]

By The product construction gives DFA's for union and intersection, two DFA's over the same alphabet can be run in parallel by a product DFA.

Proof

technique · direct

1.1

For the right quotient, first build the product DFA of $D_{L}$ and $D_{K}$ from [L4]. Declare a state $q \in Q_{L}$ to be accepting in a new DFA $D_{R}$ exactly when some word $y$ drives the product machine from $(q, q_{K})$ to a state of $F_{L} \times F_{K}$ . The transition graph of $D_{R}$ is otherwise the same as that of $D_{L}$ .

L4givenconstruct

1.2

For the left quotient, let $S : = {δ_{L}^{*} (q_{L}, x) : x \in K} \subseteq Q_{L}$ . Add a fresh start state $s$ with an $ε$ -edge from $s$ to each state of $S$ , keep the letter transitions of $D_{L}$ on the old state set $Q_{L}$ , and keep $F_{L}$ as the accepting set. This gives an epsilon-NFA $N_{L}$ .

givenconstruct

2.1

If $D_{R}$ reads $x$ and ends in the state $q = δ_{L}^{*} (q_{L}, x)$ , then by construction $q$ is accepting exactly when some $y \in K$ also takes $D_{L}$ from $q$ to a state of $F_{L}$ . By [L1], this is equivalent to $x y \in L$ for some $y \in K$ . Hence $L (D_{R}) = L / K$ .

L1step 1.1

2.2

By [L2], a word $y$ is accepted by $N_{L}$ exactly when some state of $S$ reaches a state of $F_{L}$ after reading $y$ . By the definition of $S$ and then [L1], this happens exactly when there exists $x \in K$ with $x y \in L$ . Therefore $L (N_{L}) = K^{- 1} L$ .

L1L2step 1.2

3.1

Step 2.1 shows that the right quotient is recognized by a DFA. Step 2.2 shows that the left quotient is recognized by an NFA, so [L3] makes it regular. Thus both quotients are regular.

L3step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

H. Conrad Cunningham, Notes on Models of Computation, Chapter 4: Properties of Regular Languages (standard reference, not scraped)