EpsilonNFA

📁 Source: Mathlib/Computability/EpsilonNFA.lean

Statistics

Metric	Count
Definitions `toεNFA`, `εNFA`, `IsPath`, `accept`, `accepts`, `eval`, `evalFrom`, `instInhabited`, `instOne`, `instZero`, `start`, `step`, `stepSet`, `toNFA`, `εClosure`	15
Theorems `toεNFA_correct`, `toεNFA_evalFrom_match`, `toεNFA_εClosure`, `eq_of_nil`, `singleton`, `accept_one`, `accept_zero`, `evalFrom_append_singleton`, `evalFrom_empty`, `evalFrom_nil`, `evalFrom_singleton`, `eval_append_singleton`, `eval_nil`, `eval_singleton`, `isPath_append`, `isPath_iff`, `isPath_nil`, `isPath_singleton`, `mem_accepts_iff_exists_path`, `mem_evalFrom_iff_exists`, `mem_evalFrom_iff_exists_path`, `mem_stepSet_iff`, `mem_εClosure_iff_exists`, `mem_εClosure_iff_exists_path`, `pumping_lemma`, `start_one`, `start_zero`, `stepSet_empty`, `step_one`, `step_zero`, `subset_εClosure`, `toNFA_correct`, `toNFA_evalFrom_match`, `εClosure_empty`, `εClosure_univ`	35
Total	50

NFA

Definitions

Name	Category	Theorems
`toεNFA` 📖	CompOp	3 math math: `toεNFA_correct`, `toεNFA_evalFrom_match`, `toεNFA_εClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toεNFA_correct` 📖	mathematical	—	`εNFA.accepts` `toεNFA` `accepts`	—	`εNFA.accepts.eq_1` `εNFA.eval.eq_1` `toεNFA_evalFrom_match`
`toεNFA_evalFrom_match` 📖	mathematical	—	`εNFA.evalFrom` `toεNFA` `evalFrom`	—	`evalFrom.eq_1` `εNFA.evalFrom.eq_1` `toεNFA_εClosure` `Set.ext`
`toεNFA_εClosure` 📖	mathematical	—	`εNFA.εClosure` `toεNFA`	—	`Set.ext`

(root)

Definitions

Name	Category	Theorems
`εNFA` 📖	CompData	6 math math: `εNFA.accept_one`, `εNFA.step_zero`, `εNFA.accept_zero`, `εNFA.step_one`, `εNFA.start_zero`, `εNFA.start_one`

εNFA

Definitions

Name	Category	Theorems
`IsPath` 📖	CompData	8 math math: `isPath_singleton`, `mem_εClosure_iff_exists_path`, `mem_evalFrom_iff_exists_path`, `IsPath.singleton`, `mem_accepts_iff_exists_path`, `isPath_iff`, `isPath_append`, `isPath_nil`
`accept` 📖	CompOp	3 math math: `accept_one`, `accept_zero`, `mem_accepts_iff_exists_path`
`accepts` 📖	CompOp	3 math math: `toNFA_correct`, `mem_accepts_iff_exists_path`, `NFA.toεNFA_correct`
`eval` 📖	CompOp	3 math math: `eval_singleton`, `eval_nil`, `eval_append_singleton`
`evalFrom` 📖	CompOp	8 math math: `mem_evalFrom_iff_exists_path`, `evalFrom_append_singleton`, `evalFrom_singleton`, `toNFA_evalFrom_match`, `mem_evalFrom_iff_exists`, `NFA.toεNFA_evalFrom_match`, `evalFrom_nil`, `evalFrom_empty`
`instInhabited` 📖	CompOp	—
`instOne` 📖	CompOp	3 math math: `accept_one`, `step_one`, `start_one`
`instZero` 📖	CompOp	3 math math: `step_zero`, `accept_zero`, `start_zero`
`start` 📖	CompOp	5 math math: `eval_singleton`, `eval_nil`, `mem_accepts_iff_exists_path`, `start_zero`, `start_one`
`step` 📖	CompOp	5 math math: `isPath_singleton`, `step_zero`, `isPath_iff`, `step_one`, `mem_stepSet_iff`
`stepSet` 📖	CompOp	6 math math: `eval_singleton`, `evalFrom_append_singleton`, `evalFrom_singleton`, `stepSet_empty`, `mem_stepSet_iff`, `eval_append_singleton`
`toNFA` 📖	CompOp	2 math math: `toNFA_correct`, `toNFA_evalFrom_match`
`εClosure` 📖	CompData	12 math math: `subset_εClosure`, `mem_εClosure_iff_exists_path`, `eval_singleton`, `eval_nil`, `evalFrom_singleton`, `toNFA_evalFrom_match`, `mem_εClosure_iff_exists`, `NFA.toεNFA_εClosure`, `εClosure_empty`, `evalFrom_nil`, `εClosure_univ`, `mem_stepSet_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accept_one` 📖	mathematical	—	`accept` `εNFA` `instOne` `Set.univ`	—	—
`accept_zero` 📖	mathematical	—	`accept` `εNFA` `instZero` `Set` `Set.instEmptyCollection`	—	—
`evalFrom_append_singleton` 📖	mathematical	—	`evalFrom` `stepSet`	—	`evalFrom.eq_1`
`evalFrom_empty` 📖	mathematical	—	`evalFrom` `Set` `Set.instEmptyCollection`	—	`evalFrom_nil` `εClosure_empty` `evalFrom_append_singleton` `stepSet_empty`
`evalFrom_nil` 📖	mathematical	—	`evalFrom` `εClosure`	—	—
`evalFrom_singleton` 📖	mathematical	—	`evalFrom` `stepSet` `εClosure`	—	—
`eval_append_singleton` 📖	mathematical	—	`eval` `stepSet`	—	`evalFrom_append_singleton`
`eval_nil` 📖	mathematical	—	`eval` `εClosure` `start`	—	—
`eval_singleton` 📖	mathematical	—	`eval` `stepSet` `εClosure` `start`	—	—
`isPath_append` 📖	mathematical	—	`IsPath`	—	—
`isPath_iff` 📖	mathematical	—	`IsPath` `Set` `Set.instMembership` `step`	—	—
`isPath_nil` 📖	mathematical	—	`IsPath`	—	`isPath_iff`
`isPath_singleton` 📖	mathematical	—	`IsPath` `Set` `Set.instMembership` `step`	—	—
`mem_accepts_iff_exists_path` 📖	mathematical	—	`Language` `Language.instMembershipList` `accepts` `Set` `Set.instMembership` `start` `accept` `IsPath`	—	`mem_evalFrom_iff_exists` `eval.eq_1` `mem_evalFrom_iff_exists_path`
`mem_evalFrom_iff_exists` 📖	mathematical	—	`Set` `Set.instMembership` `evalFrom` `Set.instSingletonSet`	—	`mem_εClosure_iff_exists` `evalFrom_append_singleton`
`mem_evalFrom_iff_exists_path` 📖	mathematical	—	`Set` `Set.instMembership` `evalFrom` `Set.instSingletonSet` `IsPath`	—	`evalFrom_nil` `mem_εClosure_iff_exists_path` `List.reduceOption_replicate_none` `evalFrom_append_singleton` `mem_stepSet_iff` `mem_εClosure_iff_exists` `List.reduceOption_append` `List.reduceOption_cons_of_some` `isPath_append`
`mem_stepSet_iff` 📖	mathematical	—	`Set` `Set.instMembership` `stepSet` `εClosure` `step`	—	—
`mem_εClosure_iff_exists` 📖	mathematical	—	`Set` `Set.instMembership` `εClosure` `Set.instSingletonSet`	—	—
`mem_εClosure_iff_exists_path` 📖	mathematical	—	`Set` `Set.instMembership` `εClosure` `Set.instSingletonSet` `IsPath`	—	`List.replicate_add` `isPath_append` `IsPath.eq_of_nil`
`pumping_lemma` 📖	mathematical	`Language` `Language.instMembershipList` `accepts` `Fintype.card` `Set` `Set.fintype`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra` `Language.instMul` `Language.instSingletonList` `KStar.kstar` `Language.instKStar`	—	`NFA.pumping_lemma`
`start_one` 📖	mathematical	—	`start` `εNFA` `instOne` `Set.univ`	—	—
`start_zero` 📖	mathematical	—	`start` `εNFA` `instZero` `Set` `Set.instEmptyCollection`	—	—
`stepSet_empty` 📖	mathematical	—	`stepSet` `Set` `Set.instEmptyCollection`	—	`Set.iUnion_congr_Prop` `Set.iUnion_false` `Set.iUnion_empty`
`step_one` 📖	mathematical	—	`step` `εNFA` `instOne` `Set` `Set.instEmptyCollection`	—	—
`step_zero` 📖	mathematical	—	`step` `εNFA` `instZero` `Set` `Set.instEmptyCollection`	—	—
`subset_εClosure` 📖	mathematical	—	`Set` `Set.instHasSubset` `εClosure`	—	—
`toNFA_correct` 📖	mathematical	—	`NFA.accepts` `toNFA` `accepts`	—	—
`toNFA_evalFrom_match` 📖	mathematical	—	`NFA.evalFrom` `toNFA` `εClosure` `evalFrom`	—	—
`εClosure_empty` 📖	mathematical	—	`εClosure` `Set` `Set.instEmptyCollection`	—	`Set.eq_empty_of_forall_notMem`
`εClosure_univ` 📖	mathematical	—	`εClosure` `Set.univ`	—	`Set.eq_univ_of_univ_subset` `subset_εClosure`

εNFA.IsPath

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_nil` 📖	—	`εNFA.IsPath`	—	—	`εNFA.isPath_nil`
`singleton` 📖	mathematical	`Set` `Set.instMembership` `εNFA.step`	`εNFA.IsPath`	—	`εNFA.isPath_singleton`

---

← Back to Index