IsBisimulation

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.IsBisimulation

Lean4

/-- Attribute expressing bisimilarity over two `Computation`s -/
def IsBisimulation :=
  ∀ ⦃s₁ s₂⦄,
    s₁ ~ s₂ →
      BisimO R (destruct s₁)
        (destruct s₂)
          -- If two computations are bisimilar, then they are equal

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru