HasTau

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

Statistics

Metric	Count
Definitions HasTau, τ, STr, saturate, τClosure, τSTr	6
Theorems comp, single, trans_τ, mem_saturate_image_τ, sTr_τSTr, saturate_tr_sTr, saturate_tr_saturate_sTr, saturate_τSTr_τSTr	8
Total	14

Cslib

Definitions

Name	Category	Theorems
HasTau 📖	CompData	—

Cslib.HasTau

Definitions

Name	Category	Theorems
τ 📖	CompOp	3 math math: Cslib.LTS.sTr_τSTr, Cslib.LTS.mem_saturate_image_τ, Cslib.LTS.STr.trans_τ

Cslib.LTS

Definitions

Name	Category	Theorems
STr 📖	CompData	6 math math: sTr_τSTr, STr.single, STr.trans_τ, saturate_tr_sTr, STr.comp, saturate_tr_saturate_sTr
saturate 📖	CompOp	5 math math: noε_saturate_mTr, mem_saturate_image_τ, saturate_τSTr_τSTr, saturate_tr_sTr, saturate_tr_saturate_sTr
τClosure 📖	CompOp	—
τSTr 📖	MathDef	4 math math: sTr_τSTr, saturate_τSTr_τSTr, IsSWBisimulation.follow_internal_snd, IsSWBisimulation.follow_internal_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_saturate_image_τ 📖	mathematical	—	image saturate Cslib.HasTau.τ	—	—
sTr_τSTr 📖	mathematical	—	STr Cslib.HasTau.τ τSTr	—	—
saturate_tr_sTr 📖	mathematical	—	Tr saturate STr	—	—
saturate_tr_saturate_sTr 📖	mathematical	Cslib.HasTau.τ	Tr saturate STr	—	STr.single STr.comp sTr_τSTr saturate_τSTr_τSTr
saturate_τSTr_τSTr 📖	mathematical	—	τSTr saturate	—	sTr_τSTr

Cslib.LTS.STr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	Cslib.LTS.STr Cslib.HasTau.τ	Cslib.LTS.STr	—	Cslib.LTS.sTr_τSTr
single 📖	mathematical	Cslib.LTS.Tr	Cslib.LTS.STr	—	—
trans_τ 📖	mathematical	Cslib.LTS.STr Cslib.HasTau.τ	Cslib.LTS.STr Cslib.HasTau.τ	—	Cslib.LTS.sTr_τSTr

---

← Back to Index