Documentation Verification Report

Bisimulation

πŸ“ Source: Cslib/Foundations/Semantics/LTS/Bisimulation.lean

Statistics

MetricCount
DefinitionsBisimilarity, HomBisimilarity, HomWeakBisimilarity, IsBisimulation, IsBisimulationUpTo, IsHomBisimulation, IsHomWeakBisimulation, IsSWBisimulation, IsWeakBisimulation, UpToHomBisimilarity, WeakBisimilarity, instBotSubtypeForallForallPropIsBisimulation, instBoundedOrderSubtypeForallForallPropIsBisimulation, instMaxSubtypeForallForallPropIsBisimulation, instSemilatticeSupSubtypeForallForallPropIsBisimulation, instTopSubtypeForallForallPropIsBisimulation, instTransBisimilarity, Β«term_~[_,_]_Β», Β«term_~[_]_Β», Β«term_β‰ˆ[_,_]_Β», Β«term_β‰ˆ[_]_Β»
21
Theoremsbisimilarity_neq_traceEq, deterministic_bisim_eq_traceEq, deterministic_traceEq_bisim, gfp, is_bisimulation, largest_bisimulation, le_traceEq, symm, trans, eqv, refl, symm_simulation, eqv, refl, bisim_trace, bot, comp, deterministic_traceEq_isBisimulation, follow_fst, follow_snd, inv, isSimulation, isSimulation_iff, sup, traceEq, traceEq_not_bisim, is_bisimulation, comp, follow_internal_fst, follow_internal_snd, isWeakBisimulation, comp, inv, isSwBisimulation, symm, trans, weakBisim_eq_swBisim, instIsEquivHomBisimilarity, isWeakBisimulation_iff_isSWBisimulation
39
Total60

Cslib.LTS

Definitions

NameCategoryTheorems
Bisimilarity πŸ“–MathDef
8 mathmath: Bisimilarity.deterministic_traceEq_bisim, Bisimilarity.gfp, Bisimilarity.largest_bisimulation, Bisimilarity.symm, Bisimilarity.le_traceEq, Bisimilarity.is_bisimulation, Bisimilarity.deterministic_bisim_eq_traceEq, Bisimilarity.trans
HomBisimilarity πŸ“–MathDef
19 mathmath: HomBisimilarity.symm_simulation, Cslib.CCS.bisimilarity_par_assoc, Cslib.CCS.bisimilarity_congr_pre, instIsEquivHomBisimilarity, Cslib.CCS.bisimilarity_nil_par, Cslib.CCS.bisimilarity_congr_par, HomBisimilarity.eqv, Cslib.CCS.bisimilarity_congr_choice, Cslib.CCS.bisimilarity_choice_comm, Cslib.CCS.bisimilarity_par_comm, Cslib.CCS.bisimilarity_choice_idem, Cslib.CCS.bisimilarity_par_nil, Cslib.CCS.bisimilarity_congr_res, Cslib.CCS.bisimilarityCongruence, Cslib.Logic.HML.theoryEq_eq_bisimilarity, Cslib.CCS.bisimilarity_choice_assoc, Cslib.CCS.bisimilarity_is_congruence, Cslib.CCS.bisimilarity_choice_nil, HomBisimilarity.refl
HomWeakBisimilarity πŸ“–MathDef
2 mathmath: HomWeakBisimilarity.eqv, HomWeakBisimilarity.refl
IsBisimulation πŸ“–MathDef
8 mathmath: IsBisimulation.isSimulation_iff, IsBisimulation.inv, IsBisimulationUpTo.is_bisimulation, IsBisimulation.bot, IsBisimulation.comp, IsBisimulation.sup, IsBisimulation.deterministic_traceEq_isBisimulation, Bisimilarity.is_bisimulation
IsBisimulationUpTo πŸ“–MathDefβ€”
IsHomBisimulation πŸ“–MathDef
2 mathmath: IsBisimulation.traceEq_not_bisim, Cslib.Logic.HML.theoryEq_isBisimulation
IsHomWeakBisimulation πŸ“–MathDefβ€”
IsSWBisimulation πŸ“–MathDef
4 mathmath: WeakBisimilarity.weakBisim_eq_swBisim, IsWeakBisimulation.isSwBisimulation, isWeakBisimulation_iff_isSWBisimulation, IsSWBisimulation.comp
IsWeakBisimulation πŸ“–MathDef
4 mathmath: IsSWBisimulation.isWeakBisimulation, IsWeakBisimulation.comp, IsWeakBisimulation.inv, isWeakBisimulation_iff_isSWBisimulation
UpToHomBisimilarity πŸ“–MathDef
1 mathmath: IsBisimulationUpTo.is_bisimulation
WeakBisimilarity πŸ“–MathDef
3 mathmath: WeakBisimilarity.symm, WeakBisimilarity.weakBisim_eq_swBisim, WeakBisimilarity.trans
instBotSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instBoundedOrderSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instMaxSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instSemilatticeSupSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instTopSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instTransBisimilarity πŸ“–CompOpβ€”
Β«term_~[_,_]_Β» πŸ“–CompOpβ€”
Β«term_~[_]_Β» πŸ“–CompOpβ€”
Β«term_β‰ˆ[_,_]_Β» πŸ“–CompOpβ€”
Β«term_β‰ˆ[_]_Β» πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
instIsEquivHomBisimilarity πŸ“–mathematicalβ€”HomBisimilarityβ€”HomBisimilarity.refl
Bisimilarity.trans
Bisimilarity.symm
isWeakBisimulation_iff_isSWBisimulation πŸ“–mathematicalβ€”IsWeakBisimulation
IsSWBisimulation		β€”STr.single
IsSWBisimulation.follow_internal_fst
sTr_Ο„STr
STr.comp
IsSWBisimulation.follow_internal_snd

Cslib.LTS.Bisimilarity

Theorems

NameKindAssumesProvesValidatesDepends On
bisimilarity_neq_traceEq πŸ“–mathematicalβ€”Cslib.LTSβ€”Cslib.LTS.IsBisimulation.traceEq_not_bisim
is_bisimulation
deterministic_bisim_eq_traceEq πŸ“–mathematicalβ€”Cslib.LTS.Bisimilarity
Cslib.LTS.TraceEq		β€”le_traceEq
deterministic_traceEq_bisim
deterministic_traceEq_bisim πŸ“–mathematicalCslib.LTS.TraceEqCslib.LTS.Bisimilarityβ€”Cslib.LTS.IsBisimulation.deterministic_traceEq_isBisimulation
gfp πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.Bisimilarityβ€”β€”
is_bisimulation πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.LTS.Bisimilarity		β€”β€”
largest_bisimulation πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.Bisimilarityβ€”β€”
le_traceEq πŸ“–mathematicalβ€”Cslib.LTS.Bisimilarity
Cslib.LTS.TraceEq		β€”Cslib.LTS.IsBisimulation.traceEq
symm πŸ“–mathematicalCslib.LTS.BisimilarityCslib.LTS.Bisimilarityβ€”β€”
trans πŸ“–mathematicalCslib.LTS.BisimilarityCslib.LTS.Bisimilarityβ€”β€”

Cslib.LTS.HomBisimilarity

Theorems

NameKindAssumesProvesValidatesDepends On
eqv πŸ“–mathematicalβ€”Cslib.LTS.HomBisimilarityβ€”refl
Cslib.LTS.Bisimilarity.symm
Cslib.LTS.Bisimilarity.trans
refl πŸ“–mathematicalβ€”Cslib.LTS.HomBisimilarityβ€”β€”
symm_simulation πŸ“–mathematicalβ€”Cslib.LTS.HomBisimilarity
Cslib.LTS.IsHomSimulation		β€”β€”

Cslib.LTS.HomWeakBisimilarity

Theorems

NameKindAssumesProvesValidatesDepends On
eqv πŸ“–mathematicalβ€”Cslib.LTS.HomWeakBisimilarityβ€”refl
Cslib.LTS.WeakBisimilarity.symm
Cslib.LTS.WeakBisimilarity.trans
refl πŸ“–mathematicalβ€”Cslib.LTS.HomWeakBisimilarityβ€”Cslib.LTS.WeakBisimilarity.weakBisim_eq_swBisim

Cslib.LTS.IsBisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
bisim_trace πŸ“–mathematicalCslib.LTS.IsBisimulation
Cslib.LTS.MTr		Cslib.LTS.MTrβ€”β€”
bot πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Relation.emptyHRelation		β€”β€”
comp πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.IsBisimulationβ€”β€”
deterministic_traceEq_isBisimulation πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.LTS.TraceEq		β€”Cslib.LTS.TraceEq.deterministic_isSimulation
Cslib.LTS.TraceEq.symm
follow_fst πŸ“–mathematicalCslib.LTS.IsBisimulation
Cslib.LTS.Tr		Cslib.LTS.Trβ€”β€”
follow_snd πŸ“–mathematicalCslib.LTS.IsBisimulation
Cslib.LTS.Tr		Cslib.LTS.Trβ€”β€”
inv πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.IsBisimulationβ€”β€”
isSimulation πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.IsSimulationβ€”β€”
isSimulation_iff πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.LTS.IsSimulation		β€”β€”
sup πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.IsBisimulationβ€”follow_fst
follow_snd
traceEq πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.LTS.TraceEqβ€”bisim_trace
inv
traceEq_not_bisim πŸ“–mathematicalβ€”Cslib.LTS
Cslib.LTS.IsHomBisimulation
Cslib.LTS.HomTraceEq		β€”Cslib.LTS.MTr.single

Cslib.LTS.IsBisimulationUpTo

Theorems

NameKindAssumesProvesValidatesDepends On
is_bisimulation πŸ“–mathematicalCslib.LTS.IsBisimulationUpToCslib.LTS.IsBisimulation
Cslib.LTS.UpToHomBisimilarity		β€”Cslib.LTS.Bisimilarity.trans
Cslib.LTS.Bisimilarity.largest_bisimulation

Cslib.LTS.IsSWBisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
comp πŸ“–mathematicalCslib.LTS.IsSWBisimulationCslib.LTS.IsSWBisimulationβ€”Cslib.LTS.isWeakBisimulation_iff_isSWBisimulation
Cslib.LTS.IsWeakBisimulation.comp
follow_internal_fst πŸ“–mathematicalCslib.LTS.IsSWBisimulation
Cslib.LTS.Ο„STr		Cslib.LTS.Ο„STrβ€”β€”
follow_internal_snd πŸ“–mathematicalCslib.LTS.IsSWBisimulation
Cslib.LTS.Ο„STr		Cslib.LTS.Ο„STrβ€”β€”
isWeakBisimulation πŸ“–mathematicalCslib.LTS.IsSWBisimulationCslib.LTS.IsWeakBisimulationβ€”Cslib.LTS.isWeakBisimulation_iff_isSWBisimulation

Cslib.LTS.IsWeakBisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
comp πŸ“–mathematicalCslib.LTS.IsWeakBisimulationCslib.LTS.IsWeakBisimulationβ€”Cslib.LTS.IsBisimulation.comp
inv πŸ“–mathematicalCslib.LTS.IsWeakBisimulationCslib.LTS.IsWeakBisimulationβ€”β€”
isSwBisimulation πŸ“–mathematicalCslib.LTS.IsWeakBisimulationCslib.LTS.IsSWBisimulationβ€”Cslib.LTS.isWeakBisimulation_iff_isSWBisimulation

Cslib.LTS.WeakBisimilarity

Theorems

NameKindAssumesProvesValidatesDepends On
symm πŸ“–mathematicalCslib.LTS.WeakBisimilarityCslib.LTS.WeakBisimilarityβ€”β€”
trans πŸ“–mathematicalCslib.LTS.WeakBisimilarityCslib.LTS.WeakBisimilarityβ€”Cslib.LTS.IsWeakBisimulation.comp
weakBisim_eq_swBisim πŸ“–mathematicalβ€”Cslib.LTS.WeakBisimilarity
Cslib.LTS.IsSWBisimulation		β€”β€”

---

← Back to Index