Buchi

📁 Source: Cslib/Computability/Automata/DA/Buchi.lean

Statistics

Metric	Count
Definitions Buchi, Buchi	2
Theorems buchi_eq_finAcc_omegaLim	1
Total	3

Cslib.Automata.DA

Definitions

Name	Category	Theorems
Buchi 📖	CompData	4 math math: Cslib.ωLanguage.IsRegular.of_da_buchi, Cslib.ωLanguage.IsRegular.not_da_buchi, Buchi.toNABuchi_language_eq, buchi_eq_finAcc_omegaLim

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
buchi_eq_finAcc_omegaLim 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Buchi Buchi.instωAcceptor Cslib.ωLanguage.OmegaLim.omegaLim Cslib.ωLanguage Cslib.ωLanguage.instOmegaLim Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor	—	Cslib.ωLanguage.ext mtr_extract_eq_run

Cslib.Automata.NA

Definitions

Name	Category	Theorems
Buchi 📖	CompData	11 math math: Buchi.reindex_run_iff', Buchi.inter_language_eq, Cslib.ωLanguage.isRegular_iff, Buchi.iSum_language_eq, Buchi.language_eq_fin_iSup_hmul_omegaPow, Buchi.reindex_language_eq, Buchi.loop_language_eq, Cslib.ωLanguage.Example.eventually_zero_accepted_by_na_buchi, Buchi.reindex_run_iff, Cslib.Automata.DA.Buchi.toNABuchi_language_eq, Buchi.concat_language_eq

---

← Back to Index