bisim₂ — Mathlib

English

Another presentation of a bisimulation principle, using a lifted relation between destinations to deduce equality.

Русский

Другая формулировка бисимуляционного принципа, используя поднятое отношение между Dest, чтобы вывести равенство.

LaTeX

$$$\\forall r, \\; r x y \\to LiftR (RelLast r) (Cofix.dest x) (Cofix.dest y) \\Rightarrow \\forall x y, r x y \\to x=y$$$

Lean4

/-- Bisimulation principle using `LiftR'` to match and relate children of two trees. -/
theorem bisim₂ {α : TypeVec n} (r : Cofix F α → Cofix F α → Prop)
    (h : ∀ x y, r x y → LiftR' (RelLast' α r) (Cofix.dest x) (Cofix.dest y)) : ∀ x y, r x y → x = y :=
  Cofix.bisim r <| by intros; rw [← LiftR_RelLast_iff]; apply h; assumption

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