Basic

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

Statistics

Metric	Count
Definitions DA, accept, instωAcceptor, toDA, FinAcc, accept, instAcceptor, toDA, Muller, accept, instωAcceptor, toDA, run, run', start, toFLTS	16
Theorems mtr_extract_eq_run, run_succ, run_zero	3
Total	19

Cslib.Automata

Definitions

Name	Category	Theorems
DA 📖	CompData	—

Cslib.Automata.DA

Definitions

Name	Category	Theorems
FinAcc 📖	CompData	5 math math: Cslib.Language.IsRegular.iff_dfa, FinAcc.congr_language_eq, FinAcc.toNAFinAcc_language_eq, Cslib.Automata.NA.FinAcc.toDAFinAcc_language_eq, buchi_eq_finAcc_omegaLim
Muller 📖	CompData	—
run 📖	CompOp	4 math math: run_succ, run_zero, toNA_run, mtr_extract_eq_run
run' 📖	CompOp	—
start 📖	CompOp	3 math math: run_zero, congr_mtr_eq, mtr_extract_eq_run
toFLTS 📖	CompOp	4 math math: prod_mtr_eq, run_succ, congr_mtr_eq, mtr_extract_eq_run

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mtr_extract_eq_run 📖	mathematical	—	Cslib.FLTS.mtr toFLTS start Cslib.ωSequence.extract Cslib.ωSequence Cslib.instFunLikeωSequenceNat run	—	—
run_succ 📖	mathematical	—	Cslib.ωSequence Cslib.instFunLikeωSequenceNat run Cslib.FLTS.tr toFLTS	—	—
run_zero 📖	mathematical	—	Cslib.ωSequence Cslib.instFunLikeωSequenceNat run start	—	—

Cslib.Automata.DA.Buchi

Definitions

Name	Category	Theorems
accept 📖	CompOp	—
instωAcceptor 📖	CompOp	4 math math: Cslib.ωLanguage.IsRegular.of_da_buchi, Cslib.ωLanguage.IsRegular.not_da_buchi, toNABuchi_language_eq, Cslib.Automata.DA.buchi_eq_finAcc_omegaLim
toDA 📖	CompOp	—

Cslib.Automata.DA.FinAcc

Definitions

Name	Category	Theorems
accept 📖	CompOp	—
instAcceptor 📖	CompOp	5 math math: Cslib.Language.IsRegular.iff_dfa, congr_language_eq, toNAFinAcc_language_eq, Cslib.Automata.NA.FinAcc.toDAFinAcc_language_eq, Cslib.Automata.DA.buchi_eq_finAcc_omegaLim
toDA 📖	CompOp	—

Cslib.Automata.DA.Muller

Definitions

Name	Category	Theorems
accept 📖	CompOp	—
instωAcceptor 📖	CompOp	—
toDA 📖	CompOp	—

---

← Back to Index