Pipeline-generated

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.

✓ 3 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

Finite-Automata Transition and Determinisation Interfaces: Examples

1 · Prerequisites

2 · Summary

The first example evaluates closure and six word transitions in a fully specified three-state automaton. The next computes its reachable subset DFA and proves the table exhaustive for all words. A two-state counterexample then separates the failures caused by omitting initial closure and by omitting closure after a letter.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09Open item page →

Epsilon closure and word transitions on three states

Example

Let $Q = {p, q, r}$ , $Σ = {a, b}$ , start $p$ , and $F = {r}$ , where the displayed states and letters are distinct. Specify the entire transition table by

State	$ε$	$a$	$b$
$p$	${q}$	$\emptyset$	$\emptyset$
$q$	$\emptyset$	${q, r}$	$\emptyset$
$r$	$\emptyset$	$\emptyset$	${r}$

Then $ECl ({p}) = {p, q}$ and $ECl (\emptyset) = \emptyset$ . The state sets from $p$ on $ε, a, a a, a b, b, a b a$ are, respectively, ${p, q}, {q, r}, {q, r}, {r}, \emptyset, \emptyset$ . Thus $a, a a, a b$ are accepted and $ε, b, a b a$ are rejected.

Facts & Assumptions

Given: The nine table entries, start $p$ , and final set ${r}$ above; write $E = ECl$ .

[F1]

Epsilon closure is finite saturation; the empty-word value is the initial closure and each next letter takes a successor union followed by closure. Acceptance tests nonempty intersection with the final set (Epsilon-NFAs, finite epsilon closure, and extended word transition).

Verification

1.1

The table gives a subset of $Q$ at each of its nine state/label pairs, so the transition is total on the required domain. The finite sets, start and finals meet the epsilon-NFA requirements. Starting from ${p}$ , saturation adds $q$ in one stage and adds nothing thereafter, since neither $q$ nor $r$ has an epsilon successor. Thus $E ({p}) = {p, q}$ ; more generally $E (T) = T \cup {q}$ if $p \in T$ , and $E (T) = T$ otherwise. In particular $E (\emptyset) = \emptyset$ , $E ({q, r}) = {q, r}$ and $E ({r}) = {r}$ .

givenF1

2.1

The empty-word value is $\hat{δ} (p, ε) = {p, q}$ . For $a$ , the successor union from this set is $δ (p, a) \cup δ (q, a) = \emptyset \cup {q, r} = {q, r}$ , already closed; hence $\hat{δ} (p, a) = {q, r}$ . For $b$ , the corresponding union is $\emptyset \cup \emptyset = \emptyset$ , so $\hat{δ} (p, b) = \emptyset$ .

step 1.1givenF1

3.1

After $a$ the set is ${q, r}$ . Its $a$ -successor union is ${q, r} \cup \emptyset = {q, r}$ , and its $b$ -successor union is $\emptyset \cup {r} = {r}$ . Both are closed, giving $\hat{δ} (p, a a) = {q, r}$ and $\hat{δ} (p, a b) = {r}$ . From ${r}$ the $a$ -successor union is empty, so $\hat{δ} (p, a b a) = \emptyset$ .

step 1.1step 2.1givenF1

4.1

The sets for $a, a a, a b$ each contain $r$ , whereas the sets for $ε, b, a b a$ do not. Intersecting them with $F = {r}$ gives ${r}$ in the first three cases and $\emptyset$ in the other three, proving every asserted acceptance and rejection.

step 2.1step 3.1F1given∎

Source

The witness is original to this example. The calculation uses the closure and word-transition rules of Gallier, Definitions 3.6–3.7, pp. 30–32, via the local interface.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09Open item page →

A complete determinisation table for a three-state epsilon-NFA

Example

Take $Q = {p, q, r}$ , $Σ = {a, b}$ , start $p$ , and $F = {r}$ . Define $δ (p, ε) = {q}$ , $δ (q, a) = {q, r}$ , $δ (r, b) = {r}$ , and all other state/label entries to be empty. All state names and letter names within their respective sets are distinct. Put $A = {p, q}, B = {q, r}, C = {r}, Z = \emptyset .$ The reachable part of the full subset DFA has start $A$ , accepting states $B, C$ , and complete table

State	$a$	$b$
$A$	$B$	$Z$
$B$	$B$	$C$
$C$	$Z$	$C$
$Z$	$Z$	$Z$

Exactly these four states are reachable. The other four states of $P (Q)$ are unreachable.

Facts & Assumptions

Given: The entire NFA prescription above; $A, B, C, Z$ denote the specified subsets, and $E = ECl$ .

[F1]

Epsilon closure is the least epsilon-closed superset, computed by finite saturation (Epsilon-NFAs, finite epsilon closure, and extended word transition).

[F2]

The subset DFA has $μ (T, x) = E (⋃_{q \in T} δ (q, x))$ , start $E ({p})$ , and final subsets meeting $F$ . Its extended transition equals the NFA word transition from that start and its full state set has $2^{∣ Q ∣}$ elements (Subset construction and its exact reachability invariant).

[F3]

Induction from zero and successor proves a property for every natural length (The principle of mathematical induction).

Verification

1.1

There are nine domain pairs; the three prescribed nonempty entries and the six empty entries all lie in $P (Q)$ . This makes a total epsilon-NFA with the stated start and finals. Its only epsilon edge is from $p$ to $q$ , so saturation adds $q$ precisely when $p$ is present and $q$ absent. Hence $E ({p}) = A$ , and $A, B, C, Z$ are each closed.

givenF1

2.1

From $A$ , the $a$ -union is $\emptyset \cup {q, r} = B$ and the $b$ -union is $\emptyset \cup \emptyset = Z$ . From $B$ , the $a$ -union is ${q, r} \cup \emptyset = B$ and the $b$ -union is $\emptyset \cup {r} = C$ . Closing these unions leaves them unchanged. This computes the first two rows.

step 1.1givenF2

2.2

From $C$ , the $a$ -union is $\emptyset = Z$ and the $b$ -union is ${r} = C$ . From $Z$ , both unions are empty, so both transitions return $Z$ . Again each result is closed. This computes the last two rows.

step 1.1givenF2

3.1

The start is $A$ , and the words $ε, a, a b, b$ reach $A, B, C, Z$ , respectively: the middle two follow the transitions $A \overset{a}{\to} B \overset{b}{\to} C$ , and $A \overset{b}{\to} Z$ . Thus each of the four states is reachable.

step 1.1step 2.1F2

4.1

Every word reaches one of these four states. Indeed at length zero the state is $A$ . If a prefix reaches one of the four, then appending $a$ or $b$ reaches one of the four by the computed rows. Induction on word length therefore gives the assertion for every word; the induction applies to the property that every word of a given length reaches the four-state set.

step 2.1step 2.2step 3.1F2F3

5.1

The eight subsets are $Z, {p}, {q}, C, A, {p, r}, B, {p, q, r}$ . By the two reachability implications, precisely ${p}, {q}, {p, r}, {p, q, r}$ are unreachable. Of the reachable subsets, $B \cap F = C \cap F = {r}$ and $A \cap F = Z \cap F = \emptyset$ , giving exactly the displayed accepting states. The full DFA also designates its unreachable subsets containing $r$ as final; the table states the finals of its reachable part.

step 3.1step 4.1givenF2∎

Source

This independently specified witness instantiates Aho, Lecture 3 §2. The table is for the reachable part of the full-power-set construction; its exhaustiveness follows from the induction above.

CounterexampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09Open item page →

Dropping epsilon closure changes the accepted language

Statement refuted

“For every epsilon-NFA, determinisation preserves the accepted language if the start closure is omitted, or if post-letter closure is omitted.” In the first variant only the start changes to ${q_{0}}$ ; in the second the start remains $E ({q_{0}})$ and the letter map changes to $ν (S, a) = ⋃_{q \in S} δ (q, a)$ . Both variants retain the full power set and the final-subset intersection test.

Facts & Assumptions

Given: We test the two stated variants separately, writing $E = ECl$ .

[F1]

An epsilon-NFA starts its extended transition at $E ({q_{0}})$ , closes every post-letter successor union, and accepts exactly when the resulting subset meets $F$ (Epsilon-NFAs, finite epsilon closure, and extended word transition).

[F2]

The correct subset DFA has that closed start, those closed successor unions, and final subsets meeting $F$ , with exactly the same accepted language (Subset construction and its exact reachability invariant).

Counterexample

1.1

Let $Q = {p, q}$ , $Σ = {a}$ , start $p$ , and $F = {q}$ , with $p \neq q$ . Put $δ (p, ε) = {q}$ , $δ (q, a) = {p}$ , $δ (p, a) = \emptyset$ , and $δ (q, ε) = \emptyset$ . All four domain entries are specified subsets of the finite state set, so this is an epsilon-NFA. Saturation from ${p}$ gives ${p, q}$ and then stays there; thus $E ({p}) = {p, q}$ .

constructF1

2.1

In the correct construction the empty word reaches ${p, q}$ , whose intersection with $F$ is ${q}$ , so it is accepted. In the first defective construction the empty word leaves the start at ${p}$ , whose intersection with $F$ is empty, so it is rejected. This mismatch occurs before any letter transition, even though all post-letter closures in that variant are retained.

step 1.1F1F2given

2.2

In the second defective construction the start is correctly ${p, q}$ , but on the single letter $a$ its successor union is $δ (p, a) \cup δ (q, a) = \emptyset \cup {p} = {p}$ . Omitting closure leaves that set, disjoint from $F$ , so the variant rejects $a$ . The correct construction instead closes it to $E ({p}) = {p, q}$ , which meets $F$ ; equivalently the original NFA has the accepting path $p \overset{ε}{\to} q \overset{a}{\to} p \overset{ε}{\to} q$ .

step 1.1F1F2given

3.1

Each defective rule still gives a total DFA on the finite power set: its letter outputs are subsets and each of its starts is a subset. The failures are therefore language failures, not missing transitions. The empty word distinguishes the first variant and $a$ distinguishes the second, refuting both universal preservation claims.

step 2.1step 2.2F2discharge-construct∎

Source

The two-state witness is original. It tests the two separate closures in Aho, Lecture 3 §2; neither is dispensable in general.

Finite-Automata Transition and Determinisation Interfaces: Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Epsilon closure and word transitions on three states

Example

Facts & Assumptions

Verification

Source

A complete determinisation table for a three-state epsilon-NFA

Example

Facts & Assumptions

Verification

Source

Dropping epsilon closure changes the accepted language

Statement refuted

Facts & Assumptions

Counterexample

Source

Sources