TraceEq

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

Statistics

Metric	Count
Definitions HomTraceEq, TraceEq, instTransTraceEq, traces, «term_~tr[_,_]_», «term_~tr[_]_»	6
Theorems eqv, refl, deterministic_isSimulation, symm, trans, traces_in	6
Total	12

Cslib.LTS

Definitions

Name	Category	Theorems
HomTraceEq 📖	MathDef	3 math math: IsBisimulation.traceEq_not_bisim, HomTraceEq.refl, HomTraceEq.eqv
TraceEq 📖	MathDef	7 math math: IsBisimulation.traceEq, TraceEq.deterministic_isSimulation, Bisimilarity.le_traceEq, IsBisimulation.deterministic_traceEq_isBisimulation, TraceEq.trans, TraceEq.symm, Bisimilarity.deterministic_bisim_eq_traceEq
instTransTraceEq 📖	CompOp	—
traces 📖	CompOp	1 math math: traces_in
«term_~tr[_,_]_» 📖	CompOp	—
«term_~tr[_]_» 📖	CompOp	—

Theorems

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

Cslib.LTS.HomTraceEq

Theorems

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

Cslib.LTS.TraceEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deterministic_isSimulation 📖	mathematical	—	Cslib.LTS.IsSimulation Cslib.LTS.TraceEq	—	Cslib.LTS.MTr.single Cslib.LTS.traces_in Cslib.LTS.MTr.single_invert Cslib.LTS.MTr.comp Cslib.LTS.Deterministic.deterministic
symm 📖	mathematical	Cslib.LTS.TraceEq	Cslib.LTS.TraceEq	—	—
trans 📖	mathematical	Cslib.LTS.TraceEq	Cslib.LTS.TraceEq	—	—

---

← Back to Index