Total

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

Statistics

Metric	Count
Definitions totalize, Total	2
Theorems totalize_language_eq, totalize_mtr_run, totalize_run_mtr	3
Total	5

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	Run totalize Cslib.ωSequence.appendωSequence Cslib.ωSequence Cslib.instFunLikeωSequenceNat	—	—
totalize_run_mtr 📖	mathematical	Run totalize Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.MTr toLTS Cslib.ωSequence.take start	—	Run.start Cslib.LTS.totalize.mtr_left_iff Cslib.ωSequence.extract_eq_take Cslib.LTS.ωTr_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	—	—

Cslib.LTS

Definitions

Name	Category	Theorems
Total 📖	CompData	3 math math: Cslib.Automata.NA.FinAcc.instTotalSumUnitFinConcat, Cslib.instTotalSumUnitTotalize, Cslib.Automata.NA.FinAcc.instTotalSumUnitFinLoopOfNonemptyElemStart

---

← Back to Index