# The complete reachable-subset DFA of an epsilon-NFA

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-subset-construction-nfa-to-dfa/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-subset-construction-nfa-to-dfa-01 · ocme-new142-reader-adoption-20261021



## 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

S01 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

State0 reaches1 without input, so epsilon-close the start subset first.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

For both symbols, the moves from S are{1},{2}; closure leaves them unchanged.



S03 · impliesBefore

A=\{1\}

After

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

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

List both symbol branches from A.



S04 · impliesBefore

F=\{2\}

After

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

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

Accepting state2 has no input-consuming transitions; either next symbol reaches dead state.



S05 · impliesBefore

D=\varnothing

After

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

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

The empty subset loops on both symbols, making the DFA total.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

All four subsets are reachable; the eight transitions are closed and generate no others.



S07 · impliesBefore

w=\varepsilon

After

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

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The prefix-invariant base aligns the machines' initial reachable sets.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

NFA semantics and the subset transition definition preserve the invariant for any next symbol.



S09 · impliesBefore

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

After

L(D)=L(N)

Conditions: none

Rule: work · Uses: G1, S08, work

Leaf basis: work

The all-prefix invariant and common acceptance condition give full language equivalence.







## 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 orderClose the start and close again after every move.

All eight transitionsEach 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)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-subset-construction-nfa-to-dfa-01.json)