The complete reachable-subset DFA of an epsilon-NFA

Goal and scope

List every transition and prove language equivalence by prefix induction.

Only reachable subsets are retained, explicitly including the empty dead state.

Givens and symbols

• work

• G1 — Q={0,1,2}, Sigma={a,b}, start0, finals{2}. The full NFA table has(0,epsilon)={1},(1,a)={1},(1,b)={2}; all other pairs in Q times{epsilon,a,b} have empty transitions.

• S,A,F,D — four reachable subsets
• R_N(w) — epsilon-closed NFA states reachable after w

Rules and sources

• mko_definition · cited — The DFA start is epsilon-closure({q0}). For subset S and symbol a, delta_D(S,a)=epsilon-closure(move(S,a)). A subset accepts exactly when its intersection with the NFA final set is nonempty. Empty subset is a legal dead state. Restriction to reachable subsets is allowed only when explicit. For every word prefix, the DFA subset equals all epsilon-closed NFA states reachable after that prefix; finite-word testing alone does not prove language equivalence. · mko-subset-construction-nfa-to-dfa
• work · prerequisite — Epsilon closure includes zero or finitely many epsilon steps; move unions symbol successors of every active state; word-length induction and DFA/NFA acceptance definitions.

Main derivation

\operatorname{cl}_\varepsilon(\{0\})

S=\{0,1\}\text{ is the DFA start}

\delta_D(S,s)=\operatorname{cl}_\varepsilon(\operatorname{move}(S,s))

\delta_D(S,a)=A=\{1\},\quad\delta_D(S,b)=F=\{2\}

A=\{1\}

\delta_D(A,a)=A,\quad\delta_D(A,b)=F

F=\{2\}

\delta_D(F,a)=D=\varnothing,\quad\delta_D(F,b)=D

D=\varnothing

\delta_D(D,a)=D,\quad\delta_D(D,b)=D

S\xrightarrow{a}A,\ S\xrightarrow{b}F,\ S\xrightarrow{ba}D

Q_D=\{S,A,F,D\},\quad F_D=\{F\}

w=\varepsilon

\delta_D^*(S,\varepsilon)=S=\operatorname{cl}_\varepsilon(\{0\})=R_N(\varepsilon)

\delta_D^*(S,w)=R_N(w),\quad s\in\Sigma

\delta_D^*(S,ws)=\operatorname{cl}_\varepsilon(\operatorname{move}(R_N(w),s))=R_N(ws)

\delta_D^*(S,w)\cap\{2\}\ne\varnothing\iff R_N(w)\cap\{2\}\ne\varnothing

L(D)=L(N)

Substeps and lemmas

No substeps in this guide.

Reverse audits

• S09 · premise_audit · G1, S08, work — A few tested words have not replaced the induction proof.
• S08 · premise_audit · G1, S07, work — w is arbitrary and both symbols are covered, giving induction over all words.
• S07 · premise_audit · G1, S06, work — R_N denotes all epsilon-closed reachable states after a prefix.
• S06 · premise_audit · G1, S05, work — Acceptance means nonempty intersection with{2}, not general equality to the final set.
• S05 · premise_audit · G1, S04, work — Deleting the empty state without handling incoming dead transitions leaves an incomplete DFA.
• S04 · premise_audit · G1, S03, work — An accepting subset still needs complete DFA transitions.
• S03 · premise_audit · G1, S02, work — No epsilon edge leaves1, so closure remains singleton.
• S02 · premise_audit · G1, S01, work — Move includes every active NFA state, not one chosen path.
• S01 · premise_audit · G1, work — Starting from{0} alone would miss a and b paths.

Error controls and negative controls

Closure order

Close the start and close again after every move.

All eight transitions

Each of four reachable states has transitions on both a,b.

• The DFA starts at{0}. → reject — 0 epsilon-reaches1, so the start is{0,1}.
• The empty subset is not a legal state. → reject — It represents loss of all NFA branches and is the dead state needed for totality.
• Testing a,b proves full equivalence. → reject — Full equivalence comes from arbitrary-prefix induction, not finite tests.

Result and limitations

The reachable DFA has four states and eight transitions and is equivalent to the epsilon-NFA for every word.

Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 66fd6e76217271463939e2074eb9e586f0571bdfa596621064cb082086e08ad0
• original source SHA-256: 66fd6e76217271463939e2074eb9e586f0571bdfa596621064cb082086e08ad0
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

Same-source full JSON (formulas, ASTs, controls and revision log)