is_ret — Mathlib

English

For every code c and continuation k and input v, stepNormal c k v can always be written as a configuration that returns a value (Cfg.ret).

Русский

Для любого кода c и продолжения k и входа v stepNormal c k v всегда можно записать как конфигурацию, возвращающую значение (Cfg.ret).

LaTeX

$$$\\forall c\\,k\\,v.\\;\\exists k',v',\\ stepNormal\\ c\\ k\\ v = Cfg.ret\\ k'\\ v'$$$

Lean4

theorem is_ret (c k v) : ∃ k' v', stepNormal c k v = Cfg.ret k' v' := by
  induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩

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