OmegaAcceptor

📁 Source: Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean

Statistics

Metric	Count
Definitions ωAcceptor, Accepts, language	3
Theorems mem_language	1
Total	4

Cslib.Automata

Definitions

Name	Category	Theorems
ωAcceptor 📖	CompData	—

Cslib.Automata.ωAcceptor

Definitions

Name	Category	Theorems
Accepts 📖	MathDef	1 math math: mem_language
language 📖	CompOp	13 math math: Cslib.ωLanguage.IsRegular.of_da_buchi, Cslib.Automata.NA.Buchi.inter_language_eq, Cslib.ωLanguage.isRegular_iff, Cslib.ωLanguage.IsRegular.not_da_buchi, mem_language, Cslib.Automata.NA.Buchi.iSum_language_eq, Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow, Cslib.Automata.NA.Buchi.reindex_language_eq, Cslib.Automata.NA.Buchi.loop_language_eq, Cslib.ωLanguage.Example.eventually_zero_accepted_by_na_buchi, Cslib.Automata.DA.Buchi.toNABuchi_language_eq, Cslib.Automata.NA.Buchi.concat_language_eq, Cslib.Automata.DA.buchi_eq_finAcc_omegaLim

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_language 📖	mathematical	—	Cslib.ωSequence Cslib.ωLanguage Cslib.ωLanguage.instMembershipωSequence language Accepts	—	—

---

← Back to Index