BuchiInter

📁 Source: Cslib/Computability/Automata/NA/BuchiInter.lean

Statistics

Metric	Count
Definitions histStart, histTrans, interAcc, interAccept, interNA	5
Theorems inter_freq_acc_freq_acc, inter_freq_comp_acc_freq_acc, inter_language_eq	3
Total	8

Cslib.Automata.NA.Buchi

Definitions

Name	Category	Theorems
histStart 📖	CompOp	—
histTrans 📖	CompOp	—
interAcc 📖	CompOp	—
interAccept 📖	CompOp	2 math math: inter_language_eq, inter_freq_comp_acc_freq_acc
interNA 📖	CompOp	1 math math: inter_language_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_freq_acc_freq_acc 📖	—	Cslib.Automata.NA.Run interNA interAcc Cslib.ωSequence Cslib.instFunLikeωSequenceNat	—	—	Cslib.Automata.NA.Run.trans Cslib.ωSequence.frequently_leadsTo_frequently Cslib.ωSequence.leadsTo_trans Cslib.ωSequence.step_leadsTo Cslib.ωSequence.until_frequently_not_leadsTo
inter_freq_comp_acc_freq_acc 📖	mathematical	Cslib.Automata.NA.Run interNA Cslib.ωSequence Cslib.instFunLikeωSequenceNat	interAccept	—	Cslib.Automata.NA.Run.trans Cslib.ωSequence.frequently_leadsTo_frequently Cslib.ωSequence.leadsTo_cases_or
inter_language_eq 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Cslib.Automata.NA.Buchi instωAcceptor interNA interAccept Cslib.ωSequence	—	Cslib.ωLanguage.ext Cslib.Automata.NA.iProd_run_iff Cslib.Automata.NA.hist_run_proj inter_freq_acc_freq_acc Cslib.Automata.NA.hist_run_exists inter_freq_comp_acc_freq_acc

---

← Back to Index