Documentation Verification Report

OmegaRegularLanguage

📁 Source: Cslib/Computability/Languages/OmegaRegularLanguage.lean

Statistics

Metric	Count
Definitions `IsRegular`	1
Theorems `bot`, `eq_fin_iSup_hmul_omegaPow`, `fin_cover_saturates`, `fin_cover_saturates_compl`, `hmul`, `iInf`, `iSup`, `inf`, `not_da_buchi`, `of_da_buchi`, `omegaPow`, `regular_omegaLim`, `sup`, `top`, `isRegular_iff`	15
Total	16

Cslib.ωLanguage

Definitions

Name	Category	Theorems
`IsRegular` 📖	MathDef	8 math math: `IsRegular.regular_omegaLim`, `IsRegular.of_da_buchi`, `isRegular_iff`, `IsRegular.not_da_buchi`, `IsRegular.omegaPow`, `IsRegular.top`, `IsRegular.eq_fin_iSup_hmul_omegaPow`, `IsRegular.bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_iff` 📖	mathematical	—	`IsRegular` `Cslib.Automata.ωAcceptor.language` `Cslib.Automata.NA.Buchi` `Cslib.Automata.NA.Buchi.instωAcceptor`	—	—

Cslib.ωLanguage.IsRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra`	—	`Cslib.ωLanguage.ext`
`eq_fin_iSup_hmul_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra` `Cslib.ωLanguage.instHMulLanguage` `Cslib.ωLanguage.OmegaPow.omegaPow` `Cslib.ωLanguage.instOmegaPowLanguageOfInhabited`	—	`Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow` `Cslib.ωLanguage.ext` `iSup`
`fin_cover_saturates` 📖	—	`Set.Saturates` `Cslib.ωSequence` `Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra` `Cslib.ωLanguage.IsRegular`	—	—	`Set.saturates_eq_biUnion` `iSup`
`fin_cover_saturates_compl` 📖	—	`Set.Saturates` `Cslib.ωSequence` `Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra` `Cslib.ωLanguage.IsRegular`	—	—	`fin_cover_saturates` `Set.saturates_compl`
`hmul` 📖	mathematical	`Cslib.ωLanguage.IsRegular`	`Cslib.ωLanguage` `Cslib.ωLanguage.instHMulLanguage`	—	`Cslib.Language.IsRegular.iff_nfa` `Cslib.Automata.NA.Buchi.concat_language_eq`
`iInf` 📖	mathematical	`Cslib.ωLanguage.IsRegular`	`Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra`	—	—
`iSup` 📖	mathematical	`Cslib.ωLanguage.IsRegular`	`Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra`	—	—
`inf` 📖	mathematical	`Cslib.ωLanguage.IsRegular`	`Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra`	—	`Cslib.ωLanguage.ext` `Cslib.Automata.NA.Buchi.inter_language_eq`
`not_da_buchi` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.Automata.ωAcceptor.language` `Cslib.Automata.DA.Buchi` `Cslib.Automata.DA.Buchi.instωAcceptor`	—	`Cslib.ωLanguage.Example.eventually_zero_accepted_by_na_buchi` `Cslib.ωLanguage.Example.eventually_zero_not_omegaLim`
`of_da_buchi` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.Automata.ωAcceptor.language` `Cslib.Automata.DA.Buchi` `Cslib.Automata.DA.Buchi.instωAcceptor`	—	`Cslib.Automata.DA.Buchi.toNABuchi_language_eq`
`omegaPow` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.ωLanguage.OmegaPow.omegaPow` `Cslib.ωLanguage` `Cslib.ωLanguage.instOmegaPowLanguageOfInhabited`	—	`Cslib.Language.IsRegular.iff_nfa` `Cslib.Automata.NA.Buchi.loop_language_eq`
`regular_omegaLim` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.ωLanguage.OmegaLim.omegaLim` `Cslib.ωLanguage` `Cslib.ωLanguage.instOmegaLim`	—	`Cslib.Language.IsRegular.iff_dfa`
`sup` 📖	mathematical	`Cslib.ωLanguage.IsRegular`	`Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra`	—	`Cslib.ωLanguage.ext` `Cslib.Automata.NA.Buchi.iSum_language_eq`
`top` 📖	mathematical	—	`Cslib.ωLanguage.IsRegular` `Cslib.ωLanguage` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra`	—	`Cslib.ωLanguage.ext`

---

← Back to Index