DFA

📁 Source: Mathlib/Computability/DFA.lean

Statistics

Metric	Count
Definitions `DFA`, `accept`, `accepts`, `acceptsFrom`, `comap`, `eval`, `evalFrom`, `instCompl`, `instInhabited`, `inter`, `reindex`, `start`, `step`, `union`, `IsRegular`	15
Theorems `acceptsFrom_compl`, `acceptsFrom_inter`, `acceptsFrom_union`, `accepts_comap`, `accepts_compl`, `accepts_inter`, `accepts_reindex`, `accepts_union`, `comap_accept`, `comap_id`, `comap_reindex`, `comap_start`, `comap_step`, `compl_def`, `evalFrom_append_singleton`, `evalFrom_comap`, `evalFrom_cons`, `evalFrom_nil`, `evalFrom_of_append`, `evalFrom_of_pow`, `evalFrom_reindex`, `evalFrom_singleton`, `evalFrom_split`, `eval_append_singleton`, `eval_comap`, `eval_nil`, `eval_reindex`, `eval_singleton`, `inter_accept`, `inter_start`, `inter_step`, `mem_accepts`, `mem_acceptsFrom`, `pumping_lemma`, `reindex_apply_accept`, `reindex_apply_start`, `reindex_apply_step`, `reindex_refl`, `symm_reindex`, `union_accept`, `union_start`, `union_step`, `add`, `compl`, `inf`, `of_compl`, `IsRegular_compl`, `isRegular_iff`	48
Total	63

DFA

Definitions

Name	Category	Theorems
`accept` 📖	CompOp	9 math math: `reindex_apply_accept`, `mem_acceptsFrom`, `union_accept`, `inter_accept`, `toNFA_accept`, `compl_def`, `comap_accept`, `Language.mem_accept_toDFA`, `mem_accepts`
`accepts` 📖	CompOp	12 math math: `accepts_union`, `toNFA_correct`, `accepts_comap`, `NFA.toDFA_correct`, `Language.leftQuotient_accepts`, `accepts_compl`, `accepts_reindex`, `accepts_inter`, `Language.isRegular_iff`, `Language.leftQuotient_accepts_apply`, `Language.accepts_toDFA`, `mem_accepts`
`acceptsFrom` 📖	CompOp	6 math math: `mem_acceptsFrom`, `acceptsFrom_union`, `Language.leftQuotient_accepts`, `acceptsFrom_inter`, `acceptsFrom_compl`, `Language.leftQuotient_accepts_apply`
`comap` 📖	CompOp	8 math math: `comap_reindex`, `evalFrom_comap`, `comap_start`, `comap_id`, `accepts_comap`, `comap_accept`, `eval_comap`, `comap_step`
`eval` 📖	CompOp	8 math math: `eval_append_singleton`, `eval_nil`, `Language.leftQuotient_accepts`, `eval_comap`, `eval_reindex`, `Language.leftQuotient_accepts_apply`, `eval_singleton`, `mem_accepts`
`evalFrom` 📖	CompOp	9 math math: `evalFrom_comap`, `evalFrom_of_append`, `mem_acceptsFrom`, `evalFrom_append_singleton`, `toNFA_evalFrom_match`, `evalFrom_cons`, `evalFrom_singleton`, `evalFrom_nil`, `evalFrom_reindex`
`instCompl` 📖	CompOp	3 math math: `compl_def`, `accepts_compl`, `acceptsFrom_compl`
`instInhabited` 📖	CompOp	—
`inter` 📖	CompOp	5 math math: `inter_start`, `inter_accept`, `acceptsFrom_inter`, `accepts_inter`, `inter_step`
`reindex` 📖	CompOp	9 math math: `reindex_apply_accept`, `comap_reindex`, `reindex_refl`, `symm_reindex`, `reindex_apply_start`, `accepts_reindex`, `eval_reindex`, `reindex_apply_step`, `evalFrom_reindex`
`start` 📖	CompOp	9 math math: `inter_start`, `comap_start`, `Language.start_toDFA`, `toNFA_start`, `reindex_apply_start`, `eval_nil`, `compl_def`, `union_start`, `eval_singleton`
`step` 📖	CompOp	12 math math: `union_step`, `toNFA_step`, `evalFrom_append_singleton`, `eval_append_singleton`, `evalFrom_cons`, `evalFrom_singleton`, `compl_def`, `Language.step_toDFA`, `comap_step`, `reindex_apply_step`, `eval_singleton`, `inter_step`
`union` 📖	CompOp	5 math math: `accepts_union`, `union_step`, `union_accept`, `acceptsFrom_union`, `union_start`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acceptsFrom_compl` 📖	mathematical	—	`acceptsFrom` `Compl.compl` `DFA` `instCompl` `Language` `BooleanAlgebra.toCompl` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	—
`acceptsFrom_inter` 📖	mathematical	—	`acceptsFrom` `inter` `Language` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	`Language.ext` `Set.mem_setOf`
`acceptsFrom_union` 📖	mathematical	—	`acceptsFrom` `union` `Language` `Language.instAdd`	—	`Language.ext` `Language.add_def` `Set.mem_union` `Set.mem_setOf`
`accepts_comap` 📖	mathematical	—	`accepts` `comap` `Set.preimage`	—	`Language.ext` `Set.mem_preimage` `mem_accepts` `eval_comap`
`accepts_compl` 📖	mathematical	—	`accepts` `Compl.compl` `DFA` `instCompl` `Language` `BooleanAlgebra.toCompl` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	—
`accepts_inter` 📖	mathematical	—	`accepts` `inter` `Language` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	`acceptsFrom_inter`
`accepts_reindex` 📖	mathematical	—	`accepts` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	`Language.ext` `eval_reindex` `Equiv.symm_apply_apply`
`accepts_union` 📖	mathematical	—	`accepts` `union` `Language` `Language.instAdd`	—	`acceptsFrom_union` `add_eq_sup`
`comap_accept` 📖	mathematical	—	`accept` `comap`	—	—
`comap_id` 📖	mathematical	—	`comap`	—	—
`comap_reindex` 📖	mathematical	—	`comap` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	—
`comap_start` 📖	mathematical	—	`start` `comap`	—	—
`comap_step` 📖	mathematical	—	`step` `comap`	—	—
`compl_def` 📖	mathematical	—	`Compl.compl` `DFA` `instCompl` `step` `start` `Set` `Set.instCompl` `accept`	—	—
`evalFrom_append_singleton` 📖	mathematical	—	`evalFrom` `step`	—	—
`evalFrom_comap` 📖	mathematical	—	`evalFrom` `comap`	—	`evalFrom_append_singleton`
`evalFrom_cons` 📖	mathematical	—	`evalFrom` `step`	—	—
`evalFrom_nil` 📖	mathematical	—	`evalFrom`	—	—
`evalFrom_of_append` 📖	mathematical	—	`evalFrom`	—	—
`evalFrom_of_pow` 📖	—	`evalFrom` `Language` `Language.instMembershipList` `KStar.kstar` `Language.instKStar` `Language.instSingletonList`	—	—	`Language.mem_kstar` `evalFrom_of_append` `Set.mem_singleton_iff`
`evalFrom_reindex` 📖	mathematical	—	`evalFrom` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.symm`	—	`Equiv.apply_symm_apply` `evalFrom_append_singleton` `Equiv.symm_apply_apply`
`evalFrom_singleton` 📖	mathematical	—	`evalFrom` `step`	—	—
`evalFrom_split` 📖	—	`Fintype.card` `evalFrom`	—	—	`Fintype.exists_ne_map_eq_of_card_lt` `Fintype.card_fin` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `min_eq_left` `evalFrom_of_append` `le_of_not_ge`
`eval_append_singleton` 📖	mathematical	—	`eval` `step`	—	`evalFrom_append_singleton`
`eval_comap` 📖	mathematical	—	`eval` `comap`	—	`evalFrom_comap`
`eval_nil` 📖	mathematical	—	`eval` `start`	—	—
`eval_reindex` 📖	mathematical	—	`eval` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	`evalFrom_reindex` `Equiv.symm_apply_apply`
`eval_singleton` 📖	mathematical	—	`eval` `step` `start`	—	—
`inter_accept` 📖	mathematical	—	`accept` `inter` `setOf` `Set` `Set.instMembership`	—	—
`inter_start` 📖	mathematical	—	`start` `inter`	—	—
`inter_step` 📖	mathematical	—	`step` `inter`	—	—
`mem_accepts` 📖	mathematical	—	`Language` `Language.instMembershipList` `accepts` `Set` `Set.instMembership` `accept` `eval`	—	—
`mem_acceptsFrom` 📖	mathematical	—	`Language` `Language.instMembershipList` `acceptsFrom` `Set` `Set.instMembership` `accept` `evalFrom`	—	—
`pumping_lemma` 📖	mathematical	`Language` `Language.instMembershipList` `accepts` `Fintype.card`	`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`	—	`evalFrom_split` `Language.mem_mul` `evalFrom_of_pow` `mem_accepts` `eval.eq_1` `evalFrom_of_append` `Set.mem_singleton_iff`
`reindex_apply_accept` 📖	mathematical	—	`accept` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Set.preimage` `Equiv.symm`	—	—
`reindex_apply_start` 📖	mathematical	—	`start` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	—
`reindex_apply_step` 📖	mathematical	—	`step` `DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.symm`	—	—
`reindex_refl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DFA` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.refl`	—	—
`symm_reindex` 📖	mathematical	—	`Equiv.symm` `DFA` `reindex`	—	—
`union_accept` 📖	mathematical	—	`accept` `union` `setOf` `Set` `Set.instMembership`	—	—
`union_start` 📖	mathematical	—	`start` `union`	—	—
`union_step` 📖	mathematical	—	`step` `union`	—	—

Language

Definitions

Name	Category	Theorems
`IsRegular` 📖	MathDef	5 math math: `IsRegular_compl`, `IsRegular.of_finite_range_leftQuotient`, `isRegular_iff_finite_range_leftQuotient`, `isRegular_reverse_iff`, `isRegular_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsRegular_compl` 📖	mathematical	—	`IsRegular` `Compl.compl` `Language` `BooleanAlgebra.toCompl` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`IsRegular.of_compl` `IsRegular.compl`
`isRegular_iff` 📖	mathematical	—	`IsRegular` `DFA.accepts`	—	—

Language.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Language.IsRegular`	`Language` `Language.instAdd`	—	`DFA.accepts_union` `add_eq_sup`
`compl` 📖	mathematical	`Language.IsRegular`	`Compl.compl` `Language` `BooleanAlgebra.toCompl` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	—
`inf` 📖	mathematical	`Language.IsRegular`	`Language` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	`DFA.accepts_inter`
`of_compl` 📖	—	`Language.IsRegular` `Compl.compl` `Language` `BooleanAlgebra.toCompl` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Language.instCompleteAtomicBooleanAlgebra`	—	—	`compl` `Language.compl_compl`

(root)

Definitions

Name	Category	Theorems
`DFA` 📖	CompData	12 math math: `DFA.reindex_apply_accept`, `DFA.comap_reindex`, `DFA.reindex_refl`, `DFA.symm_reindex`, `DFA.reindex_apply_start`, `DFA.compl_def`, `DFA.accepts_compl`, `DFA.acceptsFrom_compl`, `DFA.accepts_reindex`, `DFA.eval_reindex`, `DFA.reindex_apply_step`, `DFA.evalFrom_reindex`

---

← Back to Index