terminates_congr — Mathlib

English

If c1 ~ c2, then Terminates c1 ↔ Terminates c2.

Русский

Если c1 эквивалентно c2, то завершение вычисления c1 эквивалентно завершению вычисления c2.

LaTeX

$$$ c_1 \sim c_2 \Rightarrow \bigl(\operatorname{Terminates}(c_1) \iff \operatorname{Terminates}(c_2)\bigr)$$$

Lean4

theorem terminates_congr {c₁ c₂ : Computation α} (h : c₁ ~ c₂) : Terminates c₁ ↔ Terminates c₂ := by
  simp only [terminates_iff, exists_congr h]

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