Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

NFAs can be constructed for union, concatenation, and Kleene star

Statement

Let L,K⊆Σ∗ be languages recognized by NFA's over the same alphabet Σ. Then L∪K, LK, and L∗ are also recognized by NFA's over Σ.

Facts & Assumptions

Given: NFA's NL and NK over Σ with recognized languages L and K.

[L1]

By Acceptance of a word by an NFA and the recognized language, an NFA accepts a word exactly when some full computation path ends in an accepting state.

[L2]

By Boolean operations on languages over a fixed alphabet, L∪K is the set-theoretic union of the two languages.

[L3]

By Language concatenation, powers, and Kleene star, LK={uv:u∈L, v∈K} and L∗ is the set of finite concatenations of words of L.

Proof

technique · direct
1.1L1L2givenconstruct

For union, first replace NL and NK by disjoint isomorphic copies. Add a fresh start state with ε-transitions to the copied start states, keep all copied transitions, and take the union of the two copied accepting sets as the new accepting set. By [L1] and [L2], every accepting run chooses one copy at the start and then stays inside that copy, so a word is accepted exactly when one of the two original machines accepts it. Thus the new language is L∪K.

1.2L1L3construct

For concatenation, take disjoint copies of NL and NK, use the copied start state of NL as the new start state, add an ε-transition from each copied accepting state of NL to the copied start state of NK, and designate only the copied accepting states of NK as accepting. Then [L1] and [L3] show that a successful run is exactly a decomposition of the input as uv with u∈L and v∈K, so the new machine recognizes LK.

1.3L1L3construct

For star, add a fresh start state, make it the only accepting state, add an ε-transition from it to the old start state of NL, and add ε-transitions from each old accepting state back to the fresh start state. By [L1] and [L3], every accepting run chooses finitely many factors from L, and every finite concatenation of words of L is accepted. Therefore the language recognized is L∗.

2.1step 1.1step 1.2step 1.3∎

Hence NFA's can be built for union, concatenation, and Kleene star.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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