OmegaExecution

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

Statistics

Metric	Count
Definitions OmegaExecution	1
Theorems append, cons, extract_execution, extract_mTr, flatten_execution, flatten_mTr	6
Total	7

Cslib.LTS

Definitions

Name	Category	Theorems
OmegaExecution 📖	MathDef	7 math math: Cslib.Automata.NA.Run.trans, Total.omegaExecution_exists, OmegaExecution.append, OmegaExecution.flatten_execution, OmegaExecution.flatten_mTr, OmegaExecution.cons, Total.extend_omegaExecution

Cslib.LTS.OmegaExecution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append 📖	mathematical	Cslib.LTS.MTr Cslib.LTS.OmegaExecution Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence Cslib.LTS.OmegaExecution Cslib.ωSequence.appendωSequence Cslib.instFunLikeωSequenceNat Cslib.ωSequence.drop	—	Cslib.LTS.Execution.of_mTr
cons 📖	mathematical	Cslib.LTS.Tr Cslib.LTS.OmegaExecution Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.OmegaExecution Cslib.ωSequence.cons	—	—
extract_execution 📖	mathematical	Cslib.LTS.OmegaExecution	Cslib.LTS.Execution Cslib.ωSequence Cslib.instFunLikeωSequenceNat Cslib.ωSequence.extract	—	—
extract_mTr 📖	mathematical	Cslib.LTS.OmegaExecution	Cslib.LTS.MTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat Cslib.ωSequence.extract	—	—
flatten_execution 📖	mathematical	Cslib.LTS.Execution Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence Cslib.LTS.OmegaExecution Cslib.ωSequence.flatten Cslib.ωSequence.extract Cslib.ωSequence.cumLen Cslib.instFunLikeωSequenceNat	—	Cslib.ωSequence.cumLen_strictMono Cslib.ωSequence.cumLen_zero Nat.segment_lower_bound Nat.segment_range_val Nat.segment_idem Cslib.ωSequence.extract_flatten
flatten_mTr 📖	mathematical	Cslib.LTS.MTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence Cslib.LTS.OmegaExecution Cslib.ωSequence.flatten Cslib.instFunLikeωSequenceNat Cslib.ωSequence.cumLen	—	flatten_execution Cslib.LTS.Execution.of_mTr

---

← Back to Index