ToNA

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

Statistics

Metric	Count
Definitions toNAFinAcc, noε	2
Theorems toNAFinAcc_language_eq, noε_saturate_mTr	2
Total	4

Cslib.Automata.εNA.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.εNA.FinAcc instAcceptor	—	Cslib.LTS.noε_saturate_mTr

Cslib.LTS

Definitions

Name	Category	Theorems
noε 📖	CompOp	1 math math: noε_saturate_mTr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noε_saturate_mTr 📖	mathematical	—	MTr saturate Cslib.Automata.instHasTauOption noε	—	—

---

← Back to Index