Documentation Verification Report

Bisimulation

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

Statistics

MetricCount
DefinitionsBisimilarity, IsBisimulation, IsBisimulationUpTo, IsSWBisimulation, IsWeakBisimulation, WeakBisimilarity, instBoundedOrderSubtypeForallForallPropIsBisimulation, instMaxSubtypeForallForallPropIsBisimulation, instSemilatticeSupSubtypeForallForallPropIsBisimulation, instTransBisimilarity, Β«term_~[_]_Β», Β«term_β‰ˆ[_]_Β»
12
Theoremsbisimilarity_neq_traceEq, deterministic_bisim_eq_traceEq, deterministic_traceEq_bisim, eqv, gfp, is_bisimulation, largest_bisimulation, le_traceEq, refl, symm, symm_simulation, trans, bisim_trace, deterministic_traceEq_is_bisim, emptyRelation_bisimulation, is_simulation, simulation_iff, traceEq_not_bisim, union, comp, follow_fst, follow_snd, inv, traceEq, isBisimulation, isWeakBisimulation_iff_isSWBisimulation, comp, follow_internal_fst, follow_internal_fst_n, follow_internal_snd, follow_internal_snd_n, toWeakBisimulation, eqv, refl, symm, trans, weakBisim_eq_swBisim, comp, inv, toSwBisimulation, instIsEquivBisimilarity
41
Total53

Cslib

Definitions

NameCategoryTheorems
Bisimilarity πŸ“–MathDef
21 mathmath: CCS.bisimilarity_par_assoc, Bisimilarity.refl, CCS.bisimilarity_nil_par, CCS.bisimilarity_choice_comm, CCS.bisimilarity_par_comm, CCS.bisimilarity_choice_idem, Bisimilarity.deterministic_bisim_eq_traceEq, Bisimilarity.is_bisimulation, Bisimilarity.le_traceEq, CCS.bisimilarity_par_nil, CCS.bisimilarityCongruence, instIsEquivBisimilarity, Bisimilarity.deterministic_traceEq_bisim, Bisimilarity.largest_bisimulation, Logic.HML.theoryEq_eq_bisimilarity, CCS.bisimilarity_choice_assoc, Bisimilarity.gfp, CCS.bisimilarity_choice_nil, LTS.IsBisimulationUpTo.isBisimulation, Bisimilarity.eqv, Bisimilarity.symm_simulation
WeakBisimilarity πŸ“–MathDef
3 mathmath: WeakBisimilarity.eqv, WeakBisimilarity.refl, WeakBisimilarity.weakBisim_eq_swBisim
instBoundedOrderSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instMaxSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instSemilatticeSupSubtypeForallForallPropIsBisimulation πŸ“–CompOpβ€”
instTransBisimilarity πŸ“–CompOpβ€”
Β«term_~[_]_Β» πŸ“–CompOpβ€”
Β«term_β‰ˆ[_]_Β» πŸ“–CompOpβ€”

Theorems

NameKindAssumesProvesValidatesDepends On
instIsEquivBisimilarity πŸ“–mathematicalβ€”Bisimilarityβ€”Bisimilarity.refl
Bisimilarity.trans
Bisimilarity.symm

Cslib.Bisimilarity

Theorems

NameKindAssumesProvesValidatesDepends On
bisimilarity_neq_traceEq πŸ“–β€”β€”β€”β€”Cslib.Bisimulation.traceEq_not_bisim
is_bisimulation
deterministic_bisim_eq_traceEq πŸ“–mathematicalβ€”Cslib.Bisimilarity
Cslib.TraceEq		β€”le_traceEq
deterministic_traceEq_bisim
deterministic_traceEq_bisim πŸ“–mathematicalCslib.TraceEqCslib.Bisimilarityβ€”Cslib.Bisimulation.deterministic_traceEq_is_bisim
eqv πŸ“–mathematicalβ€”Cslib.Bisimilarityβ€”refl
symm
trans
gfp πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.Bisimilarityβ€”largest_bisimulation
is_bisimulation πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.Bisimilarity		β€”β€”
largest_bisimulation πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.Bisimilarityβ€”β€”
le_traceEq πŸ“–mathematicalβ€”Cslib.Bisimilarity
Cslib.TraceEq		β€”Cslib.LTS.IsBisimulation.traceEq
refl πŸ“–mathematicalβ€”Cslib.Bisimilarityβ€”β€”
symm πŸ“–β€”Cslib.Bisimilarityβ€”β€”β€”
symm_simulation πŸ“–mathematicalβ€”Cslib.Bisimilarity
Cslib.Simulation		β€”β€”
trans πŸ“–β€”Cslib.Bisimilarityβ€”β€”β€”

Cslib.Bisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
bisim_trace πŸ“–β€”Cslib.LTS.IsBisimulation
Cslib.LTS.MTr		β€”β€”β€”
deterministic_traceEq_is_bisim πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.TraceEq		β€”Cslib.TraceEq.deterministic_sim
Cslib.TraceEq.symm
emptyRelation_bisimulation πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulationβ€”β€”
is_simulation πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.Simulationβ€”β€”
simulation_iff πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.Simulation		β€”β€”
traceEq_not_bisim πŸ“–mathematicalβ€”Cslib.LTS.IsBisimulation
Cslib.TraceEq		β€”Cslib.LTS.MTr.single
union πŸ“–β€”Cslib.LTS.IsBisimulationβ€”β€”Cslib.LTS.IsBisimulation.follow_fst
Cslib.LTS.IsBisimulation.follow_snd

Cslib.LTS

Definitions

NameCategoryTheorems
IsBisimulation πŸ“–MathDef
7 mathmath: Cslib.Logic.HML.theoryEq_isBisimulation, Cslib.Bisimulation.traceEq_not_bisim, Cslib.Bisimilarity.is_bisimulation, Cslib.Bisimulation.deterministic_traceEq_is_bisim, Cslib.Bisimulation.simulation_iff, IsBisimulationUpTo.isBisimulation, Cslib.Bisimulation.emptyRelation_bisimulation
IsBisimulationUpTo πŸ“–MathDefβ€”
IsSWBisimulation πŸ“–MathDef
3 mathmath: Cslib.WeakBisimulation.toSwBisimulation, Cslib.WeakBisimilarity.weakBisim_eq_swBisim, isWeakBisimulation_iff_isSWBisimulation
IsWeakBisimulation πŸ“–MathDef
2 mathmath: Cslib.SWBisimulation.toWeakBisimulation, isWeakBisimulation_iff_isSWBisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
isWeakBisimulation_iff_isSWBisimulation πŸ“–mathematicalβ€”IsWeakBisimulation
IsSWBisimulation		β€”STr.single
Cslib.SWBisimulation.follow_internal_fst
STr.comp
Cslib.SWBisimulation.follow_internal_snd

Cslib.LTS.IsBisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
comp πŸ“–β€”Cslib.LTS.IsBisimulationβ€”β€”β€”
follow_fst πŸ“–β€”Cslib.LTS.IsBisimulation
Cslib.LTS.Tr		β€”β€”β€”
follow_snd πŸ“–β€”Cslib.LTS.IsBisimulation
Cslib.LTS.Tr		β€”β€”β€”
inv πŸ“–β€”Cslib.LTS.IsBisimulationβ€”β€”β€”
traceEq πŸ“–mathematicalCslib.LTS.IsBisimulationCslib.TraceEqβ€”Cslib.Bisimulation.bisim_trace
inv

Cslib.LTS.IsBisimulationUpTo

Theorems

NameKindAssumesProvesValidatesDepends On
isBisimulation πŸ“–mathematicalCslib.LTS.IsBisimulationUpToCslib.LTS.IsBisimulation
Relation.UpTo
Cslib.Bisimilarity		β€”Cslib.Bisimilarity.trans
Cslib.Bisimilarity.largest_bisimulation

Cslib.SWBisimulation

Theorems

NameKindAssumesProvesValidatesDepends On
comp πŸ“–β€”Cslib.LTS.IsSWBisimulationβ€”β€”Cslib.LTS.isWeakBisimulation_iff_isSWBisimulation
Cslib.WeakBisimulation.comp
follow_internal_fst πŸ“–β€”Cslib.LTS.IsSWBisimulation
Cslib.LTS.STr
Cslib.HasTau.Ο„		β€”β€”Cslib.LTS.sTr_sTrN
follow_internal_fst_n
follow_internal_fst_n πŸ“–mathematicalCslib.LTS.IsSWBisimulation
Cslib.LTS.STrN
Cslib.HasTau.Ο„		Cslib.LTS.STrβ€”β€”
follow_internal_snd πŸ“–β€”Cslib.LTS.IsSWBisimulation
Cslib.LTS.STr
Cslib.HasTau.Ο„		β€”β€”Cslib.LTS.sTr_sTrN
follow_internal_snd_n
follow_internal_snd_n πŸ“–mathematicalCslib.LTS.IsSWBisimulation
Cslib.LTS.STrN
Cslib.HasTau.Ο„		Cslib.LTS.STrβ€”β€”
toWeakBisimulation πŸ“–mathematicalCslib.LTS.IsSWBisimulationCslib.LTS.IsWeakBisimulationβ€”Cslib.LTS.isWeakBisimulation_iff_isSWBisimulation

Cslib.WeakBisimilarity

Theorems

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

Cslib.WeakBisimulation

Theorems

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

---

← Back to Index