Documentation Verification Report

MyhillNerode

📁 Source: Mathlib/Computability/MyhillNerode.lean

Statistics

Metric	Count
Definitions `leftQuotient`, `toDFA`	2
Theorems `finite_range_leftQuotient`, `of_finite_range_leftQuotient`, `accepts_toDFA`, `isRegular_iff_finite_range_leftQuotient`, `leftQuotient_accepts`, `leftQuotient_accepts_apply`, `leftQuotient_append`, `leftQuotient_nil`, `mem_accept_toDFA`, `mem_leftQuotient`, `start_toDFA`, `step_toDFA`	12
Total	14

Language

Definitions

Name	Category	Theorems
`leftQuotient` 📖	CompOp	11 math math: `leftQuotient_append`, `start_toDFA`, `leftQuotient_nil`, `isRegular_iff_finite_range_leftQuotient`, `leftQuotient_accepts`, `mem_leftQuotient`, `mem_accept_toDFA`, `step_toDFA`, `IsRegular.finite_range_leftQuotient`, `leftQuotient_accepts_apply`, `accepts_toDFA`
`toDFA` 📖	CompOp	4 math math: `start_toDFA`, `mem_accept_toDFA`, `step_toDFA`, `accepts_toDFA`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accepts_toDFA` 📖	mathematical	—	`DFA.accepts` `Set.Elem` `Language` `Set.range` `leftQuotient` `toDFA`	—	`ext` `DFA.mem_accepts` `DFA.eval_append_singleton` `leftQuotient_append`
`isRegular_iff_finite_range_leftQuotient` 📖	mathematical	—	`IsRegular` `Set.Finite` `Language` `Set.range` `leftQuotient`	—	`IsRegular.finite_range_leftQuotient` `IsRegular.of_finite_range_leftQuotient`
`leftQuotient_accepts` 📖	mathematical	—	`leftQuotient` `DFA.accepts` `Language` `DFA.acceptsFrom` `DFA.eval`	—	`leftQuotient_accepts_apply`
`leftQuotient_accepts_apply` 📖	mathematical	—	`leftQuotient` `DFA.accepts` `DFA.acceptsFrom` `DFA.eval`	—	`ext` `DFA.evalFrom_of_append`
`leftQuotient_append` 📖	mathematical	—	`leftQuotient`	—	—
`leftQuotient_nil` 📖	mathematical	—	`leftQuotient`	—	—
`mem_accept_toDFA` 📖	mathematical	—	`Set.Elem` `Language` `Set.range` `leftQuotient` `Set` `Set.instMembership` `DFA.accept` `toDFA` `instMembershipList`	—	—
`mem_leftQuotient` 📖	mathematical	—	`Language` `instMembershipList` `leftQuotient`	—	—
`start_toDFA` 📖	mathematical	—	`Language` `Set` `Set.instMembership` `Set.range` `leftQuotient` `DFA.start` `Set.Elem` `toDFA`	—	—
`step_toDFA` 📖	mathematical	—	`Language` `Set` `Set.instMembership` `Set.range` `leftQuotient` `DFA.step` `Set.Elem` `toDFA`	—	—

Language.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_range_leftQuotient` 📖	mathematical	`Language.IsRegular`	`Set.Finite` `Language` `Set.range` `Language.leftQuotient`	—	`Language.leftQuotient_accepts` `Set.finite_of_finite_preimage` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `Set.range_comp_subset_range`
`of_finite_range_leftQuotient` 📖	mathematical	—	`Language.IsRegular`	—	`Language.isRegular_iff` `Language.accepts_toDFA`

---

← Back to Index