Documentation Verification Report

BuchiCongruence

📁 Source: Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

Statistics

Metric	Count
Definitions `BuchiCongrParam`, `BuchiCongruence`, `buchiFamily`	3
Theorems `buchiCongrParam_surjective`, `buchiCongruence_fin_index`, `buchiCongruence_transfer`, `buchiFamily_cover`, `buchiFamily_saturation`, `mem_buchiFamily`	6
Total	9

Cslib.Automata.NA.Buchi

Definitions

Name	Category	Theorems
`BuchiCongrParam` 📖	CompOp	1 math math: `buchiCongrParam_surjective`
`BuchiCongruence` 📖	CompOp	5 math math: `buchiFamily_saturation`, `buchiCongruence_fin_index`, `buchiFamily_cover`, `buchiCongrParam_surjective`, `mem_buchiFamily`
`buchiFamily` 📖	CompOp	3 math math: `buchiFamily_saturation`, `buchiFamily_cover`, `mem_buchiFamily`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`buchiCongrParam_surjective` 📖	mathematical	—	`Cslib.RightCongruence.eq` `BuchiCongruence` `BuchiCongrParam`	—	—
`buchiCongruence_fin_index` 📖	mathematical	—	`Cslib.RightCongruence.eq` `BuchiCongruence`	—	`buchiCongrParam_surjective`
`buchiCongruence_transfer` 📖	mathematical	`Cslib.RightCongruence.eqvCls` `BuchiCongruence` `Cslib.LTS.pairLang` `Cslib.Automata.NA.toLTS` `toNA`	`Cslib.LTS.Execution` `Cslib.Automata.NA.toLTS` `toNA` `accept`	—	`Cslib.LTS.Execution.of_mTr`
`buchiFamily_cover` 📖	mathematical	—	`Cslib.ωLanguage` `Cslib.RightCongruence.eq` `BuchiCongruence` `Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra` `buchiFamily`	—	`Cslib.ωLanguage.ext` `buchiCongruence_fin_index` `Cslib.infinite_graph_ramsey` `Cslib.ωSequence.strictMono_of_infinite` `mem_buchiFamily`
`buchiFamily_saturation` 📖	mathematical	—	`Set.Saturates` `Cslib.RightCongruence.eq` `BuchiCongruence` `Cslib.ωSequence` `buchiFamily` `Cslib.Automata.ωAcceptor.language` `Cslib.Automata.NA.Buchi` `instωAcceptor`	—	`mem_buchiFamily` `buchiCongruence_transfer` `Cslib.LTS.OmegaExecution.flatten_execution` `Cslib.ωSequence.cumLen_strictMono` `Cslib.LTS.OmegaExecution.append` `Cslib.ωSequence.drop_frequently_iff_frequently`
`mem_buchiFamily` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `Cslib.ωLanguage.instMembershipωSequence` `buchiFamily` `Cslib.RightCongruence.eq` `BuchiCongruence` `Cslib.RightCongruence.eqvCls` `Cslib.instFunLikeωSequenceNat` `Cslib.ωSequence.appendωSequence` `Cslib.ωSequence.flatten`	—	—

---

← Back to Index