Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `NA`, `accept`, `instωAcceptor`, `toNA`, `FinAcc`, `accept`, `instAcceptor`, `toNA`, `Muller`, `accept`, `instωAcceptor`, `toNA`, `Run`, `start`, `toLTS`	15
Theorems `start`, `trans`	2
Total	17

Cslib.Automata

Definitions

Name	Category	Theorems
`NA` 📖	CompData	—

Cslib.Automata.NA

Definitions

Name	Category	Theorems
`FinAcc` 📖	CompData	14 math math: `FinAcc.totalize_language_eq`, `loop_run_one_iter`, `concat_run_left_right`, `FinAcc.finConcat_language_eq`, `concat_start_right`, `loop_run_left_left`, `Cslib.Automata.DA.FinAcc.toNAFinAcc_language_eq`, `Cslib.Automata.εNA.FinAcc.toNAFinAcc_language_eq`, `FinAcc.toDAFinAcc_language_eq`, `Buchi.loop_language_eq`, `Cslib.Language.IsRegular.iff_nfa`, `loop_run_left_right_left`, `Buchi.concat_language_eq`, `concat_run_proj`
`Muller` 📖	CompData	—
`Run` 📖	CompData	7 math math: `Buchi.reindex_run_iff'`, `totalize_mtr_run`, `iProd_run_iff`, `iSum_run_iff`, `Cslib.Automata.DA.toNA_run`, `loop_run_exists`, `Buchi.reindex_run_iff`
`start` 📖	CompOp	5 math math: `loop_run_left_right`, `concat_run_left`, `totalize_run_mtr`, `Buchi.language_eq_fin_iSup_hmul_omegaPow`, `Run.start`
`toLTS` 📖	CompOp	9 math math: `FinAcc.instTotalSumUnitFinConcat`, `Run.trans`, `loop_run_left_right`, `loop_fin_run_mtr`, `concat_run_left`, `totalize_run_mtr`, `Buchi.language_eq_fin_iSup_hmul_omegaPow`, `loop_fin_run_exists`, `FinAcc.instTotalSumUnitFinLoopOfNonemptyElemStart`

Cslib.Automata.NA.Buchi

Definitions

Name	Category	Theorems
`accept` 📖	CompOp	1 math math: `language_eq_fin_iSup_hmul_omegaPow`
`instωAcceptor` 📖	CompOp	9 math math: `inter_language_eq`, `Cslib.ωLanguage.isRegular_iff`, `iSum_language_eq`, `language_eq_fin_iSup_hmul_omegaPow`, `reindex_language_eq`, `loop_language_eq`, `Cslib.ωLanguage.Example.eventually_zero_accepted_by_na_buchi`, `Cslib.Automata.DA.Buchi.toNABuchi_language_eq`, `concat_language_eq`
`toNA` 📖	CompOp	3 math math: `reindex_run_iff'`, `language_eq_fin_iSup_hmul_omegaPow`, `reindex_run_iff`

Cslib.Automata.NA.FinAcc

Definitions

Name	Category	Theorems
`accept` 📖	CompOp	2 math math: `totalize_language_eq`, `finConcat_language_eq`
`instAcceptor` 📖	CompOp	14 math math: `totalize_language_eq`, `Cslib.Automata.NA.loop_run_one_iter`, `Cslib.Automata.NA.concat_run_left_right`, `finConcat_language_eq`, `Cslib.Automata.NA.concat_start_right`, `Cslib.Automata.NA.loop_run_left_left`, `Cslib.Automata.DA.FinAcc.toNAFinAcc_language_eq`, `Cslib.Automata.εNA.FinAcc.toNAFinAcc_language_eq`, `toDAFinAcc_language_eq`, `Cslib.Automata.NA.Buchi.loop_language_eq`, `Cslib.Language.IsRegular.iff_nfa`, `Cslib.Automata.NA.loop_run_left_right_left`, `Cslib.Automata.NA.Buchi.concat_language_eq`, `Cslib.Automata.NA.concat_run_proj`
`toNA` 📖	CompOp	3 math math: `totalize_language_eq`, `Cslib.Automata.NA.loop_run_left_right`, `Cslib.Automata.NA.concat_run_left`

Cslib.Automata.NA.Muller

Definitions

Name	Category	Theorems
`accept` 📖	CompOp	—
`instωAcceptor` 📖	CompOp	—
`toNA` 📖	CompOp	—

Cslib.Automata.NA.Run

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`start` 📖	mathematical	`Cslib.Automata.NA.Run`	`Cslib.Automata.NA.start` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	—
`trans` 📖	mathematical	`Cslib.Automata.NA.Run`	`Cslib.LTS.ωTr` `Cslib.Automata.NA.toLTS`	—	—

---

← Back to Index