Simulation

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

Statistics

Metric	Count
Definitions HomSimilarity, HomSimulationEquiv, IsHomSimulation, IsSimulation, Similarity, SimulationEquiv, instTransSimulationEquiv, «term_≤[_,_]_», «term_≤[_]_», «term_≤≥[_,_]_», «term_≤≥[_]_»	11
Theorems refl, eqv, refl, comp, trans, symm, trans	7
Total	18

Cslib.LTS

Definitions

Name	Category	Theorems
HomSimilarity 📖	MathDef	1 math math: HomSimilarity.refl
HomSimulationEquiv 📖	MathDef	2 math math: HomSimulationEquiv.eqv, HomSimulationEquiv.refl
IsHomSimulation 📖	MathDef	1 math math: HomBisimilarity.symm_simulation
IsSimulation 📖	MathDef	4 math math: IsBisimulation.isSimulation_iff, IsSimulation.comp, IsBisimulation.isSimulation, TraceEq.deterministic_isSimulation
Similarity 📖	MathDef	1 math math: Similarity.trans
SimulationEquiv 📖	MathDef	2 math math: SimulationEquiv.trans, SimulationEquiv.symm
instTransSimulationEquiv 📖	CompOp	—
«term_≤[_,_]_» 📖	CompOp	—
«term_≤[_]_» 📖	CompOp	—
«term_≤≥[_,_]_» 📖	CompOp	—
«term_≤≥[_]_» 📖	CompOp	—

Cslib.LTS.HomSimilarity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	mathematical	—	Cslib.LTS.HomSimilarity	—	—

Cslib.LTS.HomSimulationEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqv 📖	mathematical	—	Cslib.LTS.HomSimulationEquiv	—	refl Cslib.LTS.SimulationEquiv.symm Cslib.LTS.SimulationEquiv.trans
refl 📖	mathematical	—	Cslib.LTS.HomSimulationEquiv	—	—

Cslib.LTS.IsSimulation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Cslib.LTS.IsSimulation	Cslib.LTS.IsSimulation	—	—

Cslib.LTS.Similarity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trans 📖	mathematical	Cslib.LTS.Similarity	Cslib.LTS.Similarity	—	Cslib.LTS.IsSimulation.comp

Cslib.LTS.SimulationEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symm 📖	mathematical	Cslib.LTS.SimulationEquiv	Cslib.LTS.SimulationEquiv	—	—
trans 📖	mathematical	Cslib.LTS.SimulationEquiv	Cslib.LTS.SimulationEquiv	—	—

---

← Back to Index