destruct_congr_iff — Mathlib

English

Two streams s,t are equivalent iff their destructs are related by the lifted bisimulation.

Русский

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

LaTeX

$$$(s,t)\in \mathrm{WSeq}(\alpha)\;:\; s \sim_W t \iff \mathrm{LiftRel}(\mathrm{BisimO}(\sim_W))(\mathrm{destruct}(s))(\mathrm{destruct}(t))$$$

Lean4

theorem destruct_congr_iff {s t : WSeq α} : s ~ʷ t ↔ Computation.LiftRel (BisimO (· ~ʷ ·)) (destruct s) (destruct t) :=
  liftRel_destruct_iff

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