Execution

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

Statistics

Metric	Count
Definitions Execution	1
Theorems comp, cons_invert, nonEmpty_states, of_mTr, refl, split, stepL, to_mTr, split, mTr_iff_execution	10
Total	11

Cslib.LTS

Definitions

Name	Category	Theorems
Execution 📖	MathDef	9 math math: Execution.comp, Execution.stepL, OmegaExecution.extract_execution, mTr_iff_execution, Execution.split, Execution.refl, Cslib.Automata.NA.Buchi.buchiCongruence_transfer, Execution.of_mTr, Execution.cons_invert

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mTr_iff_execution 📖	mathematical	—	MTr Execution	—	—

Cslib.LTS.Execution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Cslib.LTS.Execution	Cslib.LTS.Execution	—	—
cons_invert 📖	mathematical	Cslib.LTS.Execution	Cslib.LTS.Execution	—	—
nonEmpty_states 📖	—	Cslib.LTS.Execution	—	—	—
of_mTr 📖	mathematical	Cslib.LTS.MTr	Cslib.LTS.Execution	—	—
refl 📖	mathematical	—	Cslib.LTS.Execution	—	—
split 📖	mathematical	Cslib.LTS.Execution	Cslib.LTS.Execution	—	—
stepL 📖	mathematical	Cslib.LTS.Tr Cslib.LTS.Execution	Cslib.LTS.Execution	—	—
to_mTr 📖	mathematical	Cslib.LTS.Execution	Cslib.LTS.MTr	—	cons_invert

Cslib.LTS.MTr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
split 📖	mathematical	Cslib.LTS.MTr	Cslib.LTS.MTr	—	Cslib.LTS.Execution.of_mTr Cslib.LTS.Execution.split

---

← Back to Index