NFA

📁 Source: Mathlib/Computability/NFA.lean

Statistics

Metric	Count
Definitions `toNFA`, `NFA`, `supp`, `accept`, `accepts`, `acceptsFrom`, `eval`, `evalFrom`, `instInhabited`, `reverse`, `start`, `step`, `stepSet`, `toDFA`	14
Theorems `toNFA_accept`, `toNFA_correct`, `toNFA_evalFrom_match`, `toNFA_start`, `toNFA_step`, `of_reverse`, `reverse`, `isRegular_reverse_iff`, `acceptsFrom_iUnion`, `acceptsFrom_iUnion₂`, `acceptsFrom_union`, `accepts_eq_acceptsFrom_start`, `accepts_iff_exists_path`, `append_mem_acceptsFrom`, `append_preimage_acceptsFrom`, `cons_mem_acceptsFrom`, `cons_preimage_acceptsFrom`, `disjoint_evalFrom_reverse`, `disjoint_evalFrom_reverse_iff`, `disjoint_stepSet_reverse`, `evalFrom_append`, `evalFrom_append_singleton`, `evalFrom_biUnion`, `evalFrom_cons`, `evalFrom_eq_biUnion_singleton`, `evalFrom_iUnion`, `evalFrom_iUnion₂`, `evalFrom_nil`, `evalFrom_singleton`, `evalFrom_union`, `eval_append_singleton`, `eval_nil`, `eval_singleton`, `mem_accepts`, `mem_acceptsFrom`, `mem_accepts_reverse`, `mem_evalFrom_iff_exists`, `mem_evalFrom_iff_nonempty_path`, `mem_stepSet`, `nil_mem_acceptsFrom`, `pumping_lemma`, `reverse_accept`, `reverse_reverse`, `reverse_start`, `reverse_step`, `stepSet_empty`, `stepSet_singleton`, `stepSet_union`, `toDFA_correct`	49
Total	63

DFA

Definitions

Name	Category	Theorems
`toNFA` 📖	CompOp	5 math math: `toNFA_start`, `toNFA_correct`, `toNFA_step`, `toNFA_evalFrom_match`, `toNFA_accept`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNFA_accept` 📖	mathematical	—	`NFA.accept` `toNFA` `accept`	—	—
`toNFA_correct` 📖	mathematical	—	`NFA.accepts` `toNFA` `accepts`	—	`Language.ext` `NFA.mem_accepts` `toNFA_start` `toNFA_evalFrom_match` `Set.mem_singleton_iff`
`toNFA_evalFrom_match` 📖	mathematical	—	`NFA.evalFrom` `toNFA` `Set` `Set.instSingletonSet` `evalFrom`	—	`Set.iUnion_congr_Prop` `Set.iUnion_iUnion_eq_left`
`toNFA_start` 📖	mathematical	—	`NFA.start` `toNFA` `Set` `Set.instSingletonSet` `start`	—	—
`toNFA_step` 📖	mathematical	—	`NFA.step` `toNFA` `Set` `Set.instSingletonSet` `step`	—	—

Language

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_reverse_iff` 📖	mathematical	—	`IsRegular` `reverse`	—	`IsRegular.of_reverse` `IsRegular.reverse`

Language.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_reverse` 📖	—	`Language.IsRegular` `Language.reverse`	—	—	`reverse` `Language.reverse_reverse`
`reverse` 📖	mathematical	`Language.IsRegular`	`Language.reverse`	—	`Language.ext` `NFA.toDFA_correct` `DFA.toNFA_correct`

NFA

Definitions

Name	Category	Theorems
`accept` 📖	CompOp	7 math math: `reverse_start`, `accepts_iff_exists_path`, `DFA.toNFA_accept`, `nil_mem_acceptsFrom`, `mem_acceptsFrom`, `mem_accepts`, `reverse_accept`
`accepts` 📖	CompOp	8 math math: `εNFA.toNFA_correct`, `DFA.toNFA_correct`, `accepts_iff_exists_path`, `toDFA_correct`, `toεNFA_correct`, `accepts_eq_acceptsFrom_start`, `mem_accepts_reverse`, `mem_accepts`
`acceptsFrom` 📖	CompOp	10 math math: `acceptsFrom_union`, `cons_preimage_acceptsFrom`, `acceptsFrom_iUnion₂`, `cons_mem_acceptsFrom`, `nil_mem_acceptsFrom`, `mem_acceptsFrom`, `accepts_eq_acceptsFrom_start`, `append_mem_acceptsFrom`, `acceptsFrom_iUnion`, `append_preimage_acceptsFrom`
`eval` 📖	CompOp	3 math math: `eval_singleton`, `eval_append_singleton`, `eval_nil`
`evalFrom` 📖	CompOp	20 math math: `evalFrom_append`, `evalFrom_iUnion₂`, `evalFrom_eq_biUnion_singleton`, `evalFrom_cons`, `DFA.toNFA_evalFrom_match`, `disjoint_evalFrom_reverse_iff`, `mem_evalFrom_iff_exists`, `mem_acceptsFrom`, `evalFrom_nil`, `εNFA.toNFA_evalFrom_match`, `evalFrom_append_singleton`, `mem_accepts`, `evalFrom_union`, `evalFrom_singleton`, `append_mem_acceptsFrom`, `toεNFA_evalFrom_match`, `evalFrom_iUnion`, `evalFrom_biUnion`, `mem_evalFrom_iff_nonempty_path`, `append_preimage_acceptsFrom`
`instInhabited` 📖	CompOp	—
`reverse` 📖	CompOp	7 math math: `reverse_step`, `reverse_start`, `reverse_reverse`, `disjoint_evalFrom_reverse_iff`, `mem_accepts_reverse`, `disjoint_stepSet_reverse`, `reverse_accept`
`start` 📖	CompOp	8 math math: `eval_singleton`, `DFA.toNFA_start`, `reverse_start`, `accepts_iff_exists_path`, `eval_nil`, `accepts_eq_acceptsFrom_start`, `mem_accepts`, `reverse_accept`
`step` 📖	CompOp	4 math math: `reverse_step`, `DFA.toNFA_step`, `stepSet_singleton`, `mem_stepSet`
`stepSet` 📖	CompOp	12 math math: `stepSet_union`, `eval_singleton`, `eval_append_singleton`, `cons_preimage_acceptsFrom`, `evalFrom_cons`, `cons_mem_acceptsFrom`, `evalFrom_append_singleton`, `evalFrom_singleton`, `disjoint_stepSet_reverse`, `stepSet_empty`, `stepSet_singleton`, `mem_stepSet`
`toDFA` 📖	CompOp	1 math math: `toDFA_correct`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acceptsFrom_iUnion` 📖	mathematical	—	`acceptsFrom` `Set.iUnion`	—	`Language.ext` `evalFrom_iUnion` `Set.mem_iUnion` `Set.mem_setOf_eq`
`acceptsFrom_iUnion₂` 📖	mathematical	—	`acceptsFrom` `Set.iUnion`	—	`acceptsFrom_iUnion`
`acceptsFrom_union` 📖	mathematical	—	`acceptsFrom` `Set` `Set.instUnion` `Language` `Language.instAdd`	—	`Language.add_def` `Language.ext` `evalFrom_union`
`accepts_eq_acceptsFrom_start` 📖	mathematical	—	`accepts` `acceptsFrom` `start`	—	—
`accepts_iff_exists_path` 📖	mathematical	—	`Language` `Language.instMembershipList` `accepts` `Set` `Set.instMembership` `start` `accept` `Path`	—	`mem_evalFrom_iff_exists`
`append_mem_acceptsFrom` 📖	mathematical	—	`Language` `Language.instMembershipList` `acceptsFrom` `evalFrom`	—	`evalFrom_append`
`append_preimage_acceptsFrom` 📖	mathematical	—	`Set.preimage` `acceptsFrom` `evalFrom`	—	`Set.ext` `append_mem_acceptsFrom`
`cons_mem_acceptsFrom` 📖	mathematical	—	`Language` `Language.instMembershipList` `acceptsFrom` `stepSet`	—	—
`cons_preimage_acceptsFrom` 📖	mathematical	—	`Set.preimage` `acceptsFrom` `stepSet`	—	`Set.ext` `cons_mem_acceptsFrom`
`disjoint_evalFrom_reverse` 📖	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `evalFrom` `reverse`	—	—	`disjoint_comm` `disjoint_stepSet_reverse`
`disjoint_evalFrom_reverse_iff` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `evalFrom` `reverse`	—	`disjoint_evalFrom_reverse`
`disjoint_stepSet_reverse` 📖	mathematical	—	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `stepSet` `reverse`	—	`not_iff_not`
`evalFrom_append` 📖	mathematical	—	`evalFrom`	—	—
`evalFrom_append_singleton` 📖	mathematical	—	`evalFrom` `stepSet`	—	`evalFrom_append`
`evalFrom_biUnion` 📖	mathematical	—	`evalFrom` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.biUnion_and'` `evalFrom_iUnion`
`evalFrom_cons` 📖	mathematical	—	`evalFrom` `stepSet`	—	—
`evalFrom_eq_biUnion_singleton` 📖	mathematical	—	`evalFrom` `Set.iUnion` `Set` `Set.instMembership` `Set.instSingletonSet`	—	`Set.biUnion_of_singleton`
`evalFrom_iUnion` 📖	mathematical	—	`evalFrom` `Set.iUnion`	—	`Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_comm`
`evalFrom_iUnion₂` 📖	mathematical	—	`evalFrom` `Set.iUnion`	—	`evalFrom_iUnion`
`evalFrom_nil` 📖	mathematical	—	`evalFrom`	—	—
`evalFrom_singleton` 📖	mathematical	—	`evalFrom` `stepSet`	—	—
`evalFrom_union` 📖	mathematical	—	`evalFrom` `Set` `Set.instUnion`	—	`stepSet_union`
`eval_append_singleton` 📖	mathematical	—	`eval` `stepSet`	—	`evalFrom_append`
`eval_nil` 📖	mathematical	—	`eval` `start`	—	—
`eval_singleton` 📖	mathematical	—	`eval` `stepSet` `start`	—	—
`mem_accepts` 📖	mathematical	—	`Language` `Language.instMembershipList` `accepts` `Set` `Set.instMembership` `accept` `evalFrom` `start`	—	—
`mem_acceptsFrom` 📖	mathematical	—	`Language` `Language.instMembershipList` `acceptsFrom` `Set` `Set.instMembership` `accept` `evalFrom`	—	—
`mem_accepts_reverse` 📖	mathematical	—	`Language` `Language.instMembershipList` `accepts` `reverse`	—	—
`mem_evalFrom_iff_exists` 📖	mathematical	—	`Set` `Set.instMembership` `evalFrom` `Set.instSingletonSet`	—	`evalFrom_eq_biUnion_singleton`
`mem_evalFrom_iff_nonempty_path` 📖	mathematical	—	`Set` `Set.instMembership` `evalFrom` `Set.instSingletonSet` `Path`	—	`stepSet_singleton` `mem_evalFrom_iff_exists` `evalFrom_cons`
`mem_stepSet` 📖	mathematical	—	`Set` `Set.instMembership` `stepSet` `step`	—	—
`nil_mem_acceptsFrom` 📖	mathematical	—	`Language` `Language.instMembershipList` `acceptsFrom` `Set` `Set.instMembership` `accept`	—	—
`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`	—	`toDFA_correct` `DFA.pumping_lemma`
`reverse_accept` 📖	mathematical	—	`accept` `reverse` `start`	—	—
`reverse_reverse` 📖	mathematical	—	`reverse`	—	—
`reverse_start` 📖	mathematical	—	`start` `reverse` `accept`	—	—
`reverse_step` 📖	mathematical	—	`step` `reverse` `setOf` `Set` `Set.instMembership`	—	—
`stepSet_empty` 📖	mathematical	—	`stepSet` `Set` `Set.instEmptyCollection`	—	`Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty`
`stepSet_singleton` 📖	mathematical	—	`stepSet` `Set` `Set.instSingletonSet` `step`	—	`Set.iUnion_congr_Prop` `Set.iUnion_iUnion_eq_left`
`stepSet_union` 📖	mathematical	—	`stepSet` `Set` `Set.instUnion`	—	`Set.ext`
`toDFA_correct` 📖	mathematical	—	`DFA.accepts` `Set` `toDFA` `accepts`	—	`Language.ext` `mem_accepts` `DFA.mem_accepts`

NFA.Path

Definitions

Name	Category	Theorems
`supp` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`NFA` 📖	CompData	—

---

← Back to Index