Total

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

Statistics

Metric	Count
Definitions totalize	1
Theorems totalize_language_eq, totalize_mtr_run, totalize_run_mtr	3
Total	4

Cslib.Automata.NA

Definitions

Name	Category	Theorems
totalize 📖	CompOp	2 math math: FinAcc.totalize_language_eq, totalize_mtr_run

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totalize_mtr_run 📖	mathematical	start Cslib.LTS.MTr toLTS	Cslib.ωSequence Run totalize Cslib.ωSequence.appendωSequence Cslib.instFunLikeωSequenceNat	—	—
totalize_run_mtr 📖	mathematical	Run totalize Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.MTr toLTS Cslib.ωSequence.take start Cslib.ωSequence Cslib.instFunLikeωSequenceNat	—	Run.start Cslib.LTS.totalize.nonsink_mtr_iff Cslib.ωSequence.extract_eq_take Cslib.LTS.OmegaExecution.extract_mTr Run.trans

Cslib.Automata.NA.FinAcc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totalize_language_eq 📖	mathematical	—	Cslib.Automata.Acceptor.language Cslib.Automata.NA.FinAcc instAcceptor Cslib.Automata.NA.totalize toNA accept	—	—

---

← Back to Index