BisimO — Mathlib

English

Definition of bisimilarity for weak sequences: BisimO R on two option-wrapped pairs is LiftRelO with equality on elements.

Русский

Определение бисимиляности слабых последовательностей: BisimO R — это LiftRelO с равенством элементов.

LaTeX

$$$$ \mathrm{BisimO}(R)\;=\;\mathrm{LiftRelO}(\cdot=\cdot)\;R. $$$$

Lean4

/-- Definition of bisimilarity for weak sequences -/
@[simp]
def BisimO (R : WSeq α → WSeq α → Prop) : Option (α × WSeq α) → Option (α × WSeq α) → Prop :=
  LiftRelO (· = ·) R

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