get_equiv — Mathlib

English

If c1 ~ c2 and both terminate, then get c1 = get c2.

Русский

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

LaTeX

$$$ c_1 \sim c_2 \rightarrow [\operatorname{Terminates}(c_1)] [\operatorname{Terminates}(c_2)] \rightarrow \operatorname{get}(c_1) = \operatorname{get}(c_2)$$$

Lean4

theorem get_equiv {c₁ c₂ : Computation α} (h : c₁ ~ c₂) [Terminates c₁] [Terminates c₂] : get c₁ = get c₂ :=
  get_eq_of_mem _ <| (h _).2 <| get_mem _

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