# An existential finite accepting NFA path

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-nondeterministic-finite-automaton/)

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-nondeterministic-finite-automaton-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

The specified NFA accepts aab despite a dead alternative branch; an epsilon loop alone does not accept.

A complete finite relation with input-free null; no DFA-equivalence or subset-construction claim.





## Givens and symbols


- calc


- G1 — Q={q0,q1,qf,qd}, alphabet={a,b}, start q0,finals {qf}; all edges are [q0,null,q1],[q0,null,q0],[q0,a,qd],[q1,a,q1],[q1,b,qf],[qd,a,qd],[qd,b,qd]; word aab.


- q_d — nonfinal dead state
- F — final-state set
- null — epsilon-transition marker





## Rules and sources


- calc · prerequisite — Assume finite sets, finite strings and indices, stepwise function updates and induction on natural numbers; epsilon denotes the length-zero word.
- mko_definition · cited — Transitions are [from state,input symbol or null,to state]; null is epsilon and consumes no input. States are nonempty because they contain the start, while the alphabet and final-state set may be empty. The relation may be empty or multivalued and need not be deterministic or total. An empty word may be accepted by a finite epsilon path. An empty final set is valid and recognizes the empty language. One finite accepting path proves membership; bounded-search failure does not prove rejection. An epsilon cycle alone does not accept, and all branches need not accept. · mko-nondeterministic-finite-automaton





## Main derivation

S01 · impliesBefore

Q\ne\varnothing,\quad Q\cap\Sigma=\varnothing

After

\{[q_0,\text{null},q_1],[q_0,\text{null},q_0],[q_0,a,q_d],[q_1,a,q_1],[q_1,b,q_f],[q_d,a,q_d],[q_d,b,q_d]\}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

All seven legal relation entries are explicit; epsilon, branching and missing edges are allowed without a total deterministic table.



S02 · impliesBefore

w=aab,\quad|w|=3

After

[q_0,0]

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Initialize state and consumed-input position before reading any a.



S03 · impliesBefore

[q_0,0]

After

[q_1,0]\text{ via }[q_0,\text{null},q_1]

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Choose the epsilon edge to q1 without advancing position.



S04 · impliesBefore

[q_1,0],\quad w_1=a

After

[q_1,1]

Conditions: none

Rule: calc · Uses: G1, S01, S03

Leaf basis: calc

The a-loop consumes the first a while staying at q1.



S05 · impliesBefore

[q_1,1],\quad w_2=a

After

[q_1,2]

Conditions: none

Rule: calc · Uses: G1, S01, S04

Leaf basis: calc

The same legal loop reads the second a.



S06 · impliesBefore

[q_1,2],\quad w_3=b

After

[q_f,3]

Conditions: none

Rule: calc · Uses: G1, S01, S05

Leaf basis: calc

The b-edge consumes the last symbol and reaches a final state at word length.



S07 · impliesBefore

[q_f,3],\quad q_f\in F,\quad3=|w|

After

aab\text{ accepted}

Conditions: none

Rule: mko_definition · Uses: G1, S02, S03, S04, S05, S06

Leaf basis: mko_definition

Existence of this finite consuming path suffices; not every branch must accept.



S08 · impliesBefore

[q_0,0]\xrightarrow{a}[q_d,1]\xrightarrow{a}[q_d,2]\xrightarrow{b}[q_d,3]

After

q_d\notin F\text{ on this branch, but the accepting branch still exists}

Conditions: none

Rule: calc · Uses: G1, S01, S07

Leaf basis: calc

A different complete branch ends at nonfinal dead state qd without refuting the existential witness.



S09 · impliesBefore

[q_0,0]\xrightarrow{\varepsilon}[q_0,0];\quad F'=\varnothing

After

\text{epsilon cycle alone does not accept};\quad F'=\varnothing\text{ is a valid empty-language NFA}

Conditions: none

Rule: calc · Uses: G1, S01, S07, S08

Leaf basis: calc

The loop alone neither reaches a final nor consumes input; an empty final set is valid but can never meet final-state acceptance.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S09 · premise_audit · G1, S01, S07, S08 — An empty alphabet is valid too; a one-state start/final NFA with no edges accepts epsilon.
- S08 · premise_audit · G1, S01, S07 — Requiring every branch to accept would incorrectly reject this word.
- S07 · premise_audit · G1, S02, S03, S04, S05, S06 — Start, every edge and endpoint are explicit; no bounded no-hit inference is used.
- S06 · premise_audit · G1, S01, S05 — qf needs no outgoing edge; acceptance requires only the completed finite path.
- S05 · premise_audit · G1, S01, S04 — One cannot jump to position 3; b is still unread.
- S04 · premise_audit · G1, S01, S03 — An unchanged state is not epsilon; this step consumes a symbol.
- S03 · premise_audit · G1, S01, S02 — The epsilon edge does not read the first a.
- S02 · premise_audit · G1, S01 — Position zero is an initial value, not acceptance.
- S01 · premise_audit · G1 — qf may have no outgoing edges; the start lies in nonempty Q.





## Error controls and negative controls

Existential quantifierOne full accepting path certifies membership; dead branches do not prove rejection.

Epsilon positionnull edges keep position; input-symbol edges advance by one.


- One dead branch forces rejection of aab. → reject — Another complete accepting path is explicitly given.
- An epsilon cycle is itself acceptance. → reject — A finite path must still consume all input and end final.
- An NFA needs a nonempty alphabet and final set. → reject — Both may be empty; only states must be nonempty to contain a start.





## Result and limitations

The specified NFA accepts aab despite a dead alternative branch; an epsilon loop alone does not accept.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 2f202837026e2fb8c1a908dc18766c8e59c70be3d98e1011ca235aa4e3cd7172
- original source SHA-256: 2f202837026e2fb8c1a908dc18766c8e59c70be3d98e1011ca235aa4e3cd7172
- 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-nondeterministic-finite-automaton-01.json)