Simulation

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

Statistics

Metric	Count
Definitions Similarity, Simulation, SimulationEquiv, instTransSimulationEquiv, «term_≤[_]_», «term_≤≥[_]_»	6
Theorems refl, trans, comp, eqv, refl, symm, trans	7
Total	13

Cslib

Definitions

Name	Category	Theorems
Similarity 📖	MathDef	1 math math: Similarity.refl
Simulation 📖	MathDef	3 math math: Bisimulation.is_simulation, Bisimulation.simulation_iff, Bisimilarity.symm_simulation
SimulationEquiv 📖	MathDef	2 math math: SimulationEquiv.eqv, SimulationEquiv.refl
instTransSimulationEquiv 📖	CompOp	—
«term_≤[_]_» 📖	CompOp	—
«term_≤≥[_]_» 📖	CompOp	—

Cslib.Similarity

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
refl 📖	mathematical	—	Cslib.Similarity	—	—
trans 📖	—	Cslib.Similarity	—	—	Cslib.Simulation.comp

Cslib.Simulation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	Cslib.Simulation	—	—	—

Cslib.SimulationEquiv

Theorems

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

---

← Back to Index