English
If R is a bisimulation on M F and M F is inhabited, then whenever two elements s1, s2 are related by R, they are equal. Intuitively, bisimilarity collapses to equality for well-behaved M F.
Русский
Если R — бисимуляция на M F и M F непуст, то для любых элементов s1, s2 с R s1 s2 выполняется s1 = s2. Грубое толкование: бисимуляция эквивалентна равенству для корректного M F.
LaTeX
$$$[Nonempty\ (M F)]\ (bisim : IsBisimulation\ R)\Rightarrow \forall s_1,s_2,\ R\ s_1\ s_2\rightarrow s_1 = s_2$$$
Lean4
theorem eq_of_bisim [Nonempty (M F)] (bisim : IsBisimulation R) : ∀ s₁ s₂, R s₁ s₂ → s₁ = s₂ :=
by
inhabit M F
classical
introv Hr; apply ext
introv
by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
· have H := nth_of_bisim R bisim _ _ ps Hr h
exact H.left
· rw [not_or] at h
obtain ⟨h₀, h₁⟩ := h
simp only [iselect_eq_default, *, not_false_iff]
