BehaviouralTheory

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

Statistics

Metric	Count
Definitions	0
Theorems bisimilarityCongruence, bisimilarity_choice_assoc, bisimilarity_choice_comm, bisimilarity_choice_idem, bisimilarity_choice_nil, bisimilarity_congr_choice, bisimilarity_congr_par, bisimilarity_congr_pre, bisimilarity_congr_res, bisimilarity_is_congruence, bisimilarity_nil_par, bisimilarity_par_assoc, bisimilarity_par_comm, bisimilarity_par_nil	14
Total	14

Cslib.CCS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bisimilarityCongruence 📖	mathematical	—	Cslib.Congruence Process instHasContextProcess Cslib.Bisimilarity Act lts	—	Cslib.instIsEquivBisimilarity
bisimilarity_choice_assoc 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.choice	—	—
bisimilarity_choice_comm 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.choice	—	—
bisimilarity_choice_idem 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.choice	—	—
bisimilarity_choice_nil 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.choice Process.nil	—	—
bisimilarity_congr_choice 📖	mathematical	Cslib.Bisimilarity Process Act lts	Process.choice	—	Cslib.LTS.IsBisimulation.follow_fst Cslib.Bisimilarity.largest_bisimulation Cslib.Bisimilarity.refl Cslib.LTS.IsBisimulation.follow_snd
bisimilarity_congr_par 📖	mathematical	Cslib.Bisimilarity Process Act lts	Process.par	—	Cslib.LTS.IsBisimulation.follow_fst Cslib.LTS.IsBisimulation.follow_snd
bisimilarity_congr_pre 📖	mathematical	Cslib.Bisimilarity Process Act lts	Process.pre	—	—
bisimilarity_congr_res 📖	mathematical	Cslib.Bisimilarity Process Act lts	Process.res	—	Cslib.LTS.IsBisimulation.follow_fst Cslib.Bisimilarity.is_bisimulation Cslib.LTS.IsBisimulation.follow_snd
bisimilarity_is_congruence 📖	mathematical	Cslib.Bisimilarity Process Act lts	Context.fill	—	—
bisimilarity_nil_par 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.par Process.nil	—	—
bisimilarity_par_assoc 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.par	—	—
bisimilarity_par_comm 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.par	—	—
bisimilarity_par_nil 📖	mathematical	—	Cslib.Bisimilarity Process Act lts Process.par Process.nil	—	—

---

← Back to Index