ExampleEventuallyZero

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

Statistics

Metric	Count
Definitions eventually_zero, eventually_zero_na	2
Theorems eventually_zero_accepted_by_na_buchi, eventually_zero_not_omegaLim	2
Total	4

Cslib.ωLanguage.Example

Definitions

Name	Category	Theorems
eventually_zero 📖	CompOp	2 math math: eventually_zero_not_omegaLim, eventually_zero_accepted_by_na_buchi
eventually_zero_na 📖	CompOp	1 math math: eventually_zero_accepted_by_na_buchi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_zero_accepted_by_na_buchi 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Cslib.Automata.NA.Buchi Cslib.Automata.NA.Buchi.instωAcceptor eventually_zero_na eventually_zero	—	Cslib.ωLanguage.ext Cslib.Automata.NA.Run.trans
eventually_zero_not_omegaLim 📖	mathematical	—	Cslib.ωLanguage.OmegaLim.omegaLim Cslib.ωLanguage Cslib.ωLanguage.instOmegaLim eventually_zero	—	Cslib.ωLanguage.mem_omegaLim Cslib.ωSequence.frequently_iff_strictMono Cslib.ωSequence.cumLen_strictMono Cslib.ωSequence.extract_eq_ofFn

---

← Back to Index