TraceEq

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

Statistics

Metric	Count
Definitions traces, TraceEq, instTransTraceEq, «term_~tr[_]_»	4
Theorems traces_in, deterministic_sim, eqv, refl, symm, trans	6
Total	10

Cslib

Definitions

Name	Category	Theorems
TraceEq 📖	MathDef	7 math math: LTS.IsBisimulation.traceEq, Bisimulation.traceEq_not_bisim, Bisimilarity.deterministic_bisim_eq_traceEq, Bisimilarity.le_traceEq, Bisimulation.deterministic_traceEq_is_bisim, TraceEq.refl, TraceEq.eqv
instTransTraceEq 📖	CompOp	—
«term_~tr[_]_» 📖	CompOp	—

Cslib.LTS

Definitions

Name	Category	Theorems
traces 📖	CompOp	1 math math: traces_in

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
traces_in 📖	mathematical	MTr	traces	—	—

Cslib.TraceEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deterministic_sim 📖	—	Cslib.TraceEq Cslib.LTS.Tr	—	—	Cslib.LTS.MTr.single Cslib.LTS.traces_in Cslib.LTS.MTr.single_invert Cslib.LTS.MTr.comp Cslib.LTS.Deterministic.deterministic
eqv 📖	mathematical	—	Cslib.TraceEq	—	refl symm trans
refl 📖	mathematical	—	Cslib.TraceEq	—	—
symm 📖	—	Cslib.TraceEq	—	—	—
trans 📖	—	Cslib.TraceEq	—	—	—

---

← Back to Index