ToNA

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

Statistics

Metric	Count
Definitions toNABuchi, toNAFinAcc, instCoeNA, toNA	4
Theorems toNABuchi_language_eq, toNAFinAcc_language_eq, toNA_run	3
Total	7

Cslib.Automata.DA

Definitions

Name	Category	Theorems
instCoeNA 📖	CompOp	—
toNA 📖	CompOp	1 math math: toNA_run

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNA_run 📖	mathematical	—	Cslib.Automata.NA.Run toNA run	—	Cslib.ωSequence.ext

Cslib.Automata.DA.Buchi

Definitions

Name	Category	Theorems
toNABuchi 📖	CompOp	1 math math: toNABuchi_language_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNABuchi_language_eq 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Cslib.Automata.NA.Buchi Cslib.Automata.NA.Buchi.instωAcceptor toNABuchi Cslib.Automata.DA.Buchi instωAcceptor	—	Cslib.ωLanguage.ext

Cslib.Automata.DA.FinAcc

Definitions

Name	Category	Theorems
toNAFinAcc 📖	CompOp	1 math math: toNAFinAcc_language_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNAFinAcc_language_eq 📖	mathematical	—	Cslib.Automata.Acceptor.language Cslib.Automata.NA.FinAcc Cslib.Automata.NA.FinAcc.instAcceptor toNAFinAcc Cslib.Automata.DA.FinAcc instAcceptor	—	—

---

← Back to Index