Alphabeta Math
LemmaStatement: 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.

Epsilon-closure is a closure operator

Statement

Let N be an NFA with epsilon-moves and let S,T be subsets of its state set. Then:

  1. S⊆ECl⁡(S);
  2. if S⊆T, then ECl⁡(S)⊆ECl⁡(T);
  3. ECl⁡(ECl⁡(S))=ECl⁡(S).

Facts & Assumptions

Given: An NFA with epsilon-moves N and subsets S,T of its state set.

[L1]

By The epsilon-closure of a set of NFA states, a state lies in ECl⁡(S) exactly when it is reachable from some state of S by a finite chain of ε-transitions.

Proof

technique · direct
1.1L1given

For every s∈S, the length-zero ε-chain from s to itself shows s∈ECl⁡(S) by [L1]. Hence S⊆ECl⁡(S).

1.2L1given

Assume S⊆T and let q∈ECl⁡(S). By [L1], some ε-chain starts in a state of S and ends at q; because that start state also lies in T, the same chain shows q∈ECl⁡(T). Thus ECl⁡(S)⊆ECl⁡(T).

2.1L1step 1.1∎

Step 1.1 gives ECl⁡(S)⊆ECl⁡(ECl⁡(S)). For the reverse inclusion, let q∈ECl⁡(ECl⁡(S)). By [L1], there is an ε-chain from some r∈ECl⁡(S) to q, and again by [L1] there is an ε-chain from some s∈S to r. Concatenating the two finite chains gives an ε-chain from s to q, so q∈ECl⁡(S). Therefore ECl⁡(ECl⁡(S))=ECl⁡(S).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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