Language

📁 Source: Mathlib/Computability/Language.lean

Statistics

Metric	Count
Definitions `Language`, `Language`, `instAdd`, `instCompleteAtomicBooleanAlgebra`, `instInhabited`, `instInsertList`, `instKStar`, `instKleeneAlgebra`, `instMembershipList`, `instMul`, `instOne`, `instSemiring`, `instSingletonList`, `instSub`, `instZero`, `map`, `reverse`, `reverseIso`, `Symbol`, `instDecidableEqSymbol`, `decEq`, `instFintypeSymbol`, `instReprSymbol`, `repr`	24
Theorems `add_def`, `add_iSup`, `add_self`, `append_mem_mul`, `compl_compl`, `ext`, `ext_iff`, `iSup_add`, `iSup_mul`, `iSup_sub`, `instMulLeftMono`, `instMulRightMono`, `instOrderedSub`, `join_mem_kstar`, `kstar_def`, `kstar_def_nonempty`, `kstar_eq_iSup_pow`, `le_add_congr`, `le_iff`, `le_mul_congr`, `map_id`, `map_kstar`, `map_map`, `mem_add`, `mem_iSup`, `mem_inf`, `mem_kstar`, `mem_kstar_iff_exists_nonempty`, `mem_mul`, `mem_one`, `mem_pow`, `mem_reverse`, `mem_sub`, `mul_def`, `mul_iSup`, `mul_self_kstar_comm`, `nil_mem_kstar`, `nil_mem_one`, `notMem_zero`, `one_add_kstar_mul_self_eq_kstar`, `one_add_self_mul_kstar_eq_kstar`, `one_def`, `reverseIso_apply`, `reverseIso_symm_apply`, `reverse_add`, `reverse_bijective`, `reverse_eq_image`, `reverse_iInf`, `reverse_iSup`, `reverse_injective`, `reverse_involutive`, `reverse_kstar`, `reverse_mem_reverse`, `reverse_mul`, `reverse_one`, `reverse_pow`, `reverse_reverse`, `reverse_surjective`, `reverse_zero`, `self_eq_mul_add_iff`, `sub_def`, `sub_iSup`, `zero_def`	63
Total	87

FirstOrder

Definitions

Name	Category	Theorems
`Language` 📖	CompData	—

Language

Definitions

Name	Category	Theorems
`instAdd` 📖	CompOp	19 math math: `DFA.accepts_union`, `reverse_add`, `reverseIso_apply`, `iSup_add`, `self_eq_mul_add_iff`, `NFA.acceptsFrom_union`, `one_add_kstar_mul_self_eq_kstar`, `one_add_self_mul_kstar_eq_kstar`, `le_iff`, `RegularExpression.matches'_add`, `add_iSup`, `DFA.acceptsFrom_union`, `add_self`, `instOrderedSub`, `IsRegular.add`, `reverseIso_symm_apply`, `mem_add`, `add_def`, `le_add_congr`
`instCompleteAtomicBooleanAlgebra` 📖	CompOp	26 math math: `iSup_add`, `reverse_iInf`, `iSup_sub`, `NFA.pumping_lemma`, `instMulRightMono`, `mem_iSup`, `reverse_iSup`, `εNFA.pumping_lemma`, `instMulLeftMono`, `sub_iSup`, `le_iff`, `IsRegular_compl`, `add_iSup`, `instOrderedSub`, `DFA.accepts_compl`, `IsRegular.inf`, `iSup_mul`, `DFA.acceptsFrom_inter`, `DFA.pumping_lemma`, `IsRegular.compl`, `mem_inf`, `DFA.acceptsFrom_compl`, `compl_compl`, `mul_iSup`, `DFA.accepts_inter`, `kstar_eq_iSup_pow`
`instInhabited` 📖	CompOp	—
`instInsertList` 📖	CompOp	—
`instKStar` 📖	CompOp	17 math math: `map_kstar`, `join_mem_kstar`, `NFA.pumping_lemma`, `self_eq_mul_add_iff`, `one_add_kstar_mul_self_eq_kstar`, `εNFA.pumping_lemma`, `one_add_self_mul_kstar_eq_kstar`, `mem_kstar_iff_exists_nonempty`, `kstar_def`, `RegularExpression.matches'_star`, `kstar_def_nonempty`, `DFA.pumping_lemma`, `nil_mem_kstar`, `mul_self_kstar_comm`, `reverse_kstar`, `kstar_eq_iSup_pow`, `mem_kstar`
`instKleeneAlgebra` 📖	CompOp	—
`instMembershipList` 📖	CompOp	28 math, 1 bridge math: `ext_iff`, `mem_iSup`, `mem_reverse`, `DFA.mem_acceptsFrom`, `mem_one`, `NFA.accepts_iff_exists_path`, `mem_kstar_iff_exists_nonempty`, `NFA.cons_mem_acceptsFrom`, `notMem_zero`, `NFA.nil_mem_acceptsFrom`, `εNFA.mem_accepts_iff_exists_path`, `ContextFreeGrammar.mem_language_iff`, `mem_sub`, `mem_pow`, `nil_mem_one`, `mem_mul`, `NFA.mem_acceptsFrom`, `mem_leftQuotient`, `NFA.mem_accepts_reverse`, `mem_inf`, `NFA.mem_accepts`, `mem_accept_toDFA`, `NFA.append_mem_acceptsFrom`, `nil_mem_kstar`, `mem_add`, `reverse_mem_reverse`, `DFA.mem_accepts`, `mem_kstar` bridge: `RegularExpression.rmatch_iff_matches'`
`instMul` 📖	CompOp	19 math math: `reverseIso_apply`, `RegularExpression.matches'_mul`, `NFA.pumping_lemma`, `self_eq_mul_add_iff`, `instMulRightMono`, `one_add_kstar_mul_self_eq_kstar`, `εNFA.pumping_lemma`, `instMulLeftMono`, `one_add_self_mul_kstar_eq_kstar`, `mul_def`, `append_mem_mul`, `reverse_mul`, `iSup_mul`, `mem_mul`, `DFA.pumping_lemma`, `mul_iSup`, `reverseIso_symm_apply`, `mul_self_kstar_comm`, `le_mul_congr`
`instOne` 📖	CompOp	7 math math: `one_add_kstar_mul_self_eq_kstar`, `one_add_self_mul_kstar_eq_kstar`, `mem_one`, `one_def`, `nil_mem_one`, `reverse_one`, `RegularExpression.matches'_epsilon`
`instSemiring` 📖	CompOp	8 math math: `map_kstar`, `reverse_pow`, `mem_pow`, `map_map`, `RegularExpression.matches'_pow`, `RegularExpression.matches'_map`, `map_id`, `kstar_eq_iSup_pow`
`instSingletonList` 📖	CompOp	4 math math: `NFA.pumping_lemma`, `εNFA.pumping_lemma`, `DFA.pumping_lemma`, `RegularExpression.matches'_char`
`instSub` 📖	CompOp	5 math math: `iSup_sub`, `sub_def`, `sub_iSup`, `instOrderedSub`, `mem_sub`
`instZero` 📖	CompOp	5 math math: `reverse_zero`, `notMem_zero`, `zero_def`, `ContextFreeGrammar.language_eq_zero_of_forall_input_ne_initial`, `RegularExpression.matches'_zero`
`map` 📖	CompOp	4 math math: `map_kstar`, `map_map`, `RegularExpression.matches'_map`, `map_id`
`reverse` 📖	CompOp	22 math math: `reverse_add`, `reverseIso_apply`, `reverse_iInf`, `reverse_iSup`, `mem_reverse`, `reverse_zero`, `reverse_pow`, `ContextFreeGrammar.language_reverse`, `IsRegular.reverse`, `reverse_mul`, `reverse_injective`, `reverse_bijective`, `reverse_surjective`, `isRegular_reverse_iff`, `reverse_one`, `reverse_eq_image`, `reverse_involutive`, `reverseIso_symm_apply`, `reverse_kstar`, `reverse_mem_reverse`, `reverse_reverse`, `IsContextFree.reverse`
`reverseIso` 📖	CompOp	2 math math: `reverseIso_apply`, `reverseIso_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_def` 📖	mathematical	—	`Language` `instAdd` `Set` `Set.instUnion`	—	—
`add_iSup` 📖	mathematical	—	`Language` `instAdd` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`sup_iSup`
`add_self` 📖	mathematical	—	`Language` `instAdd`	—	`sup_idem`
`append_mem_mul` 📖	mathematical	`Language` `instMembershipList`	`instMul`	—	`Set.mem_image2_of_mem`
`compl_compl` 📖	mathematical	—	`Compl.compl` `Language` `BooleanAlgebra.toCompl` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	—
`ext` 📖	—	`Language` `instMembershipList`	—	—	`Set.ext`
`ext_iff` 📖	mathematical	—	`Language` `instMembershipList`	—	`ext`
`iSup_add` 📖	mathematical	—	`Language` `instAdd` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`iSup_sup`
`iSup_mul` 📖	mathematical	—	`Language` `instMul` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.image2_iUnion_left`
`iSup_sub` 📖	mathematical	—	`Language` `instSub` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.iUnion_diff`
`instMulLeftMono` 📖	mathematical	—	`MulLeftMono` `Language` `instMul` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.image2_subset_left`
`instMulRightMono` 📖	mathematical	—	`MulRightMono` `Language` `instMul` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.image2_subset_right`
`instOrderedSub` 📖	mathematical	—	`OrderedSub` `Language` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `instAdd` `instSub`	—	`sdiff_le_iff'`
`join_mem_kstar` 📖	mathematical	`Language` `instMembershipList`	`KStar.kstar` `instKStar`	—	—
`kstar_def` 📖	mathematical	—	`KStar.kstar` `Language` `instKStar` `setOf`	—	—
`kstar_def_nonempty` 📖	mathematical	—	`KStar.kstar` `Language` `instKStar` `setOf`	—	`ext` `mem_kstar_iff_exists_nonempty`
`kstar_eq_iSup_pow` 📖	mathematical	—	`KStar.kstar` `Language` `instKStar` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`ext`
`le_add_congr` 📖	mathematical	`Language` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`instAdd`	—	`add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IdemSemiring.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`le_iff` 📖	mathematical	—	`Language` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `instAdd`	—	`sup_eq_right`
`le_mul_congr` 📖	mathematical	`Language` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`instMul`	—	`mul_le_mul'` `instMulLeftMono` `instMulRightMono`
`map_id` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Language` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map`	—	`Set.image_id_eq`
`map_kstar` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Language` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map` `KStar.kstar` `instKStar`	—	`kstar_eq_iSup_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Set.image_iUnion`
`map_map` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Language` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `map`	—	`Set.image_image` `Set.image_congr`
`mem_add` 📖	mathematical	—	`Language` `instMembershipList` `instAdd`	—	—
`mem_iSup` 📖	mathematical	—	`Language` `instMembershipList` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.mem_iUnion`
`mem_inf` 📖	mathematical	—	`Language` `instMembershipList` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.mem_inter_iff`
`mem_kstar` 📖	mathematical	—	`Language` `instMembershipList` `KStar.kstar` `instKStar`	—	—
`mem_kstar_iff_exists_nonempty` 📖	mathematical	—	`Language` `instMembershipList` `KStar.kstar` `instKStar`	—	—
`mem_mul` 📖	mathematical	—	`Language` `instMembershipList` `instMul`	—	`Set.mem_image2`
`mem_one` 📖	mathematical	—	`Language` `instMembershipList` `instOne`	—	—
`mem_pow` 📖	mathematical	—	`Language` `instMembershipList` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`pow_zero` `instIsEmptyFalse` `pow_succ'`
`mem_reverse` 📖	mathematical	—	`Language` `instMembershipList` `reverse`	—	—
`mem_sub` 📖	mathematical	—	`Language` `instMembershipList` `instSub`	—	—
`mul_def` 📖	mathematical	—	`Language` `instMul` `Set.image2`	—	—
`mul_iSup` 📖	mathematical	—	`Language` `instMul` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.image2_iUnion_right`
`mul_self_kstar_comm` 📖	mathematical	—	`Language` `instMul` `KStar.kstar` `instKStar`	—	`kstar_eq_iSup_pow` `iSup_mul` `mul_iSup`
`nil_mem_kstar` 📖	mathematical	—	`Language` `instMembershipList` `KStar.kstar` `instKStar`	—	—
`nil_mem_one` 📖	mathematical	—	`Language` `instMembershipList` `instOne`	—	`Set.mem_singleton`
`notMem_zero` 📖	mathematical	—	`Language` `instMembershipList` `instZero`	—	—
`one_add_kstar_mul_self_eq_kstar` 📖	mathematical	—	`Language` `instAdd` `instOne` `instMul` `KStar.kstar` `instKStar`	—	`mul_self_kstar_comm` `one_add_self_mul_kstar_eq_kstar`
`one_add_self_mul_kstar_eq_kstar` 📖	mathematical	—	`Language` `instAdd` `instOne` `instMul` `KStar.kstar` `instKStar`	—	`pow_zero` `kstar_eq_iSup_pow` `mul_iSup` `sup_iSup_nat_succ`
`one_def` 📖	mathematical	—	`Language` `instOne` `Set` `Set.instSingletonSet`	—	—
`reverseIso_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Language` `MulOpposite` `instMul` `MulOpposite.instMul` `instAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `reverseIso` `MulOpposite.op` `reverse`	—	—
`reverseIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Language` `MulOpposite.instMul` `instMul` `MulOpposite.instAdd` `instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `reverseIso` `reverse` `MulOpposite.unop`	—	—
`reverse_add` 📖	mathematical	—	`reverse` `Language` `instAdd`	—	—
`reverse_bijective` 📖	mathematical	—	`Function.Bijective` `Language` `reverse`	—	`Function.Involutive.bijective` `reverse_involutive`
`reverse_eq_image` 📖	mathematical	—	`reverse` `Set.image`	—	`List.reverse_involutive` `Equiv.image_eq_preimage_symm`
`reverse_iInf` 📖	mathematical	—	`reverse` `iInf` `Language` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.preimage_iInter`
`reverse_iSup` 📖	mathematical	—	`reverse` `iSup` `Language` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`Set.preimage_iUnion`
`reverse_injective` 📖	mathematical	—	`Language` `reverse`	—	`Function.Involutive.injective` `reverse_involutive`
`reverse_involutive` 📖	mathematical	—	`Function.Involutive` `Language` `reverse`	—	`Function.Involutive.preimage` `List.reverse_involutive`
`reverse_kstar` 📖	mathematical	—	`reverse` `KStar.kstar` `Language` `instKStar`	—	`kstar_eq_iSup_pow` `reverse_iSup` `reverse_pow`
`reverse_mem_reverse` 📖	mathematical	—	`Language` `instMembershipList` `reverse`	—	`mem_reverse`
`reverse_mul` 📖	mathematical	—	`reverse` `Language` `instMul`	—	`reverse_eq_image` `Set.image_image2` `Set.image2_congr` `Set.image2_image_right` `Set.image2_image_left` `Set.image2_swap`
`reverse_one` 📖	mathematical	—	`reverse` `Language` `instOne`	—	—
`reverse_pow` 📖	mathematical	—	`reverse` `Language` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`MulOpposite.op_injective` `map_pow` `MulEquivClass.instMonoidHomClass` `RingEquivClass.toMulEquivClass` `RingEquiv.instRingEquivClass`
`reverse_reverse` 📖	mathematical	—	`reverse`	—	`reverse_involutive`
`reverse_surjective` 📖	mathematical	—	`Language` `reverse`	—	`Function.Involutive.surjective` `reverse_involutive`
`reverse_zero` 📖	mathematical	—	`reverse` `Language` `instZero`	—	—
`self_eq_mul_add_iff` 📖	mathematical	`Language` `instMembershipList`	`instAdd` `instMul` `KStar.kstar` `instKStar`	—	`le_antisymm` `Nat.strong_induction_on` `mem_mul` `one_add_self_mul_kstar_eq_kstar` `one_add_mul` `Distrib.rightDistribClass` `mul_assoc` `nil_mem_kstar` `kstar_eq_iSup_pow` `iSup_mul` `iSup_le_iff` `pow_zero` `one_mul` `add_comm` `le_self_add` `IdemSemiring.toCanonicallyOrderedAdd` `pow_add` `pow_one` `le_imp_le_of_le_of_le` `mul_le_mul_right` `instMulLeftMono` `le_refl`
`sub_def` 📖	mathematical	—	`Language` `instSub` `Set` `Set.instSDiff`	—	—
`sub_iSup` 📖	mathematical	—	`Language` `instSub` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`Set.diff_iUnion`
`zero_def` 📖	mathematical	—	`Language` `instZero` `Set` `Set.instEmptyCollection`	—	—

(root)

Definitions

Name	Category	Theorems
`Language` 📖	CompOp	94 math, 1 bridge math: `DFA.accepts_union`, `Language.map_kstar`, `Language.reverse_add`, `Language.ext_iff`, `Language.reverseIso_apply`, `Language.iSup_add`, `Language.reverse_iInf`, `Language.iSup_sub`, `Language.sub_def`, `RegularExpression.matches'_mul`, `Language.instMulRightMono`, `NFA.acceptsFrom_union`, `Language.mem_iSup`, `Language.start_toDFA`, `Language.reverse_iSup`, `Language.mem_reverse`, `Language.one_add_kstar_mul_self_eq_kstar`, `DFA.mem_acceptsFrom`, `Language.reverse_zero`, `Language.reverse_pow`, `Language.instMulLeftMono`, `Language.one_add_self_mul_kstar_eq_kstar`, `Language.sub_iSup`, `Language.le_iff`, `Language.mem_one`, `Language.IsRegular_compl`, `RegularExpression.matches'_add`, `Language.add_iSup`, `DFA.acceptsFrom_union`, `NFA.accepts_iff_exists_path`, `Language.mem_kstar_iff_exists_nonempty`, `Language.kstar_def`, `NFA.cons_mem_acceptsFrom`, `Language.notMem_zero`, `Language.add_self`, `Language.isRegular_iff_finite_range_leftQuotient`, `Language.mul_def`, `NFA.nil_mem_acceptsFrom`, `εNFA.mem_accepts_iff_exists_path`, `RegularExpression.matches'_star`, `Language.zero_def`, `ContextFreeGrammar.mem_language_iff`, `Language.instOrderedSub`, `Language.mem_sub`, `Language.reverse_mul`, `Language.mem_pow`, `Language.leftQuotient_accepts`, `DFA.accepts_compl`, `Language.map_map`, `Language.IsRegular.inf`, `Language.one_def`, `Language.reverse_injective`, `Language.reverse_bijective`, `Language.iSup_mul`, `Language.nil_mem_one`, `ContextFreeGrammar.language_eq_zero_of_forall_input_ne_initial`, `Language.reverse_surjective`, `DFA.acceptsFrom_inter`, `Language.kstar_def_nonempty`, `Language.mem_mul`, `NFA.mem_acceptsFrom`, `Language.mem_leftQuotient`, `NFA.mem_accepts_reverse`, `Language.reverse_one`, `Language.IsRegular.compl`, `Language.mem_inf`, `DFA.acceptsFrom_compl`, `NFA.mem_accepts`, `Language.compl_compl`, `Language.mem_accept_toDFA`, `Language.IsRegular.add`, `RegularExpression.matches'_pow`, `NFA.append_mem_acceptsFrom`, `Language.step_toDFA`, `Language.mul_iSup`, `Language.IsRegular.finite_range_leftQuotient`, `Language.nil_mem_kstar`, `Language.reverse_involutive`, `RegularExpression.matches'_zero`, `RegularExpression.matches'_map`, `RegularExpression.matches'_epsilon`, `Language.reverseIso_symm_apply`, `DFA.accepts_inter`, `Language.mul_self_kstar_comm`, `Language.map_id`, `Language.reverse_kstar`, `Language.kstar_eq_iSup_pow`, `Language.accepts_toDFA`, `Language.mem_add`, `Language.reverse_mem_reverse`, `DFA.mem_accepts`, `RegularExpression.matches'_char`, `Language.mem_kstar`, `Language.add_def` bridge: `RegularExpression.rmatch_iff_matches'`
`Symbol` 📖	CompData	26 math math: `ContextFreeGrammar.Derives.append_right`, `ContextFreeGrammar.Produces.append_left`, `ContextFreeGrammar.produces_reverse_comm`, `ContextFreeGrammar.Derives.reverse`, `ContextFreeGrammar.generates_reverse_comm`, `ContextFreeGrammar.produces_reverse`, `ContextFreeRule.rewrites_of_exists_parts`, `ContextFreeGrammar.Produces.exists_nonterminal_input_mem`, `ContextFreeGrammar.mem_language_iff`, `ContextFreeRule.Rewrites.exists_parts`, `ContextFreeGrammar.Derives.append_left`, `ContextFreeGrammar.derives_reverse_comm`, `ContextFreeRule.rewrites_reverse_comm`, `ContextFreeRule.rewrites_iff`, `ContextFreeGrammar.generates_reverse`, `ContextFreeRule.rewrites_reverse`, `ContextFreeRule.Rewrites.reverse`, `ContextFreeGrammar.Produces.append_right`, `ContextFreeGrammar.Generates.reverse`, `ContextFreeGrammar.derives_reverse`, `ContextFreeRule.Rewrites.input_output`, `ContextFreeRule.Rewrites.append_right`, `ContextFreeRule.Rewrites.append_left`, `ContextFreeGrammar.derives_nonterminal`, `ContextFreeGrammar.Produces.reverse`, `ContextFreeRule.Rewrites.nonterminal_input_mem`
`instDecidableEqSymbol` 📖	CompOp	—
`instFintypeSymbol` 📖	CompOp	—
`instReprSymbol` 📖	CompOp	—

instDecidableEqSymbol

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

instReprSymbol

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index