Total

📁 Source: Cslib/Foundations/Semantics/LTS/Total.lean

Statistics

Metric	Count
Definitions Total, chooseFLTS, chooseOmegaExecution, totalize	4
Theorems chooseFLTS, extend_omegaExecution, omegaExecution_exists, total, instTotalSumUnitTotalize, no_sink_to_nonsink, nonsink_mtr_iff, nonsink_tr_iff	8
Total	12

Cslib.LTS

Definitions

Name	Category	Theorems
Total 📖	CompData	3 math math: Cslib.Automata.NA.FinAcc.instTotalSumUnitFinConcat, instTotalSumUnitTotalize, Cslib.Automata.NA.FinAcc.instTotalSumUnitFinLoopOfNonemptyElemStart
chooseFLTS 📖	CompOp	1 math math: Total.chooseFLTS
chooseOmegaExecution 📖	CompOp	—
totalize 📖	CompOp	4 math math: totalize.nonsink_mtr_iff, instTotalSumUnitTotalize, totalize.nonsink_tr_iff, totalize.no_sink_to_nonsink

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTotalSumUnitTotalize 📖	mathematical	—	Total totalize	—	—

Cslib.LTS.Total

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chooseFLTS 📖	mathematical	—	Cslib.LTS.Tr Cslib.FLTS.tr Cslib.LTS.chooseFLTS	—	total
extend_omegaExecution 📖	mathematical	Cslib.LTS.MTr	Cslib.ωSequence Cslib.LTS.OmegaExecution Cslib.ωSequence.appendωSequence Cslib.instFunLikeωSequenceNat	—	omegaExecution_exists
omegaExecution_exists 📖	mathematical	—	Cslib.ωSequence Cslib.LTS.OmegaExecution Cslib.instFunLikeωSequenceNat	—	—
total 📖	mathematical	—	Cslib.LTS.Tr	—	—

Cslib.LTS.totalize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
no_sink_to_nonsink 📖	mathematical	—	Cslib.LTS.MTr Cslib.LTS.totalize	—	—
nonsink_mtr_iff 📖	mathematical	—	Cslib.LTS.MTr Cslib.LTS.totalize	—	—
nonsink_tr_iff 📖	mathematical	—	Cslib.LTS.Tr Cslib.LTS.totalize	—	—

---

← Back to Index