TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30

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.

The product construction gives DFA's for union and intersection

Statement

Let $D_{1} = (Q_{1}, Σ, δ_{1}, q_{1}, F_{1})$ and $D_{2} = (Q_{2}, Σ, δ_{2}, q_{2}, F_{2})$ be DFA's over the same alphabet, and let $L_{i} = L (D_{i})$ .

Then there is a DFA over $Σ$ recognizing $L_{1} \cap L_{2}$ , and there is a DFA over $Σ$ recognizing $L_{1} \cup L_{2}$ .

Facts & Assumptions

Given: Two DFA's $D_{1}$ and $D_{2}$ over the same alphabet $Σ$ .

[L1]

A word is accepted by a DFA exactly when the extended transition from the start state lands in an accepting state, by Acceptance of a word by a DFA and the recognized language.

[L2]

For languages over a fixed alphabet, union and intersection are the set-theoretic operations $L \cup K$ and $L \cap K$ , by Boolean operations on languages over a fixed alphabet.

Proof

technique · direct

1.1

Define the product machine $D_{\times}$ to have state set $Q_{1} \times Q_{2}$ , start state $(q_{1}, q_{2})$ , and transition rule $δ_{\times} ((p, r), a) : = (δ_{1} (p, a), δ_{2} (r, a)) .$ Intuitively, $D_{\times}$ runs the two machines in parallel on the same input.

givenconstruct

1.2

We claim that for every pair of states $(p, r)$ and every word $w$ , $δ_{\times}^{*} ((p, r), w) = (δ_{1}^{*} (p, w), δ_{2}^{*} (r, w)) .$ The claim is proved by induction on the length of $w$ : it is immediate for $ε$ , and appending one letter updates both coordinates exactly as the component machines do.

constructinduction

2.1

If the accepting set is $F_{\cap} : = F_{1} \times F_{2}$ , then step 1.2 and [L1] show that a word $w$ is accepted exactly when $δ_{1}^{*} (q_{1}, w) \in F_{1}$ and $δ_{2}^{*} (q_{2}, w) \in F_{2}$ , that is, exactly when $w \in L_{1} \cap L_{2}$ . By [L2], this machine recognizes the intersection.

L1L2step 1.2

2.2

If the accepting set is $F_{\cup} : = (F_{1} \times Q_{2}) \cup (Q_{1} \times F_{2})$ , then step 1.2 and [L1] show that a word $w$ is accepted exactly when at least one component machine accepts $w$ , that is, exactly when $w \in L_{1} \cup L_{2}$ . By [L2], this machine recognizes the union.

L1L2step 1.2

3.1

Therefore the product construction yields DFA's for both intersection and union over the fixed alphabet $Σ$ .

step 1.1step 2.1step 2.2∎

Depends on

Used by

Dependency tree · two levels

6 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

Jean Gallier and Jocelyn Quaintance, Introduction to the Theory of Computation: Some Notes for CIS511 (standard reference, not scraped)
John Watrous, Introduction to the Theory of Computing, Lecture 4 (standard reference, not scraped)