Basic

📁 Source: Cslib/Languages/CCS/Basic.lean

Statistics

Metric	Count
Definitions Act, Co, IsVisible, instDecidableCoOfDecidableEq, isCo, fill, Process, instDecidableEqAct, decEq, instDecidableEqContext, decEq, instDecidableEqProcess, decEq, instHasContextProcess	14
Theorems symm, co_isVisible, isCo_iff, isVisible_neq_τ, complete, isContext_def	6
Total	20

Cslib.CCS

Definitions

Name	Category	Theorems
Act 📖	CompData	9 math math: bisimilarity_par_assoc, bisimilarity_nil_par, bisimilarity_choice_comm, bisimilarity_par_comm, bisimilarity_choice_idem, bisimilarity_par_nil, bisimilarityCongruence, bisimilarity_choice_assoc, bisimilarity_choice_nil
Process 📖	CompData	11 math math: bisimilarity_par_assoc, bisimilarity_nil_par, bisimilarity_choice_comm, bisimilarity_par_comm, bisimilarity_choice_idem, Context.complete, isContext_def, bisimilarity_par_nil, bisimilarityCongruence, bisimilarity_choice_assoc, bisimilarity_choice_nil
instDecidableEqAct 📖	CompOp	—
instDecidableEqContext 📖	CompOp	—
instDecidableEqProcess 📖	CompOp	—
instHasContextProcess 📖	CompOp	3 math math: Context.complete, isContext_def, bisimilarityCongruence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isContext_def 📖	mathematical	—	Cslib.HasContext.fill Process instHasContextProcess Context.fill	—	—

Cslib.CCS.Act

Definitions

Name	Category	Theorems
Co 📖	CompData	1 bridge bridge: isCo_iff
IsVisible 📖	CompData	1 math math: co_isVisible
instDecidableCoOfDecidableEq 📖	CompOp	—
isCo 📖	CompOp	1 bridge bridge: isCo_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
co_isVisible 📖	mathematical	Co	IsVisible	—	—
isCo_iff 📖	bridging (iff)	—	isCo Co	isCo	—
isVisible_neq_τ 📖	—	IsVisible	—	—	—

Cslib.CCS.Act.Co

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symm 📖	—	Cslib.CCS.Act.Co	—	—	—

Cslib.CCS.Context

Definitions

Name	Category	Theorems
fill 📖	CompOp	2 math math: Cslib.CCS.isContext_def, Cslib.CCS.bisimilarity_is_congruence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete 📖	mathematical	—	Cslib.HasContext.fill Cslib.CCS.Process Cslib.CCS.instHasContextProcess Cslib.CCS.Process.nil Cslib.CCS.Process.const	—	—

Cslib.CCS.instDecidableEqAct

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

Cslib.CCS.instDecidableEqContext

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

Cslib.CCS.instDecidableEqProcess

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index