eval_maximal₁ — Mathlib

English

If b is in eval f a, then no nontrivial one-step reachability from b exists; equivalently, for every c, not Reaches₁ f b c.

Русский

Если b находится в eval f a, то из b далее нельзя сделать нетривиального перехода; для любого c верно, что не Reaches₁ f b c.

LaTeX

$$$b \\in \\mathrm{eval}\\ f\\ a \\Rightarrow \\forall c, \\neg \\mathrm{Reaches}_1\\ f\\ b\\ c$$$

Lean4

theorem eval_maximal₁ {σ} {f : σ → Option σ} {a b} (h : b ∈ eval f a) (c) : ¬Reaches₁ f b c
  | bc => by
    let ⟨_, b0⟩ := mem_eval.1 h
    let ⟨b', h', _⟩ := TransGen.head'_iff.1 bc
    cases b0.symm.trans h'

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